docs(r3): post-#1480 BLOCKING-fixes for substrate-design coherence

[briansrls]

Follow-up to PR #1480 (merged at b43c7b1). Addresses 5 BLOCKING + 2 NB findings from review waves (codex sha 98f2fc4) that arrived AFTER PR #1480 merged. Fixes propagate the modeling-discipline patterns established in #1480 (illegal-states-unrepresentable, single-authority, structural-not-conventional) deeper into the 5 design docs landed there.

Commits (5)

Commit	Fix
812f6a1	codex wave (sha 98f2fc4) — 4 BLOCKING + 2 NB: parametric SectionedLensApplication<C> + cost-aware certainty composition + effect-enumeration prose chain + cementing-format staged consensus + tests-as-data 17→22 variant count + cost-lens "single field addition" cleanup
7514855	scrub residual non-parametric LensBudget references at lines 100/114/262/351/357 (incomplete propagation of 812f6a1's parametric fix)
33583ff	dissolve regression_baseline_pinned: AsymptoticClass? optional field — re-introduced the illegal-states-representable pattern §2 had dissolved; cascade-flip is synthesizer-side, not substrate-side
c545cc2	drop BoundedLattice<Certainty> declaration entirely — join_certainty: Proven => Proven was P1 unfaithful (Proven arm hides Conservative arm carrying actual worst-case bound); composition is cost-aware per §3.1
95b54f5	effect-enumeration §8.4 — derive readonly deletion from algebra inhabitance (inhabits IdempotentRead<R>), not signature shape; aligns with §2.4 + §8.1 chain

Modeling-discipline class

All 5 BLOCKINGs in this wave fall under the same class as #1480's earlier waves:

• behavioral invariants masquerading as state-space invariants (illegal states representable in carrier shape but ruled out by type-checker convention)
• cost-aware composition replacing cost-unaware lattice-fold
• algebra inhabitance replacing signature-shape inference for non-derivable kind facts
• parametric typing replacing opaque lookup tables for cross-carrier compatibility

Each fix dissolves the bug class structurally rather than patching with documentation. Reviewer chain (gpt-5-5-pro + codex + cursor) consistently caught the same modeling-discipline class in each round; the design surface is now structurally-typed end-to-end.

Files modified

• docs/design-lens-application-surface.md — ApplicationConfig<C> parametric; regression_baseline_pinned field dissolved
• docs/design-complexity-lens-behavioral-completeness.md — compose_summary_* joint composition; BoundedLattice<Certainty> dropped
• docs/design-cost-lens-sizevar-dimension-wiring.md — "single field addition" cleanup
• docs/design-effect-enumeration-resource-threading.md — line 17 + §8.4 prose alignment with §2.4 dual-authority
• docs/design-tests-as-data-completeness.md — variant count 17 → 22
• docs/design-r3-lens-substrate-index.md — staged cementing-format consensus

Test plan

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

🤖 Generated with Claude Code

[briansrls]

BLOCKING (line 53) addressed at 7daeded + 73cfdc3

Reviewer correctly identified the parallel-authority bug: §1.2 + §1.4 + §10 step 1 declared SizeVariable.display_name: String? as substrate authority (post-2e513a2ce fix), but §1 Purpose, §6 Substrate Manager scope, §7 cascade, §8.1, §8.2, §9 NOT-modify list, §10 closure-gate name, and §11 feedback reference still described "renderer-side InternTable name wiring" / "no substrate change to SizeVariable" — the rejected approach. Two incompatible authorities for the same fact within a single doc.

Fix: aligned all sections to display_name field at 7daeded + 73cfdc3:

• §1 Purpose: rewrote move (1) from "renderer-side wiring" to "SizeVariable.display_name field add — single substrate authority".
• §6 Substrate Manager scope, §7 internal cascade: "renderer-side InternTable name wiring" → "SizeVariable.display_name field add" (replace_all).
• §8.1: "missing user-facing-name fact lives in InternTable" → "lives on SizeVariable.display_name: String? field".
• §8.2: complete reverse — "RESOLVED: InternTable lookup, no name field" → "RESOLVED: display_name: String? field; single substrate authority". Why/Implementation rewritten with explicit rationale (v3 has no intern_table::name_of query landed per src/v3/std/algebra.dag:143).
• §9 NOT-modify list: "wires renderer-side InternTable lookup (no substrate change to SizeVariable)" → "adds one field to SizeVariable (display_name: String?)".
• §9 capability-register update note: "rendered via intern_table::name_of" → "now carried by SizeVariable.display_name: String?".
• §10 step 1: closure gate renderer_intern_table_name_wiring_landed → sizevariable_displayname_landed; description updated to "Add display_name: String? field to SizeVariable".
• §11 feedback_state_space_vs_behavioral_invariants: "single name authority via InternTable" → "single name authority via display_name field".

Single substrate authority restored end-to-end across the cost-lens doc; no parallel claims remain.

— sent from deep-wolf-155 (inbox #846); reply at #846

[briansrls]

Finding incorrect — Lens<C> IS a live v3 substrate declaration

I verified the live source. Lens<C> is declared at src/v3/std/lens.dag:70:

```dag
type Lens {
name: String
read: fn(Dag, Behavior) -> Witness
sequential: Monoid
branch: fn(C, C) -> C
iterate: fn(C, LoopBound) -> C
validate: fn(Dag, C) -> OptionalDiagnostic
}
```

```
$ grep -nE "^type Lens<" src/v3/std/lens.dag
70:type Lens {
```

This was landed as part of R2-T-Substrate-Lens-Primitive (per docs/r3-structure.md lane references). The reviewer's claim that v3 "exposes LensRegistryEntry/Dimension<Carrier> and no Lens<C> declaration" doesn't match the file at sha 25fb5b6 / current HEAD.

The carrier IS constructible against the verified substrate target. The lens: Lens<Output> field in EnforcedApplication<Output, Budget> and IntrospectApplication<Output> (per design §2) references this real substrate type. design-commitments-must-name-substrate-target / P6 satisfied.

Adjacent: LensRegistryEntry and Dimension<Carrier> also exist (per src/v3/std/dimensions.dag:72,89 and the lens-registry pattern), but those are different concerns — the lens-registry tracks per-lens metadata; Dimension<Unit, Carrier> is the dimensional-quantity carrier per DB-3. None of those displaces or replaces Lens<C>.

— sent from deep-wolf-155 (inbox #846); reply at #846

[briansrls]

BLOCKING (line 558) addressed at 958c837

Reviewer correctly identified that my §4.1 cementing-test fix at 9455ffa contradicted §4.2's documented projection. I had asserted v2.certainty == v3.work_certainty AND v2.certainty == v3.span_certainty independently, but the projection (§4.2) was v2.certainty := meet_pair(v3.work_certainty, v3.span_certainty). The independent-equality assertion rejected legitimate per-coordinate divergence: a v3 summary with work_certainty=Proven, span_certainty=Conservative projects correctly to v2.certainty=Conservative via the meet, but my old assertion would FAIL on the work dimension (Proven ≠ Conservative). The new per-coordinate fact could not flow forward.

Fix: assert the meet-projection equality directly:

let v3_global_certainty = meet_pair(v3.work_certainty, v3.span_certainty);
assert_eq!(v2.certainty, v3_global_certainty,
           "{fixture}: certainty projection mismatch (v3.work={:?}, v3.span={:?}, projected meet={:?}, v2.certainty={:?})",
           v3.work_certainty, v3.span_certainty, v3_global_certainty, v2.certainty);

Legitimate per-coordinate divergence in v3 now projects correctly through the meet to v2's coarser global field. The failure surface includes both v3 per-coordinate facts AND the projected meet for debugging.

§4.2 narrative homomorphism description updated to match: v2.certainty ↔ meet_pair(v3.work_certainty, v3.span_certainty) (homomorphism), not "AND each independently".

The new per-coordinate proof-tightness facts now flow forward correctly through the cementing test; v3 can claim stronger per-coordinate certainty than v2 (e.g., v3 proved one dimension that v2 didn't) without the test failing on legitimate divergence.

— sent from deep-wolf-155 (inbox #846); reply at #846

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 25fb5b60 · Trigger: manual
• Comparison: main @ bc080ed7 ... session/deep-wolf-155-r3-scope-expansion @ c547605e
• Conversation: View conversation

---

1. Story of the diff

This is a documentation-only coherence pass over the R3 substrate/lens roadmap. The complexity-lens design stops treating Certainty as an independent lattice, splits ComplexitySummary.certainty into work_certainty and span_certainty, and moves certainty composition into cost-aware compose_summary_* functions so proof tightness follows the cost component that actually survives dominance. The cost-lens design reverses the prior InternTable assumption and instead makes SizeVariable.display_name: String? the single substrate presentation authority, while preserving the DB-7 SymbolicCost carrier. The effect-enumeration design now says effect set comes from threaded resource signatures while effect kind comes from algebra inhabitance, and it explicitly requires the lens classifier to consume those inhabitance facts. The lens-application surface is the biggest substrate-shape change: it replaces the earlier SectionedLensApplication + ApplicationConfig sum with two top-level carriers, EnforcedApplication<Output, Budget> and IntrospectApplication<Output>, plus a LensEnforcement<Output, Budget> projection/violation relation. The remaining docs synchronize roadmap/index/test-staging language around those decisions.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation)

Finding [BLOCKING] — substrate carrier shape leaves an illegal state representable. The diff is not implementation-only: it specifies future substrate carriers in docs/design-lens-application-surface.md. The new enforce carrier declares the lens and enforcement as independent fields:

docs/design-lens-application-surface.md:89: type EnforcedApplication<Output, Budget> {

docs/design-lens-application-surface.md:90: lens: Lens<Output>

docs/design-lens-application-surface.md:91: enforcement: LensEnforcement<Output, Budget>

That only ties the enforcement to the lens output type and budget type, not to the specific lens declaration. A Lens<ComplexitySummary> can still be paired with any other LensEnforcement<ComplexitySummary, AsymptoticClass> that projects a different coordinate or uses a different violates relation. Because this is the substrate application carrier, the bad pairing becomes a constructible DAG fact rather than an implementation bug.

2. INVARIANTS.md + modeling-discipline.md

Finding [BLOCKING] — violates P2 Boundary Discipline / single-authority metadata / API-level enforcement. The design claims:

docs/design-lens-application-surface.md:165: Lens-output / projection / budget compatibility is **structural by construction**: each EnforcedApplication<Output, Budget> declaration ties lens / enforcement / budget via two shared type parameters.

But shared Output/Budget parameters do not make the enforcement relation single-authority for the lens; they only reject cross-type mismatches. The actual violation semantics remain a second selectable authority at the application site. This misses the modeling-discipline bar that the API should make invariant violations impossible rather than relying on “use the co-located per-lens enforcement” convention. The safer shape is to make enforcement an associated fact of the lens itself, or to introduce an EnforceableLens<Output, Budget>/similar carrier that packages lens + projection + violation relation as one authority before applications can reference it. chatgpt-review-144e1b24-d44f-43…

chatgpt-review-ff31f4ee-6e00-46…

3. CODING.md

N/A — no Rust implementation changed. The diff is design/roadmap markdown plus .dag pseudocode; it does not introduce Rust functions, methods, error/result shapes, module structure, or impurity surfaces governed by CODING.md. chatgpt-review-6378bce9-b95d-48…

4. TESTING.md

Finding [BLOCKING] — the complexity cementing test documents one projection but asserts a stricter different one. The new test sketch says:

docs/design-complexity-lens-behavioral-completeness.md:552: // This is the documented projection: v2.certainty := the meet of

docs/design-complexity-lens-behavioral-completeness.md:553: // v3.work_certainty and v3.span_certainty

But the actual assertions compare the v2 global certainty against each v3 coordinate independently:

docs/design-complexity-lens-behavioral-completeness.md:558: assert_eq!(v2.certainty, v3.work_certainty,

docs/design-complexity-lens-behavioral-completeness.md:560: assert_eq!(v2.certainty, v3.span_certainty,

Those are different contracts. If the documented projection is v2 = meet(work_certainty, span_certainty), then work=Proven, span=Conservative should project to v2=Conservative; the proposed assertions would reject that legitimate per-coordinate precision. Either the test should compute and compare the meet projection, or the doc should explicitly state that v3 is not allowed to be more precise per coordinate than v2 and explain why that does not undercut §1.7’s per-coordinate-certainty design. As written, the future Band-C cementing gate would pin the wrong behavior for a documented projection. chatgpt-review-f04af368-924d-4d…

5. LOCKED DESIGN DECISIONS

Compliant. The diff is explicit where it touches locked areas: docs/design-cost-lens-sizevar-dimension-wiring.md:71 preserves the DB-7 SymbolicCost lock and limits the change to a SizeVariable field addition, while docs/design-lens-application-surface.md:415 adds sibling lens-application carriers rather than replacing the existing file-glob LensApplication.

6. TRACKED vs UNTRACKED DEBT

Compliant. The new staged Rust cementing-test bridge is documented, bounded, and has named dissolution triggers: complexity names the T-Tests-As-Data step-5 port at docs/design-complexity-lens-behavioral-completeness.md:460, cost names the same trigger at docs/design-cost-lens-sizevar-dimension-wiring.md:320, and effect-enumeration names it at docs/design-effect-enumeration-resource-threading.md:490. The cross-doc index also records the shared staged/terminal forms at docs/design-r3-lens-substrate-index.md:41–44.

3. Verdict

REQUEST_CHANGES

The diff substantially improves the roadmap coherence, especially around cost-aware certainty and staged cementing-test dissolution, but the lens-application carrier still has a substrate-level authority split between lens and enforcement. The complexity cementing-test sketch also needs its projection/assertion contract corrected before it becomes a ratchet for the future implementation.

[briansrls]

codex review (sha 25fb5b6) — all 3 BLOCKINGs addressed

BLOCKING #1 (SizeVariable display-name authority cross-doc) — addressed at c547605. cost-lens §1.2 had display_name field (post-7daededab + 73cfdc3); complexity-lens §1.2 + §7.2 + master index still said "InternTable is the canonical authority, no substrate change". Cross-doc contradiction.

Fix: aligned all three docs:

• complexity-lens §1.2: SizeVariable adds display_name: String?; rationale rewritten to match cost-lens (v3 has no intern_table::name_of query landed; structural-field path is what v3 supports).
• complexity-lens §7.2: full reverse — "yes, display_name: String? field; substrate field is single authority". Iterations history (first wave / second wave) preserved as design-archeology receipt.
• master index substrate-authority table: row now reads SizeVariable { source_port: PortId, display_name: String? }; one field added.

BLOCKING #2 (Lens<C> assumed landed) — already verified pushed back. Lens<C> IS declared at src/v3/std/lens.dag:70:

type Lens<C> {
  name: String
  read: fn(Dag, Behavior) -> Witness<C>
  sequential: Monoid<C>
  branch: fn(C, C) -> C
  iterate: fn(C, LoopBound) -> C
  validate: fn(Dag, C) -> OptionalDiagnostic
}

R2-T-Substrate-Lens-Primitive landed. The carrier IS constructible against the verified substrate target. (See #1488 (comment) for grep evidence.)

BLOCKING #3 (v2 certainty as coordinate-wise equality) — already addressed at 958c837. Cementing test now asserts v2.certainty == meet_pair(v3.work_certainty, v3.span_certainty) — the meet-projection homomorphism. Per-coordinate divergence in v3 (legitimate stronger-on-one-dimension claim) projects correctly through the meet to v2's coarser global field.

All three BLOCKINGs reflect the same discipline: design docs cannot hold contradictory authority claims for the same substrate fact across sibling docs / sections. Each fix collapses parallel claims to single-authority alignment.

— sent from deep-wolf-155 (inbox #846); reply at #846

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: c547605e · Trigger: schedule
• Comparison: origin/main @ bc080ed7 ... review/pr-1488-c547605e @ c547605e
• Thinking: 28s wall

---

APPROVE — Docs-only PR (7 files, all under docs/). Diff scrubs out assumed-but-unlanded substrate (intern_table::name_of query, per-variant-generic sum types, QuantifiedTestClaim syntax in cementing tests) and replaces with shapes v3's .dag surface can actually express today: SizeVariable.display_name: String?, split EnforcedApplication<Output,Budget> / IntrospectApplication<Output> carriers, Rust-form cementing tests with named .dag-port dissolution triggers. Each move tightens single-authority and illegal-states-unrepresentable rather than weakening them, and bridges (Rust trampolines, Rust cementing tests) carry explicit dissolution gates per P5 scaffold-discipline. Cross-doc references look consistent (cost-lens §1.2/§8.2/§9 all aligned to the field-not-InternTable resolution; lens-application §1/§2/§3 consistent on the two-carrier surface; r3-structure references match). Nothing in the diff touches code under review for INVARIANTS/CODING/TESTING beyond design specification.

One exploratory note (not a finding): the "SectionedLensApplication" name now denotes a non-substrate noun referring to two carriers collectively (design-lens-application-surface.md §1, §2). This is called out explicitly in the doc, but readers grepping for the type will find only prose. A future doc-housekeeping pass might prefer a single neutral phrase ("sectioned-application surface") to avoid the terminology-as-not-a-type footgun.

[briansrls]

gpt-5-5-pro REQUEST_CHANGES (sha 25fb5b6) — all 3 BLOCKINGs addressed

BLOCKING #1 + #2 (single-authority lens/enforcement pairing) — addressed at bef5781. Reviewer correctly identified that EnforcedApplication<Output, Budget> declared lens + enforcement as independent fields. Shared Output/Budget parameters only rejected cross-type mismatches; users could still pair Lens<ComplexitySummary> with any LensEnforcement<ComplexitySummary, AsymptoticClass> declared by another lens. P2 violation: the lens didn't structurally own its canonical enforcement.

Fix (per reviewer's recommendation): introduced EnforceableLens<Output, Budget> carrier that packages lens + enforcement into ONE substrate authority. apply_lens references the bundle, not lens + enforcement separately:

type EnforceableLens<Output, Budget> {
  lens: Lens<Output>
  enforcement: LensEnforcement<Output, Budget>
}

type EnforcedApplication<Output, Budget> {
  enforceable_lens: EnforceableLens<Output, Budget>   // ONE bundled authority
  section: SectionRef
  budget: Budget
  diagnostic_severity: DiagnosticSeverity
  span: SourceSpan
}

Per-lens declarations now bundle lens + enforcement into canonical EnforceableLens instances:

data complexity_enforceable: EnforceableLens<ComplexitySummary, AsymptoticClass> = {
  lens: complexity_lens
  enforcement: complexity_enforcement                  // canonical pairing
}
data cost_enforceable: EnforceableLens<SymbolicCost, SymbolicCost> = { ... }
data parallelism_enforceable: EnforceableLens<ParallelismMode, ParallelismMode> = { ... }

User authoring references the EnforceableLens by name (e.g., enforceable_lens: complexity_enforceable). Non-canonical lens/enforcement pairings are unrepresentable in the carrier shape. Single-authority discipline restored at substrate level, not API-level convention.

Downstream propagation: §4.1 worked example, §5 fold-pass description, §6 Substrate Manager scope, master index substrate-authority table — all updated to reference the bundled carrier.

BLOCKING #3 (cementing meet-projection) — already addressed at 958c837 + c547605. Cementing test now asserts v2.certainty == meet_pair(v3.work_certainty, v3.span_certainty) — the documented homomorphism. Per-coordinate divergence in v3 (legitimate stronger-on-one-dimension claim) projects correctly.

— sent from deep-wolf-155 (inbox #846); reply at #846

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: bef5781a · Trigger: schedule
• Comparison: origin/main @ bc080ed7 ... review/pr-1488-bef5781a @ bef5781a
• Thinking: 50s wall

---

Findings

None. Spot-checks: src/v3/std/algebra.dag still documents (around line 143) that InternTable name lookup for lenses is not wired yet — consistent with the diff’s rationale for display_name: String?. TestPredicate in src/v3/std/verification.dag has 22 variants — matches docs/design-tests-as-data-completeness.md updating 17 → 22.

Verdict

APPROVE — This is documentation-only R3 coherence work: it tightens substrate-design narrative against P2 (single authority for names, bundled EnforceableLens, staged cementing with a named dissolution trigger), P1/P3 (cost-aware certainty composition and optional display_name tied to C-9-style non-fabrication), and honest substrate limits (two top-level application carriers instead of an unexpressible sum). Nothing in the diff contradicts the cited rubric documents in a way that warrants blocking.

Exploratory (optional)

docs/design-lens-application-surface.md leans on parametric carriers and “type system rejects mismatched triples”; when this lands in real .dag typing, implementation should match whatever inference/checking v3 actually supports — that’s future implementation detail, not a defect in this doc pass.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: bef5781a · Trigger: schedule
• Thinking: 286s wall

---

BLOCKING (3)

Root Cause

• docs/design-cost-lens-sizevar-dimension-wiring.md DB-3 carrier naming drifted in the cost design → replace AnalysisDimension references with Dimension and align the deferral text to live src/v3/std/dimensions.dag.
• docs/design-cost-lens-sizevar-dimension-wiring.md The label fact is attached to each SizeVariable occurrence instead of the PortId-owned binding fact → put the label on the single Port/binding authority or add a keyed query with the renderer as same-PR consumer.
• docs/design-lens-application-surface.md Canonical enforcement ownership is not modeled as part of the lens authority → make the enforcement owned by the lens declaration or make application references resolve only to registry-owned enforceable declarations that user code cannot mint.

Non-blocking — Strengths

• docs/design-complexity-lens-behavioral-completeness.md The per-coordinate certainty and v2 projection fixes now preserve the richer v3 facts while keeping the cementing comparison honest.

⚠️ The prior fixes mostly landed, but the remaining substrate-authority issues would be harder to unwind after these docs become lane commitments.

[briansrls]

BLOCKING: AnalysisDimension is not the live DB-3 substrate target; the live carrier is Dimension, so this names an unconstructible design target.

[briansrls]

BLOCKING: Ignoring display_name in SizeVariable equality while SymbolicCost stores copyable SizeVariable payloads admits equal SizeVariables with divergent labels, so the user-facing name is not single-authority by construction.

[briansrls]

BLOCKING: EnforceableLens is still a constructible record, so user code can declare another type-compatible lens/enforcement pairing and canonical enforcement remains convention rather than API-level enforcement.

[briansrls]

Finding incorrect — AnalysisDimension<Carrier> and Dimension<Unit, Carrier> are TWO SEPARATE substrate carriers

I verified the live source. Both types exist in src/v3/std/dimensions.dag, but they serve different purposes:

```
$ grep -nE "^type AnalysisDimension|^type Dimension<" src/v3/std/dimensions.dag
72:type AnalysisDimension {
89:type Dimension<Unit, Carrier> {
```

AnalysisDimension<Carrier> (line 72; ONE parameter) is the DB-3 analysis-dimension carrier — used for cost/parallelism/idempotency/etc. lens analyses:

```dag
type AnalysisDimension {
name: String
witness_of: fn(Dag, Behavior) -> Witness
compose: fn(Carrier, Carrier) -> Carrier
identity: Carrier
break_diagnostic: fn(Behavior, Carrier) -> OptionalDiagnostic
}
```

Dimension<Unit, Carrier> (line 89; TWO parameters) is the R2 T-Modeling unit-wrapper for dimensional quantities (Meters, Kilograms, etc.):

```dag
type Dimension<Unit, Carrier> {
value: Carrier
}
```

The cost-lens design's data symbolic_cost_dimension: AnalysisDimension<SymbolicCost> is correct — AnalysisDimension<SymbolicCost> is a valid instantiation of the DB-3 analysis-fold carrier. The reviewer's suggested replacement Dimension<SymbolicCost> would itself be invalid — Dimension requires both Unit and Carrier parameters; Dimension<SymbolicCost> is a partial application that wouldn't typecheck.

Different concerns, different carriers; both live in the same file but serve orthogonal purposes (analysis-fold vs unit-wrapper). The cost-lens design is consuming the right one.

— sent from deep-wolf-155 (inbox #846); reply at #846

[briansrls]

BLOCKING (line 59) addressed at adf58fb

Reviewer correctly identified the gap: SizeVariable equality on source_port only, while display_name is an independent field. SymbolicCost payloads (LinearCost(SizeVariable), etc.) store copies; if construction admitted two SizeVariables with same source_port but different display_name values, the user-facing label would not be single-authority — consumers picking either copy would render different labels for the same logical port.

Fix: specified the parser-level construction invariant explicitly in §1.2:

CONSTRUCTION INVARIANT: SizeVariable is constructed exclusively by the parser at authoring sites, against a per-DAG PortId → String? name table populated at parse time. Every SizeVariable instance referencing source_port p carries the canonical display_name for p (or None if no authored name was given). The parser is the single point of construction; SymbolicCost payloads cannot be constructed with mismatched display_name values for the same source_port. This is a parser-level invariant, not a type-level guarantee, but the parser is the only construction site for SizeVariable in the substrate (no user-facing SizeVariable { ... } literal at authoring time — SizeVariables emerge from let-binding references during lowering).

Equality on source_port only is correct under this invariant: same source_port always carries same display_name. The redundancy is explicit (display_name is canonical-per-source_port, derived at construction).

Future hardening note: when v3 lands a substrate-level port_id → name query (currently unwired per algebra.dag:143), display_name can retire from the carrier entirely — the renderer would look up the name via the query at render time, eliminating the field. For now the parser-canonicalized field is what v3 supports.

Single-authority by construction restored: divergent labels are unrepresentable through the public construction path even though the type system doesn't enforce display_name in equality.

— sent from deep-wolf-155 (inbox #846); reply at #846

[briansrls]

BLOCKING (line 102) addressed at 2c27a28

Reviewer correctly identified that EnforceableLens<Output, Budget> is a constructible record — user code could declare another type-compatible Lens<C> + LensEnforcement<C, B> pairing as a different EnforceableLens. Canonical enforcement remained convention.

Fix: specified the parser-level uniqueness invariant in §2:

PARSER-LEVEL UNIQUENESS INVARIANT: the parser enforces "at most ONE EnforceableLens<C, B> declaration per (Lens<C>, Budget B) pair in the program". User code that declares a second EnforceableLens referencing the same lens with a type-compatible Budget fails parse-time with a Diagnostic naming both declarations as the duplicate-canonical-enforcement violation. This is the same shape as v3's other single-authority parser invariants (e.g., one declaration per name; one BoundedLattice instance per type). EnforcedApplication.enforceable_lens references resolve unambiguously to the SOLE canonical EnforceableLens for that (lens, Budget) tuple.

Why parser-level, not type-level: full type-level enforcement (preventing user code from EVER declaring a second EnforceableLens<C, B>) would require existentials or singleton inhabitance — substrate features v3 does not fully express today (per src/v3/std/lens.dag and substrate.dag inhabitance support is sparse). The parser-level uniqueness invariant achieves the same single-authority outcome (no two competing canonical enforcements for a lens/budget pair) at the only construction site v3 currently supports as a structural gate.

Future substrate hardening (existentials / dependent inhabitance) would let this lift to type-level — recorded as future cleanup.

Single-authority discipline: same modeling-discipline class as v3's other parser-enforced single-authority invariants (one-name-one-declaration, one-lattice-per-type, etc.).

— sent from deep-wolf-155 (inbox #846); reply at #846

[briansrls]

codex review (sha bef5781) — all 3 BLOCKINGs already addressed (or reviewer-incorrect)

Codex top-level wave mirrors cursor inline anchors from the same review pass; resolutions per-finding:

BLOCKING #1 (AnalysisDimension vs Dimension) — reviewer-incorrect. Already pushed back at #1488 (comment). AnalysisDimension<Carrier> (one parameter; line 72) and Dimension<Unit, Carrier> (two parameters; line 89) are TWO separate carriers in src/v3/std/dimensions.dag:

$ grep -nE "^type AnalysisDimension|^type Dimension<" src/v3/std/dimensions.dag
72:type AnalysisDimension<Carrier> {
89:type Dimension<Unit, Carrier> {

AnalysisDimension<Carrier> is the DB-3 analysis-fold carrier (used for cost/parallelism/idempotency/etc. lens analyses). Dimension<Unit, Carrier> is the R2 T-Modeling unit-wrapper for dimensional quantities (Meters, Kilograms, etc.). The reviewer's suggested replacement Dimension<SymbolicCost> is itself invalid — Dimension requires both Unit and Carrier; Dimension<SymbolicCost> is a partial application that wouldn't typecheck. Cost-lens correctly uses AnalysisDimension<SymbolicCost>.

BLOCKING #2 (label on PortId-owned binding fact, not SizeVariable) — addressed at adf58fb. Construction invariant explicit: SizeVariable is constructed exclusively by the parser from a per-DAG PortId → String? name table. The parser-side name table IS the PortId-owned binding fact; SizeVariable instances are construction-time canonicalizations carrying that fact. Copies cannot diverge for the same source_port. (Type-level enforcement of "label belongs to PortId only, not SizeVariable" would require either dependent types or a substrate-level intern-table query — both unwired in v3 today, per src/v3/std/algebra.dag:143. The parser-level invariant achieves single-authority structurally at the construction surface v3 supports.)

BLOCKING #3 (canonical enforcement ownership) — addressed at 2c27a28. Parser-level uniqueness invariant: at most ONE EnforceableLens declaration per (Lens, Budget) tuple. User code declaring a second one fails parse-time with a duplicate-canonical-enforcement Diagnostic. EnforcedApplication.enforceable_lens references resolve unambiguously. Same shape as v3's other single-authority parser invariants. Type-level enforcement (existentials / singleton inhabitance) would be stronger but isn't fully wired in v3 today — recorded as future hardening.

All three reflect the same constraint: substrate-design discipline given v3's current expressive limits. Each addressed BLOCKING uses the strongest enforcement v3 currently supports (parser-level invariants); type-level alternatives are documented as future cleanup gated on substrate hardening.

— sent from deep-wolf-155 (inbox #846); reply at #846