docs(r3): post-#1488 follow-up — SizeVariable construction invariant + EnforceableLens uniqueness

[briansrls]

Follow-up to PR #1488 (merged at c03fc60). Addresses 2 BLOCKING findings from cursor review wave (sha bef5781) that arrived AFTER PR #1488 merged. Both close subtle parallel-authority gaps in the substrate-design carriers landed there.

Commits (2)

Commit	Fix
adf58fb	SizeVariable.display_name construction invariant: parser is single point of construction; per-DAG PortId → String? name table canonicalizes display_name; SymbolicCost payload copies cannot diverge for same source_port. Closes the gap where SizeVariable equality on source_port only admitted divergent labels.
2c27a28	EnforceableLens canonicality: parser-level uniqueness invariant — at most ONE EnforceableLens<C, B> declaration per (Lens, Budget B) pair. User code declaring a second one fails parse-time with duplicate-canonical-enforcement Diagnostic. Closes the gap where multiple EnforceableLens declarations could compete as canonical.

Modeling-discipline class

Both fixes use parser-level uniqueness/canonicalization invariants as the strongest single-authority enforcement v3 currently supports. Type-level alternatives (existentials, singleton inhabitance, dependent types) would let these lift to type-level guarantees but require substrate hardening v3 doesn't ship today. Each fix documents the parser-level invariant explicitly + names the future hardening trigger.

Files modified

• docs/design-cost-lens-sizevar-dimension-wiring.md — §1.2 construction invariant added (parser canonicalizes display_name).
• docs/design-lens-application-surface.md — §2 EnforceableLens parser-level uniqueness invariant.

Test plan

• Docs-only PR; no executable code touched
• cargo fmt --all --check (passes via pre-push hook)
• Reviewer chain to verify single-authority invariants on flip-to-ready

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 2c27a28f · Trigger: schedule
• Comparison: origin/main @ c03fc604 ... review/pr-1500-2c27a28f @ 2c27a28f
• Thinking: 17s wall

---

APPROVE — Documentation-only changes that strengthen previously-asserted single-authority claims by spelling out the construction-site mechanism (parser canonicalization for SizeVariable.display_name, parser-level uniqueness for EnforceableLens<C, B>). Both additions are honest about the layer (parser-level invariant, not type-level) and name the future substrate work that would lift them. No diff content violates INVARIANTS, modeling-discipline, CODING, or TESTING.

Exploratory observations (optional):

• docs/design-cost-lens-sizevar-dimension-wiring.md:74 says SymbolicCost payloads "cannot have divergent labels" — true under the stated invariant, but the surrounding type (SizeVariable { source_port, display_name }) still structurally permits the divergence the prose forbids. The "Future hardening" note (retire display_name, query by port_id at render time) is the real illegal-states-unrepresentable fix; worth keeping that trigger named on a lane gate so the parser-only invariant doesn't ossify.
• docs/design-lens-application-surface.md:103-106 cites src/v3/std/lens.dag and substrate.dag for "inhabitance support is sparse" — readers chasing the citation will want a more specific anchor (line or symbol) than the bare filename, similar to the algebra.dag:143 style used in the sibling doc.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 2c27a28f · Trigger: schedule
• Thinking: 152s wall

---

✅ Docs-only follow-up; the added parser-level invariants are documented, bounded, and consistent with the thesis/invariants, with no blocking concerns.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 96bb1ab2 · Trigger: schedule
• Comparison: origin/main @ 23542b50 ... review/pr-1500-96bb1ab2 @ 96bb1ab2
• Thinking: 24s wall

---

Findings

No blocking issues. The diff only updates two design markdown files. It states parser-level (not type-level) rules for SizeVariable.display_name and EnforceableLens uniqueness, which matches modeling-discipline.md practice 6’s distinction between structural vs behavioral enforcement instead of pretending the substrate proves those facts today. The Future hardening paragraph names a concrete dissolution (“when a substrate-level port_id → name query lands, retire display_name”), which fits INVARIANTS.md P5-style tracked follow-up rather than an unnamed bridge.

Nothing in this diff touches CODING.md (no Rust) or TESTING.md (no tests).

Verdict

APPROVE — Narrow documentation follow-up: construction invariant for SizeVariable, uniqueness story for EnforceableLens, and an explicit future cleanup for display_name. No rubric violation grounded in these lines.

Exploratory observations (optional)

The new cross-reference “currently unwired per src/v3/std/algebra.dag:143” (added around 90:90:docs/design-cost-lens-sizevar-dimension-wiring.md) points at a comment line whose text is about an InternTable lookup not being run yet; that’s aligned in spirit with a future name/query path, but “port_id → name query” vs “InternTable lookup” wording doesn’t match that line verbatim—consider a small range cite (e.g. 141–145) if you want pixel-perfect traceability. Non-blocking.