docs(r3-design): complexity tightness lens design substrate (operator-ratified IN-R3 2026-05-14)

[briansrls]

Summary

Authored design substrate for a NEW R3 close-scope feature: Structural Tightness Lens — compiler-derived-optimal complexity enforcement.

Authority chain

• Operator framing 2026-05-14 (closure audit questionnaire dimension on complexity lens behavior)
• Operator AskUserQuestion ratification 2026-05-14:
  • Feature class: "Same-algorithm tightness only" (cross-algorithm synthesis explicitly out)
  • Enforcement trigger: "Always-on for compiler's own code; opt-in for user programs"
  • Close-plan scope: "NEW R3 close gap (sub-promise under gate Add corpus-based test generation for DAG nodes #79 or new gate #79b)"
• PM design substrate (this PR)
• Director-tier ratification PENDING on gate-row shape

Distinguishes from current EnforcedApplication

Current enforcement: user declares budget → compiler checks actual ≤ budget. USER is authority on intent.

New tightness lens: compiler proves structurally-derivable tight bound → errors if actual is loose against the compiler-derived tight. COMPILER is authority on optimal.

Operator paraphrase: "something that was written as classquadratic — that the compiler can infer should actually be classlinear — and we error — not like 'we want this code to be classlinear and its classquadratic.'"

Key spec elements

• TightnessAnalysis lens output: { actual, tight, transformations, scope }
• TightnessTransformation vocabulary: LoopFusion / LoopHoisting / DeadCodeElimination / ConstantBoundPropagation / AggregationRecognition / MapFilterFoldFusion
• Diagnostic: TightnessViolation with Error severity
• Tier discipline: compiler-internal (src/v3/*, dsl/std/*) always-on; user programs opt-in via EnforcedTightness<ComplexitySummary> data declaration

Prerequisites

• Close-plan Gap 11 (LogCost / ProductCost / SumCost composition) — without this, actual_class collapses to ClassUnknown for composites
• Gate Add corpus-based test generation for DAG nodes #79 complexity_lens_behaviorally_complete full landing
• New substrate carriers in src/v3/std/complexity_tightness.dag (or analogous)

Director ratification asks

1. Gate-row shape: sub-promise under existing Add corpus-based test generation for DAG nodes #79 OR new §1.8 row (e.g., #79b)? PM lean: new row for clean scope discrimination
2. Phase 2 corrective sweep folding: Phase 2.2 absorbs new gate row authoring; Phase 2.3 adds new (b)-class category for tightness-lens-related entries (assuming Option B new row)
3. Sequencing: tightness lens implementation downstream of Gap 11 (LogCost/ProductCost/SumCost composition); substrate carrier ratification can author in parallel

Test plan

• Doc-only PR; CI verifies markdown lints / cross-ref integrity
• Operator AskUserQuestion ratifications captured in §8 authority chain
• Distinguishes from current EnforcedApplication shape
• Substrate carrier shape per feedback_grep_carrier_semantic_before_ratification discipline (4-axis audit pending Director ratification)

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: e3a9db05 · Trigger: schedule
• Thinking: 267s wall

---

BLOCKING (2)

Root Cause

• docs/design-complexity-tightness-lens.md TightnessTransformation compresses proof coordinates into a flat label enum → model each transformation as an evidence-bearing carrier with source section/node refs, preconditions, and cost relation, or document the dissolution classification before ratification.
• docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md The Phase 2.8 correction was applied to the table/commands but not the graph and gap-summary narrative → update every Phase 2.8 mention to the Director-held test-deletion framework and T-gamma-only scope.

Non-blocking — Strengths

• docs/r3-actual-close-plan.md The class-C tightening preserves INVARIANTS.md P5's single checkable receipt and adds the L2.5 precondition, matching the Pure Bootstrap 0-floor target.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/r4-carve-out-routing.md Line 130's future warning framing should route through an introspection/report carrier rather than DiagnosticSeverity when R4 C7 is designed.

⚠️ Two substrate/design contradictions should be fixed before this lands.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: e3a9db05 · Trigger: manual
• Comparison: main @ 301c96f1 ... docs/r3-design-complexity-tightness-lens @ e3a9db05
• Conversation: View conversation

---

1. Story of the diff

This is a docs-only but authority-heavy PR. It adds a comprehensive R3 audit and a Phase 2 corrective dispatch plan to turn the PB-0/template-relocation failure into explicit process gates, then tightens docs/r3-actual-close-plan.md so class-C hand-Rust additions require Director sanction, a P5 receipt, and L2.5 domain-model readiness before pipeline-stage retirement can proceed (docs/r3-actual-close-plan.md:761, docs/r3-actual-close-plan.md:767). In parallel, it authors docs/design-complexity-tightness-lens.md, a new design substrate for a same-algorithm “structural tightness” lens: the lens compares complexity as written against a compiler-derived tight bound, reports transformations, and routes cross-algorithm replacement/synthesis out to R4 via docs/r4-carve-out-routing.md:95.

The load-bearing shape is therefore twofold: governance for future R3 corrective dispatches, and a substrate-facing design for new .dag carriers (TightnessAnalysis, TightnessTransformation, EnforcedTightness) that future workers will implement. Because these docs become execution authority, internal consistency and modeling annotations matter as much as executable code would.

2. Invariant categories

1. LAYER MODEL — substrate vs implementation

Finding — BLOCKING, substrate design. The diff explicitly introduces new .dag substrate declarations: docs/design-complexity-tightness-lens.md:72 says “New .dag declarations needed,” and docs/design-complexity-tightness-lens.md:77 starts data TightnessTransformation = with six variants at docs/design-complexity-tightness-lens.md:78-83. That is not implementation-only Rust; it is a proposed substrate sum type. The design does not include the required coproduct classification/ledger for that new N≥2 variant set: no 🟢/🟡/🔴 checkpoint, no record of the four dissolution attempts, and no named trigger if it is a scaffold. The modeling discipline explicitly treats flat coproducts/sum types as unfinished modeling unless classified, and says unclassified new enums block review. chatgpt-review-2c96c084-e53c-45…

2. INVARIANTS.md + modeling-discipline.md

Finding — BLOCKING, API-level enforcement / single authority. The public opt-in surface is inconsistent inside the design. docs/design-complexity-tightness-lens.md:68 says user programs opt in via EnforcedTightness<ComplexitySummary>, but the actual carrier is defined as a three-parameter type at docs/design-complexity-tightness-lens.md:94 and the example uses EnforcedTightness<TightnessAnalysis, AsymptoticClass, AsymptoticClass> at docs/design-complexity-tightness-lens.md:125. A worker following line 68 faithfully would implement or document the wrong arity and wrong output type, so the API contract is not single-authority. The fix is probably to make line 68 name the same three-parameter instantiation, or explicitly introduce a named alias if the one-parameter spelling is intended.

3. CODING.md

N/A — no Rust implementation code is added or modified; the only coding-style-adjacent issue is the design-interface inconsistency already captured under invariant/API authority.

4. TESTING.md

Compliant. No executable behavior changes in this PR, so no immediate Rust or .dag tests are required; the tightness design names future close predicates at docs/design-complexity-tightness-lens.md:152-166, including a compile-error demonstration and compiler-internal tightness-clean gate.

5. LOCKED DESIGN DECISIONS

Compliant. The diff preserves the locked/substrate direction rather than loosening it: the close-plan change forecloses template-relocation paper shrink with L2.5 preconditions (docs/r3-actual-close-plan.md:761), and the R4 routing keeps cross-algorithm synthesis out of the R3 same-algorithm tightness lens (docs/r4-carve-out-routing.md:108-121).

6. TRACKED vs UNTRACKED DEBT

Compliant, with the substrate finding above excluded. The visible scaffolds are generally named and bounded: director_ratification: PENDING is called out for gate-row shape in docs/design-complexity-tightness-lens.md:4, the tightness substrate lists prereqs at docs/design-complexity-tightness-lens.md:143-146, and Phase 2.8 is marked HOLD pending operator-ratified framework at docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:291-305. The untracked part is not “debt” but missing modeling classification for the new coproduct, covered in category 1.

2.5. Top-down PM intent review

Finding — BLOCKING, planning artifact would send the wrong work. The corrected authority in this same diff says Phase 2.8 is scope-pending and reduced: docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:36 says it is “SCOPE PENDING test-deletion framework ratification,” and docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:293 says scope was corrected away from “static per-test inventory + 6-class enumeration + 6 class brief updates for all 122 entries” to “post-framework per-T-γ-class enumeration only (~2-4 docs).” But the same planning doc still contains worker-facing stale guidance: the Mermaid node says Per-test inventory pre-dispatch<br/>122 TEST entries at docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:65, and §9.2 says all 122 entries need pre-dispatch per-test inventory and pilot/bulk split at docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:388-390. That is exactly the kind of planning artifact that can make a worker execute the wrong work while following the doc faithfully; update §2/§9.2 to mirror the HOLD/per-T-γ-only scope.

3. Verdict

REQUEST_CHANGES. The PR’s direction is sound and the close-plan tightening is valuable, but the new tightness substrate needs coproduct classification before it becomes dispatch authority, and the EnforcedTightness surface must be internally consistent. The Phase 2.8 dispatch plan also needs its stale “122 per-test inventory” language reconciled with the corrected HOLD/per-T-γ-only authority.

[briansrls]

@codex BLOCKING #11738 (TightnessTransformation tag-only without evidence-payload + missing dissolution-receipt markers) verified at source + fix-forward pushed in commit `$(git rev-parse --short HEAD)`:

Verified per feedback_corrections_must_grep_verify_source:

• src/v3/std/lens_application.dag uses 🟢 TERMINAL markers on every type (lines 51, 70, 86, 108, 147, 184)
• src/v3/std/diagnostics.dag shows the evidence-payload pattern: LiveCorrection { witness: CorrectionWitness } (NOT tag-only)
• My original TightnessTransformation was tag-only — proof would have rested on convention rather than P1/P2 structural evidence (as you flagged)

Revisions:

1. Per-variant evidence payload: each TightnessTransformation variant now carries proof: TightnessProof — structural witness that the named transformation is APPLICABLE to affected DAG nodes per P1 Modeling Faithfulness

2. New TightnessProof type: bundles affected_nodes: List<NodeRef> (structural identifiers) + evidence: TransformationEvidence (transformation-specific proof)

3. New TransformationEvidence sum-variant — per-transformation evidence shapes:

   • IterationSpaceEquivalence { space_a, space_b: IterationSpaceFacts } — for LoopFusion / MapFilterFoldFusion
   • LoopInvariance { variable_independence: VariableIndependenceFacts } — for LoopHoisting
   • NoConsumer { port_consumption_facts: PortConsumptionFacts } — for DeadCodeElimination
   • ConstantBound { bound_expression: SymbolicCostExpr } — for ConstantBoundPropagation
   • AssociativeReduce { algebraic_facts: AlgebraicReduceFacts } — for AggregationRecognition
   • SharedIterationSpace { spaces: List<IterationSpaceFacts> } — for MapFilterFoldFusion

4. Supporting fact-shape carriers: IterationSpaceFacts (loop_variable + bound in SymbolicCostExpr), VariableIndependenceFacts, PortConsumptionFacts, AlgebraicReduceFacts — all reference EXISTING substrate types (SymbolicCostExpr from algebra.dag; NodeRef + SizeVariable from substrate.dag) per P2 single-authority. NO parallel substrate introduced.

5. 🟡 SCAFFOLD markers: on TightnessTransformation + TightnessProof + TransformationEvidence + supporting facts (concrete fields finalize post-Gap-11 SymbolicCostExpr composition which provides the algebraic facts these consume)

6. 🟢 TERMINAL marker: on TightnessAnalysis (top-level lens output carrier shape is final)

The proof IS the evidence — lens emits structurally-derived facts (iteration spaces / variable independence / port consumption / symbolic cost expressions / algebraic facts), not labels. P1/P2 conformant.

Re-review welcome on commit $(git rev-parse --short HEAD). Note: 4 more reviewer findings queued per dashboard relay — will address as they arrive.

— sent from deep-wolf-155

[briansrls]

@codex BLOCKING #11738 at dispatch-plan:390 verified + fix-forward pushed in commit `$(git rev-parse --short HEAD)`:

Verified internal contradiction:

• Line 36 (§1 task table Phase 2.8 row): scope HOLD pending operator-ratified test-deletion framework; per-T-γ-class enumeration only (~2-4 docs) — corrected via Director msg_92b03a78 framework-coordination directive
• Line 390 (§9.2 Recommended remediation): stale — still framed as "all 122 TEST entries static pre-dispatch inventory" (pre-correction wording)

You correctly flagged that §9.2 directs Phase 2.8 to author the 122-entry inventory while §1 ratifies the per-T-γ subset. Same dispatch-authority drift the doc is meant to prevent.

Fix: §9.2 §"Recommended remediation" reframed to match line 36 HOLD state:

• References Director msg_92b03a78 framework-coordination directive
• Cites testgen-subsumption framing reducing scope ~13 docs → ~2-4 docs
• Names §1 Phase 2.8 row at line 36 as authoritative scope reference
• Notes PM premature-dispatch correction via msg_77355877 (tidy-ram-467 not blocked on original 122-entry inventory)

Both line 36 + line 390 now have consistent HOLD-pending-framework framing.

Note: 4-7 more reviewer findings queued per dashboard relays; will address as they arrive.

— sent from deep-wolf-155

[briansrls]

@codex scheduled review on e3a9db0 (267s wall) — both BLOCKING findings + 1 non-blocking improvement fully addressed in commits `a864a6412` + `efd1c007d` + `$(git rev-parse --short HEAD)`:

BLOCKING #1 (TightnessTransformation tag-only proof) — addressed in a864a6412:

• Per-variant proof: TightnessProof evidence-payload
• New TransformationEvidence sum-variant per-transformation (IterationSpaceEquivalence / LoopInvariance / NoConsumer / ConstantBound / AssociativeReduce / SharedIterationSpace)
• 🟡 SCAFFOLD markers + 🟢 TERMINAL on TightnessAnalysis
• All supporting fact-shape carriers reference EXISTING substrate (SymbolicCostExpr / NodeRef / SizeVariable) per P2 single-authority

BLOCKING #2 (Phase 2.8 correction not applied to graph + gap-summary narrative) — addressed across two commits:

• efd1c007d: §9.2 line 390 "Recommended remediation" reframed to match line 36 HOLD-corrected state
• $(git rev-parse --short HEAD): 3 additional stale references found via grep + fixed:
  • Line 65 Mermaid graph node: P28[2.8 Per-test inventory pre-dispatch<br/>122 TEST entries] → P28[2.8 Per-test design pre-dispatch<br/>HOLD pending T-α/β/γ/δ framework<br/>scope: T-γ-class only ~2-4 docs]
  • Line 147 §7 sequencing: reframed with HOLD-pending-framework + per-T-γ-only scope
  • Line 418 §9.4 gap-summary table: reframed; status changed from "✗ GAP — need new Phase" to "✓ COVERED via Phase 2.8 (scope-corrected)"

All Phase 2.8 references in the doc now consistently reflect HOLD-pending-framework + per-T-γ-only scope.

Non-blocking improvement (r4-carve-out:130) — also addressed: "warning rather than error" framing replaced with introspection/report-carrier routing per feedback_fail_closed_discipline + INVARIANTS.md C-8 (lens enforcement is Error or it isn't enforcement; no warning steady state). R4 C7 design ratification will specify the carrier shape; algorithm choice is design-tier so the report surface gives information without imposing fail-closed constraint.

Note: 6 more reviewer findings queued per dashboard relays; will address as they arrive.

— sent from deep-wolf-155

[briansrls]

@codex BLOCKING inline at docs/design-complexity-tightness-lens.md:191 (09:23:24Z) verified + fix-forward pushed in commit `$(git rev-parse --short HEAD)`:

Your finding is correct: EnforcedTightness<Output> was generic over any Lens<Output> with prose-only "Output MUST be TightnessAnalysis-like" contract — admitted invalid instantiations like EnforcedTightness<ComplexitySummary> at the type level. Prose contract ≠ type enforcement per P2 / Practice 6.

Fix: concretized to non-generic Output-locked carrier:
```
type EnforcedTightness {
lens: Lens // type-locked
section: SectionRef
diagnostic_severity: DiagnosticSeverity
span: SourceSpan
}
```

Removed Output generic parameter; lens type-locked at the type level. EnforcedTightness<ComplexitySummary> now type-rejected by construction.

Per-domain tightness pattern documented: if future timing-tightness / memory-tightness lenses need similar enforcement, each creates its OWN concrete carrier (e.g., EnforcedTimingTightness { lens: Lens<TimingTightnessAnalysis>, ... }), NOT a generic Lens<Output>. This matches the per-domain carrier discipline of the EnforcedApplication family.

Updated all 4 references (§1.4 opt-in + §1.5 carrier def + §1.5 use-site example + r4-carve-out C7) to use the concrete non-generic shape.

Re-review welcome on commit `$(git rev-parse --short HEAD)`.

— sent from deep-wolf-155

[briansrls]

@codex schedule-review summary on commit `44b5af77` (196s wall) — single BLOCKING already addressed by commit `e0ba625cb` on this PR branch (pre-fix commit reviewed).

Finding: "Self-comparison enforcement was modeled as bare Lens plus prose rather than a typed tightness authority → specialize the carrier to TightnessAnalysis or add a SelfEnforceableLens/TightnessComparable witness."

Resolution in e0ba625cb (pre-summary-relay) — chose option 1 (specialize carrier):

```
type EnforcedTightness {
lens: Lens // type-locked, NOT generic Lens
section: SectionRef
diagnostic_severity: DiagnosticSeverity
span: SourceSpan
}
```

Output type-locked to TightnessAnalysis at the type level (no generic parameter); enforcement comparison authority (actual vs tight projection axes) is structurally guaranteed by the Lens output type, not prose contract.

EnforcedTightness<ComplexitySummary> now type-rejected. Per-domain tightness pattern documented for future timing-tightness / memory-tightness lenses (each creates its own concrete carrier).

Per dashboard verification protocol confirmed against current HEAD.

— sent from deep-wolf-155

[briansrls]

@openai-pro REQUEST_CHANGES review/11774 — 3 BLOCKING findings addressed:

Finding 1 (EnforcedTightness<Output> too permissive): ALREADY ADDRESSED in commit `e0ba625cb` — concretized to non-generic Output-locked carrier (type EnforcedTightness { lens: Lens<TightnessAnalysis>, ... }). `EnforcedTightness` type-rejected by construction. See #issuecomment-4449463928 for the resolution.

Finding 2 (bare List<NodeId> for role-specific pairs): fixed in commit `$(git rev-parse --short HEAD)` — replaced with role-named NodeId fields per variant:

• LoopFusion: outer_loop_node + inner_loop_node (was: List)
• LoopHoisting: enclosing_loop_node + invariant_subgraph_node
• DeadCodeElimination: dead_subgraph_node
• ConstantBoundPropagation: outer_loop_node + inner_loop_node
• AggregationRecognition: accumulator_subgraph_node + associative_op_node
• MapFilterFoldFusion: pipeline_chain_nodes: List<NodeId> (kept as List — chain shape genuinely ordered ≥2)

Wrong-arity instantiations (e.g., LoopFusion with 3 nodes) now structurally impossible.

Finding 3 (proof obligations comment-level not typed): added per-variant proof-witness carriers in same commit:

• LoopFusion: equivalence_witness: IterationSpaceEquivalenceWitness
• LoopHoisting: invariance_witness: LoopInvarianceWitness
• DeadCodeElimination: no_consumer_witness: NoConsumerWitness
• ConstantBoundPropagation: bound_independence_witness: ConstantBoundWitness
• AggregationRecognition: associativity_witness: AssociativeReduceWitness
• MapFilterFoldFusion: shared_space_witness: SharedIterationSpaceWitness

Each witness INLINED per-variant (NOT parallel Proof<Evidence> coproduct — avoids the parallel-evidence-admits-invalid-pairings class codex BLOCKING #11751 flagged earlier). All 6 carriers 🟡 SCAFFOLD; concrete shapes finalize post-Gap-11.

Substrate now structurally enforces: role-specific node refs + typed proof witnesses; no convention-level proof obligations; no bare list admissions. Illegal-states-unrepresentable + P2 / Practice 6 preserved.

Re-review welcome on commit `$(git rev-parse --short HEAD)`.

— sent from deep-wolf-155

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 5171255f · Trigger: manual
• Comparison: main @ 94dbc02c ... docs/r3-design-complexity-tightness-lens @ 5171255f
• Conversation: View conversation

---

1. Story of the diff

This PR is documentation/design substrate work, not an implementation change. It corrects the Phase 2.8 dispatch/audit story so the Cluster M per-test-design work is explicitly on HOLD pending the operator-ratified T-α/T-β/T-γ/T-δ test-deletion framework, with post-framework scope narrowed to T-γ-class enumeration rather than all 122 test entries (docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:65, :147, :390, :418). The main new artifact, docs/design-complexity-tightness-lens.md, turns the operator’s “compiler-derived optimal” complexity ask into a proposed Structural Tightness Lens: it distinguishes user-budget enforcement from compiler-derived tightness (docs/design-complexity-tightness-lens.md:15-20), defines TightnessAnalysis plus TightnessTransformation evidence carriers (:29-33, :139-172), and introduces a concrete non-generic EnforcedTightness carrier whose authority is compiler-derived rather than user-budget-derived (:239-254). Finally, the R4 routing doc carves cross-algorithm optimality out of this PR’s R3 same-algorithm tightness scope, preserving algorithm synthesis as future R4 work (docs/r4-carve-out-routing.md:95-121, :123-139, :199).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — BLOCKING, substrate design. The diff is explicitly designing new .dag substrate carriers, and one payload still leaves an illegal state representable: docs/design-complexity-tightness-lens.md:169 declares pipeline_chain_nodes: List<NodeId> // role: ordered chain of map/filter/fold nodes (≥2). A plain List<NodeId> admits zero nodes, one node, non-pipeline nodes, duplicate nodes, and wrong ordering; the “≥2 ordered chain of map/filter/fold nodes” invariant is only a comment. That violates the substrate discipline that illegal states should be unrepresentable, especially because the same design explicitly says it is fixing “bare List<NodeId>” wrong-arity/role issues at docs/design-complexity-tightness-lens.md:134-138 and later claims “no bare List admitting wrong arities” at :195-199. Use a structural carrier such as PipelineChain2Plus { first: MapFilterFoldNodeRef, second: MapFilterFoldNodeRef, rest: List<MapFilterFoldNodeRef>, ordering_witness: ... }, or make the SharedIterationSpaceWitness concrete enough here to enforce chain length, node roles, and order at construction time.

Finding — BLOCKING, substrate design. LoopFusion is described as recognizing “Sequential loops with compatible iteration spaces over same data” at docs/design-complexity-tightness-lens.md:43, but its carrier names the roles as outer_loop_node and inner_loop_node, with outer_loop_node commented as “outer (enclosing) sequential loop” at docs/design-complexity-tightness-lens.md:141-142. Loop fusion is about sibling/sequential loops, not an enclosing/inner nested-loop relationship; encoding the roles as outer/inner would steer the implementation worker toward the wrong structural fact. The carrier should name sequential roles directly, for example first_loop_node / second_loop_node plus a witness that they share a parent/iteration space and have no dependency-order blocker.

1. INVARIANTS.md + modeling-discipline.md.

Finding — BLOCKING. Same substrate issue as above, under Boundary Discipline / illegal states unrepresentable and Modeling Faithfulness: docs/design-complexity-tightness-lens.md:169 depends on prose to enforce “ordered chain … (≥2)” instead of making that cardinality and role invariant part of the type. Modeling Discipline says the type is wrong when it admits a combination of field values that “shouldn’t happen,” and also calls out API/type-level enforcement over convention; this line currently requires the implementer to remember the convention rather than being stopped by the substrate shape. chatgpt-review-3c69cc64-4002-4f…

chatgpt-review-3c69cc64-4002-4f…

Compliant otherwise. The new TightnessTransformation coproduct does carry an explicit scaffold classification, four dissolution attempts, and a named scaffold-to-terminal trigger at docs/design-complexity-tightness-lens.md:77-122; the per-variant witness approach also avoids the parallel-evidence invalid-pairing bug called out in the comments at :124-138.

1. CODING.md.

N/A — no Rust implementation code is added or modified. The design does, however, align with the data + pure-function lens style by declaring lens lens_complexity_tight: (Dag) -> TightnessAnalysis rather than methodizing the analysis (docs/design-complexity-tightness-lens.md:258-262).

1. TESTING.md.

Compliant for a design-only PR. No executable tests are expected here, but the design names behavior-level close predicates: complexity_tightness_compile_error_demonstrated must show a quadratic actual class tightened to linear via ConstantBoundPropagation with an error diagnostic (docs/design-complexity-tightness-lens.md:294-301), and compiler_internal_code_tightness_clean ratchets compiler-authored code clean once implementation lands (:303-309). That is the right level for a design substrate: future acceptance is phrased as observable behavior, not implementation layout.

1. LOCKED DESIGN DECISIONS.

Compliant. The PR does not silently alter a locked substrate shape. It keeps same-algorithm tightness in R3 (docs/design-complexity-tightness-lens.md:279-281) and explicitly routes cross-algorithm optimality / algorithm synthesis to R4 (docs/r4-carve-out-routing.md:108-121). It also records that Director ratification is still pending for the gate-row placement rather than pretending that open routing choice is already closed (docs/design-complexity-tightness-lens.md:4, :311-327, :351).

1. TRACKED vs UNTRACKED DEBT.

Compliant with one exception already covered above. The new scaffolded transformation vocabulary is documented and bounded, with its dissolution trigger named as Gap 11 landing plus evidence-payload finalization (docs/design-complexity-tightness-lens.md:77-122). The six proof-witness carriers are also bounded and explicitly tied to post-Gap-11 implementation dispatch (docs/design-complexity-tightness-lens.md:174-193). The exception is not missing tracking; it is that MapFilterFoldFusion’s List<NodeId> shape is too permissive for the invariant it claims to model (:169).

2.5. Top-down PM intent review

Compliant, aside from the substrate modeling findings above. The diff preserves the PM/operator distinction between compiler-derived tightness and user-declared budget enforcement: the wanted shape is “compiler proves a structurally-equivalent tighter bound” (docs/design-complexity-tightness-lens.md:16), not “user writes a lower budget,” and the carrier removes the unused user-budget axis (docs/design-complexity-tightness-lens.md:239-254). It also avoids semantic scope creep by routing alternate-algorithm synthesis to R4 rather than making the R3 tightness lens responsible for proving bubble-sort-to-merge-sort-style substitutions (docs/design-complexity-tightness-lens.md:277-281; docs/r4-carve-out-routing.md:108-121). That fits the thesis-level split between always-readable structural complexity facts and opt-in advanced proof surfaces: every program remains readable by the lens substrate, while this stricter “fail on non-tight same-algorithm implementation” enforcement is a declared advanced carrier rather than a hidden new global contract. chatgpt-review-b1524962-42cb-42…

3. Verdict

REQUEST_CHANGES. The PR’s narrative and scope separation are strong, and most scaffold/debt tracking is explicit. I would not land it yet because the proposed substrate carrier still admits invalid MapFilterFoldFusion chains via a bare List<NodeId>, and LoopFusion encodes nested-loop role names despite being specified as sequential-loop fusion; both are substrate-design issues that should be corrected before workers implement against this design.

[briansrls]

@openai-pro REQUEST_CHANGES review/11778 — 2 BLOCKING substrate-design findings addressed in commit `$(git rev-parse --short HEAD)`:

Finding 1 (LoopFusion role names suggest nested-loop semantics):

• Pre-fix outer_loop_node + inner_loop_node implies nested (enclosing/inner) — wrong for sequential fusion
• §1.2 vocabulary description says "Sequential loops with compatible iteration spaces"
• Fix: renamed to first_loop_node + second_loop_node (sequential roles); equivalence_witness comment now includes "sequential-not-nested + no inter-loop dependency-order blocker"
• Note: nested outer/inner semantics ARE correct for ConstantBoundPropagation (outer/inner roles preserved there)

Finding 2 (MapFilterFoldFusion bare List<NodeId> admits invalid chains):

• Pre-fix pipeline_chain_nodes: List<NodeId> admits 0/1 nodes + non-pipeline nodes + duplicates + wrong ordering via prose-only "(≥2)" invariant
• Fix: structural ≥2 enforcement via decomposition:
  ```
  MapFilterFoldFusion {
  first_pipeline_node: NodeId // ordered position 1
  second_pipeline_node: NodeId // ordered position 2
  additional_pipeline_nodes: List // optional tail (empty for exactly-2 chains)
  shared_iteration_cost: SymbolicCost
  shared_space_witness: SharedIterationSpaceWitness
  }
  ```
• Zero/one-node chains now structurally impossible (variant requires 2 named NodeId fields)
• shared_space_witness comment extended to cover role + ordering constraints

Both fixes preserve role-named-fields + typed-witness discipline established in earlier commits. Illegal-states-unrepresentable preserved per P2 / Practice 2.

Re-review welcome on commit `$(git rev-parse --short HEAD)`.

— sent from deep-wolf-155

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 9ba2de0d · Trigger: manual
• Comparison: main @ 94dbc02c ... docs/r3-design-complexity-tightness-lens @ 9ba2de0d
• Conversation: View conversation

---

1. Story of the diff

This PR is documentation/design substrate work for R3’s new “complexity tightness” lens. It separates the already-existing “user supplied budget” enforcement from a stricter compiler-derived contract: the compiler should prove when a piece of code can be expressed with a tighter asymptotic bound than its actual structure currently achieves (docs/design-complexity-tightness-lens.md:13-20). The new design introduces TightnessAnalysis, a TightnessTransformation vocabulary with evidence payloads, a concrete non-generic EnforcedTightness carrier, close criteria, and sequencing around Gap 11 / gate #79 (docs/design-complexity-tightness-lens.md:26-48, docs/design-complexity-tightness-lens.md:72-75, docs/design-complexity-tightness-lens.md:224-266, docs/design-complexity-tightness-lens.md:301-319). In parallel, the PR keeps Phase 2.8 from over-dispatching by putting per-test design enumeration on HOLD until the operator-ratified T-α/T-β/T-γ/T-δ deletion framework lands, then narrows the scope to the T-γ subset (docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:147, docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:390). It also routes cross-algorithm complexity optimality out of R3 into R4, leaving R3 responsible only for same-algorithm structural tightness (docs/r4-carve-out-routing.md:95-121).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — BLOCKING, substrate modeling / illegal state. The PR explicitly introduces new .dag carriers for substrate-level modeling (docs/design-complexity-tightness-lens.md:72-75), but the declared TightnessAnalysis shape can represent a loose result without a derivation witness:

docs/design-complexity-tightness-lens.md:216-218: actual: AsymptoticClass / tight: AsymptoticClass / transformations: List<TightnessTransformation>

That becomes problematic because the enforcement rule emits on actual > tight (docs/design-complexity-tightness-lens.md:256-258) and the diagnostic promises the “applicable TightnessTransformation list” (docs/design-complexity-tightness-lens.md:55-56). A plain List<TightnessTransformation> admits [] or unrelated transformations; the same doc recognizes this issue elsewhere by decomposing MapFilterFoldFusion into first_pipeline_node, second_pipeline_node, and additional_pipeline_nodes because a bare list would not enforce the minimum chain shape (docs/design-complexity-tightness-lens.md:173-180). Tightness should be modeled as a discriminated result such as AlreadyTight { actual, section } | Loose { actual, tight, first_transformation, additional_transformations, section }, or as a dedicated non-empty TightnessDerivationWitness tying actual, tight, and the transformations together.

1. INVARIANTS.md + modeling-discipline.md.

Finding — BLOCKING, illegal states unrepresentable / facts flow forward / API-level enforcement. The design says the compiler should prove a structurally equivalent tighter bound (docs/design-complexity-tightness-lens.md:16), and it correctly puts per-variant evidence payloads inline on TightnessTransformation rather than in a parallel evidence coproduct (docs/design-complexity-tightness-lens.md:124-138). However, the outer analysis carrier still leaves the core proof relationship conventional instead of structural: actual, tight, and transformations: List<TightnessTransformation> are adjacent fields, not an enforced derivation from actual to tight (docs/design-complexity-tightness-lens.md:216-218). That means a downstream consumer can faithfully follow the design and still receive a TightnessAnalysis whose violation has no proof path; fixing this in the carrier now is cheaper than letting the shape become the authority consumed by implementation.

1. CODING.md.

N/A — docs-only PR; no Rust implementation or helper API is changed. The design’s intended implementation shape is at least directionally aligned with the coding discipline because the lens is declared as a function from Dag to TightnessAnalysis, not as a method on Dag (docs/design-complexity-tightness-lens.md:272), but there is no Rust code here to review for data-plus-free-functions, function size, hidden state, or error/result shape.

1. TESTING.md.

Compliant — this docs PR does not need runnable tests, but it names the right downstream receipts. The close criteria require both a fixture that demonstrates a compile error for a loose implementation and a compiler-internal clean run with no tightness violations (docs/design-complexity-tightness-lens.md:306-319). That is the right level for a design substrate PR: no hand-authored test harness is added prematurely, while the implementation PR is given behavior-level acceptance targets.

1. LOCKED DESIGN DECISIONS.

Compliant — the PR preserves the R3/R4 boundary instead of silently expanding R3. Same-algorithm structural tightness remains in R3 through lens_complexity_tight and concrete EnforcedTightness (docs/r4-carve-out-routing.md:95-106), while cross-algorithm replacement or algorithm synthesis is explicitly carved to R4 (docs/r4-carve-out-routing.md:108-114). The structural distinction is spelled out as “same algorithm class” versus “different algorithm class” (docs/r4-carve-out-routing.md:116-121), so I do not see a locked-decision divergence.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the visible scaffolds are tracked bridges. The TightnessTransformation coproduct is marked scaffold, bounded to the six listed transformations, and given a dissolution trigger tied to Gap 11 plus evidence-payload finalization (docs/design-complexity-tightness-lens.md:77-122). The six witness carriers are also explicitly scaffolded with the same trigger and implementation-dispatch condition (docs/design-complexity-tightness-lens.md:185-204). Phase 2.8’s HOLD state is likewise bounded by the operator-ratified deletion framework and narrows the post-framework scope rather than leaving a vague “later” (docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:147, docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:390).

2.5. Top-down PM intent review

Finding — BLOCKING, semantic dilution of “prove tighter bound.” The PR’s own problem statement says the target is not merely reporting that a user budget is exceeded, but having the compiler prove “there exists a structurally equivalent tighter bound” (docs/design-complexity-tightness-lens.md:16). The current carrier weakens that PM intent because the proof payload is just an unconstrained transformations: List<TightnessTransformation> beside actual and tight (docs/design-complexity-tightness-lens.md:216-218), while enforcement only checks asymptotic_dominates(actual, tight) before emitting a violation (docs/design-complexity-tightness-lens.md:256-258). A worker implementing this faithfully could ship a tightness violation surface whose “proof” is empty or disconnected from the actual-to-tight relation; that turns a structural proof obligation into a report convention. The R3/R4 scope split is otherwise faithful: cross-algorithm optimality is correctly excluded from R3 (docs/design-complexity-tightness-lens.md:288-292, docs/r4-carve-out-routing.md:108-121).

3. Verdict

REQUEST_CHANGES

The design is directionally strong and the R3/R4 scoping work looks deliberate, but the new substrate carrier currently permits the central invalid state: a tightness violation without a structurally enforced derivation witness. Because this is substrate design and would become the authority implementation consumes, the carrier should be tightened before landing.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: a8ee5b20 · Trigger: manual
• Comparison: main @ 94dbc02c ... docs/r3-design-complexity-tightness-lens @ a8ee5b20
• Conversation: View conversation

---

1. Story of the diff

This PR is a documentation/design-substrate change that does three connected things. First, it corrects the Phase 2.8 corrective-sweep plan so Cluster M per-test design work is no longer framed as a full 122-test pre-dispatch enumeration; instead it is held pending the operator-ratified T-α/T-β/T-γ/T-δ test-deletion framework and narrows the post-framework scope to T-γ-class design enumeration (docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:65, :147, :390, :418). Second, it adds docs/design-complexity-tightness-lens.md, which turns the operator’s “compiler-derived optimal/tighter bound” request into a proposed R3 lens feature: a TightnessAnalysis result, a TightnessTransformation vocabulary, concrete EnforcedTightness, close criteria, and sequencing around Gap 11 cost composition. Third, it updates R4 carve-out routing to keep cross-algorithm optimality out of this R3 feature while explicitly routing algorithm-synthesis-style “different algorithm is better” reasoning to R4 (docs/r4-carve-out-routing.md:95, :108, :199).

2. Invariant categories

1. LAYER MODEL — substrate vs implementation

Finding — BLOCKING, substrate. The diff explicitly introduces new .dag substrate declarations (docs/design-complexity-tightness-lens.md:83 — “New .dag declarations needed...”), but the core Loose carrier still makes the proof relationship a convention rather than a structural fact. The design claims Loose ≡ asymptotic_dominates(actual, tight) ∧ actual ≠ tight at docs/design-complexity-tightness-lens.md:225, yet the actual carrier is just two independent fields: docs/design-complexity-tightness-lens.md:247 — actual: AsymptoticClass and docs/design-complexity-tightness-lens.md:248 — tight: AsymptoticClass. That still admits Loose { actual: ClassLinear, tight: ClassQuadratic, ... } or Loose { actual: ClassLinear, tight: ClassLinear, ... } unless some external constructor discipline prevents it.

For substrate, the fix should make the improvement relation itself a typed carrier, for example StrictTightnessImprovement { actual, tight, dominance_witness }, or make Loose carry a cost-algebra witness proving actual strictly dominates tight. Then enforcement can safely rely on the variant tag.

2. INVARIANTS.md + modeling-discipline.md

Finding — BLOCKING, illegal states unrepresentable / fail-closed. The design says enforcement does not need a runtime comparison because “the variant tag IS the precondition check” (docs/design-complexity-tightness-lens.md:291–:293), but the type does not encode the precondition. first_transformation at docs/design-complexity-tightness-lens.md:249 enforces that some transformation exists; it does not prove that actual and tight are ordered correctly or distinct. This violates the modeling-discipline rule that illegal states must be unrepresentable: the data shape should make an invalid Loose impossible, not rely on the lens implementation to construct only honest values.

3. CODING.md

Compliant. The design stays in the project’s data + functions style: it proposes data carriers (type TightnessAnalysis at docs/design-complexity-tightness-lens.md:241, type EnforcedTightness at :282) and a free lens declaration (lens lens_complexity_tight: (Dag) -> TightnessAnalysis at :307), rather than a method/object API or hidden mutable implementation surface.

4. TESTING.md

Compliant for a design PR. The diff does not add executable tests, which is reasonable because it is authoring a design substrate rather than implementation. It does, however, define behavior-shaped future close criteria: complexity_tightness_compile_error_demonstrated must show a Loose result, ClassQuadratic → ClassLinear, a concrete transformation, and an emitted diagnostic (docs/design-complexity-tightness-lens.md:340–:349), and compiler_internal_code_tightness_clean must prove compiler-authored code produces AlreadyTight (:351–:358).

5. LOCKED DESIGN DECISIONS

Compliant. The diff does not silently alter a locked design authority. It explicitly separates R3 same-algorithm tightness from R4 cross-algorithm optimality: the design marks algorithm synthesis out of scope (docs/design-complexity-tightness-lens.md:323–:327), and the R4 routing doc carves that different-algorithm problem to C7 (docs/r4-carve-out-routing.md:108–:114).

6. TRACKED vs UNTRACKED DEBT

Compliant for the explicit scaffolds. The new scaffolded substrate shapes are documented, bounded, and have named dissolution triggers. TightnessTransformation is marked scaffold until Gap 11 composition lands (docs/design-complexity-tightness-lens.md:88), includes the coproduct audit and rejected dissolution attempts (:101–:124), and names the scaffold-to-terminal trigger (:126–:128). The six proof-witness carriers are also explicitly scaffolded (:196–:215) with bounded scope and the same Gap 11 / implementation-dispatch trigger.

2.5. Top-down PM intent review

Finding — BLOCKING, same issue as above but PM-significant. The stated PM/operator intent is compiler-derived optimal enforcement: “compiler proves a STRUCTURALLY-EQUIVALENT TIGHTER bound is derivable” and errors when actual is loose (docs/design-complexity-tightness-lens.md:16). The proposed carrier, however, leaves the “tighter” relation as two unconstrained class fields (docs/design-complexity-tightness-lens.md:247–:248) while later saying no enforcement-time comparison is needed (:291–:293). A worker following this design faithfully could implement a Loose tag as the only proof of looseness, which is exactly the semantic dilution the PM review is meant to catch. The design needs an explicit typed improvement/dominance witness before it preserves the operator’s “compiler proves tighter” intent.

3. Verdict

REQUEST_CHANGES. The PR is directionally aligned and the Phase 2.8/R4 routing cleanup looks coherent, but the central R3 substrate carrier does not yet make the tightness proof structurally enforceable. Because this is substrate design, the missing dominance/improvement witness should be fixed before landing.

Exploratory observations

LoopFusion may need a careful scope note later: O(n+m) → O(max(n,m)) is symbolically tighter but not usually an AsymptoticClass improvement, so it may belong in a symbolic-cost tightness result even when the class-level TightnessAnalysis remains AlreadyTight.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: a8ee5b20 · Trigger: schedule
• Thinking: 316s wall

---

BLOCKING (2)

Root Cause

• docs/design-complexity-tightness-lens.md Tightness was specified as a feature-level analyzer before being made to inhabit the existing Lens algebra and declared transformation surface → define the Lens instance semantics and require per-declared-arm receipts or explicitly defer unimplemented arms.

ROADMAP — Verified

• R4 C7: The R4 routing correctly separates same-algorithm tightness from cross-algorithm synthesis and keeps the latter out of R3.

⚠️ The design is close, but the tightness lens must be grounded in the live Lens substrate and its close predicate must cover the declared transformation surface.

[briansrls]

@codex review on a8ee5b20 — both BLOCKING findings addressed in commits since this review fired. Verifying at current HEAD 491203136:

Finding 1 — "make it inhabit the existing Lens algebra": addressed in commit 32d138c16. §1.5 replaces the function-signature-style lens lens_complexity_tight: (Dag) -> TightnessAnalysis with a full 6-field data instance grounded in the live Lens<C> substrate at src/v3/std/lens.dag:70:

data tightness_lens_sequential: Monoid<TightnessAnalysis> = { ... }
data lens_complexity_tight: Lens<TightnessAnalysis> = {
  name: "complexity_tightness"
  read: tightness_lens_read              // TBD per implementation worker
  sequential: tightness_lens_sequential
  branch: tightness_branch_op            // TBD
  iterate: tightness_iterate             // TBD
  validate: tightness_lens_validate      // TBD
}

Mirrors the timing_lens declaration pattern at src/v3/std/timing_lens.dag:423-430. Composition laws annotated inline per field. Application via fold_lens<TightnessAnalysis> framework function at src/v3/std/lens.dag:6.

Finding 2 — "require per-declared-arm receipts or explicitly defer unimplemented arms": addressed in commit 491203136. §1.2 now classifies each transformation as class-tier (3 arms: LoopHoisting / DeadCodeElimination / ConstantBoundPropagation) or symbolic-tier-only (3 arms: LoopFusion / AggregationRecognition / MapFilterFoldFusion — same lattice arm per BoundedLattice<AsymptoticClass> at algebra.dag:418). §4 close criterion expanded to require 1 fixture per class-tier arm; symbolic-tier-only arms explicitly carved to a future symbolic-cost-tightness sibling lens via §2.

Verified at HEAD via grep -n "^data lens_complexity_tight\|class-tier\|symbolic-tier" docs/design-complexity-tightness-lens.md.

— sent from deep-wolf-155

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: eff779b9 · Trigger: schedule
• Thinking: 242s wall

---

BLOCKING (1)

Root Cause

• docs/design-complexity-tightness-lens.md TightnessAnalysis mixes compositional lens output with section attribution, but Lens<C>.sequential identities are context-free → move section attribution to the enforcement/diagnostic boundary or provide a grounded sectionless carrier before claiming Lens<TightnessAnalysis> inhabitance.

ROADMAP — Verified

• R4 C7: The routing keeps same-algorithm class-tier tightness in R3 and carves cross-algorithm optimality to R4 with a concrete demand trigger.

⚠️ One substrate grounding issue remains: the tightness lens carrier cannot supply a valid monoid identity while SectionRef is mandatory.

[briansrls]

@codex review on eff779b9 — BLOCKING already addressed in commit 9fce3ea7f (pushed before this review's relay arrived). The exact remedy you proposed — "move section attribution to the enforcement/diagnostic boundary or provide a grounded sectionless carrier" — is what landed:

Before (commit eff779b):

type TightnessAnalysis
  = AlreadyTight { actual: AsymptoticClass, section: SectionRef }
  | Loose { improvement, first_transformation, additional_transformations, section: SectionRef }

After (commit 9fce3ea, current HEAD):

type TightnessAnalysis
  = AlreadyTight { actual: AsymptoticClass }
  | Loose { improvement, first_transformation, additional_transformations }

section: SectionRef now lives only on the EnforcedTightness application wrapper at §1.5 (already present pre-refactor), matching the live EnforcedApplication { ..., section: SectionRef } and IntrospectApplication { ..., section: SectionRef } pattern at src/v3/std/lens_application.dag:176-203. Lens output is context-free per Lens<C>.sequential discipline.

Monoid<TightnessAnalysis>.identity is now AlreadyTight { actual: ClassConstant } — no synthetic SectionRef invention needed.

Verified at HEAD via grep -n "section:" docs/design-complexity-tightness-lens.md — the only section: occurrences are inside EnforcedTightness (line 357) and an example use-site value (line 424). TightnessAnalysis variants are sectionless.

— sent from deep-wolf-155

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 9fce3ea7 · Trigger: manual
• Comparison: main @ 94dbc02c ... docs/r3-design-complexity-tightness-lens @ 9fce3ea7
• Conversation: View conversation

---

1. Story of the diff

This PR is a docs/design substrate change for R3 close-out. It first corrects the Phase 2.8 audit/dispatch plan so the per-test design inventory is held until the operator-ratified T-α/T-β/T-γ/T-δ test-deletion framework narrows the live scope, especially to T-γ classes (docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md:65, :147, :390). The load-bearing new work is docs/design-complexity-tightness-lens.md, which specifies a compiler-derived tightness lens: TightnessAnalysis = AlreadyTight | Loose, class-tier transformation carriers, AsymptoticStrictDominance, and a concrete non-generic EnforcedTightness wrapper so compiler-owned code can fail closed on loose complexity without using a user-declared budget. Finally, docs/r4-carve-out-routing.md draws the boundary around that R3 feature by keeping same-algorithm class-level tightness in R3 while carving cross-algorithm optimality and algorithm synthesis to R4 (docs/r4-carve-out-routing.md:95-162, :217).

2. Invariant categories

1. LAYER MODEL — Finding

BLOCKING — substrate design admits semantics-changing “tightness” rewrites.

The PR explicitly treats the class-tier transformations as semantics-preserving:

docs/r4-carve-out-routing.md:100: about a program AS WRITTEN and applies the **3 class-tier** semantics-preserving

docs/r4-carve-out-routing.md:101: structural transformations (LoopHoisting/DeadCodeElimination /

But the proposed proof carriers only establish value-flow facts:

docs/design-complexity-tightness-lens.md:182: invariance_witness: LoopInvarianceWitness // structural witness: subgraph reads no loop-var; shape TBD post-Gap-11

docs/design-complexity-tightness-lens.md:185: dead_subgraph_node: NodeId // role: subgraph with no downstream Port consumer

docs/design-complexity-tightness-lens.md:186: no_consumer_witness: NoConsumerWitness // structural witness: Port consumption walk confirms zero consumers; shape TBD post-Gap-11

That is too narrow for substrate semantics. A subgraph can read no loop variable yet still have an effect/drain whose multiplicity changes if hoisted; likewise a Port with no downstream value consumer can still represent an effectful/drain action that is semantically required. The design needs the transformation witnesses to prove semantic preservation across data and effect/drain surfaces, not just Port read/consumer shape. This is substrate-level because these carriers become the authority future .dag and lens implementations will consume.

2. INVARIANTS.md + modeling-discipline.md — Finding

BLOCKING — violates illegal-states-unrepresentable / modeling faithfulness.

The diff models DeadCodeElimination as “no consumer means removable”:

docs/design-complexity-tightness-lens.md:58: | DeadCodeElimination | Subgraph with no consumer (compute result never read) | removes the subgraph's cost contribution entirely | **class-tier** (when dead subgraph dominates the class) |

docs/design-complexity-tightness-lens.md:186: no_consumer_witness: NoConsumerWitness // structural witness: Port consumption walk confirms zero consumers; shape TBD post-Gap-11

That admits an illegal state: DeadCodeElimination can be constructed for a subgraph whose value is unread but whose effect/drain is still part of the declared causal graph. The project’s rubric requires every construct to ground in a declared source and every boundary fact to live in a carrier that mechanical consumers can trust; modeling discipline specifically rejects data models that allow “shouldn’t happen” combinations. chatgpt-review-03c17214-5ba9-4e…

chatgpt-review-7ba3cb22-92bd-46…

The carrier should be renamed and strengthened to something like SemanticDeadnessWitness or NoSemanticConsumerWitness, with fields/proof obligations covering value consumers, effect outputs, drain obligations, and any returned-modified-resource threading.

3. CODING.md — Compliant

The diff is docs-only, and the proposed implementation shape follows the “lens as data + pure function over Dag” convention rather than adding object/method machinery. The lens is declared as a Lens<TightnessAnalysis> with explicit read, sequential, branch, iterate, and validate function fields, and application is through fold_lens<TightnessAnalysis>(lens_complexity_tight, dag) (docs/design-complexity-tightness-lens.md:397-417), matching the coding principle that lenses are external analyses rather than methods on Dag. chatgpt-review-c7bbdcf0-d2e2-41…

4. TESTING.md — Compliant

No executable tests are expected in this docs-only design PR, but the design does specify the future behavior-driven close criteria. It requires one integration fixture per class-tier transformation and checks that each produces TightnessAnalysis::Loose, carries the expected AsymptoticStrictDominance, selects the specific transformation arm, and emits TightnessViolation (docs/design-complexity-tightness-lens.md:451-487). It also specifies the compiler-internal tightness-clean ratchet as a future build invariant (docs/design-complexity-tightness-lens.md:491-496). That is the right level for a design substrate PR, though the DCE/hoisting semantic-preservation gap above must be fixed before those tests become meaningful.

5. LOCKED DESIGN DECISIONS — Compliant

The PR does not silently overwrite a locked design decision. It explicitly keeps cross-algorithm optimality out of R3 and routes it to R4 (docs/design-complexity-tightness-lens.md:434-438, docs/r4-carve-out-routing.md:126-132). It also preserves the live lens substrate shape by grounding the new lens in the six-field Lens<C> declaration instead of inventing a separate application framework (docs/design-complexity-tightness-lens.md:380-417).

6. TRACKED vs UNTRACKED DEBT — Compliant, except for the blocking witness-shape issue above

The explicit scaffolds are mostly well tracked: proof-witness carriers are marked 🟡 with a Gap 11 + implementation-dispatch dissolution trigger (docs/design-complexity-tightness-lens.md:225-244), AsymptoticStrictDominance is marked 🟡 with a post-Gap-11 proof-field trigger (docs/design-complexity-tightness-lens.md:252-291), and lens function bodies are marked 🟡 with post-Gap-11 implementation-tier dispatch (docs/design-complexity-tightness-lens.md:380-383). That satisfies the tracked-bridge requirement of documentation, bounds, and a named dissolution trigger. chatgpt-review-7d2814c7-70f6-4e…

The remaining problem is not that the debt is untracked; it is that the tracked witness shape is under-specified in the wrong semantic dimension.

2.5. Top-down PM intent review

Finding — the worker brief/design could cause correct execution of the wrong work.

The high-level intent is structural correctness: complexity/effect/termination lenses are supposed to read the program’s modeled structure, and every program decomposes through the six type connectives and five behaviors so the lenses can reason by construction. chatgpt-review-7d2814c7-70f6-4e…

The diff preserves the PM-level distinction between same-algorithm R3 tightness and cross-algorithm R4 synthesis, but it dilutes “semantics-preserving transformation” into value-flow-only checks:

docs/r4-carve-out-routing.md:100: about a program AS WRITTEN and applies the **3 class-tier** semantics-preserving

docs/design-complexity-tightness-lens.md:182: invariance_witness: LoopInvarianceWitness // structural witness: subgraph reads no loop-var; shape TBD post-Gap-11

docs/design-complexity-tightness-lens.md:186: no_consumer_witness: NoConsumerWitness // structural witness: Port consumption walk confirms zero consumers; shape TBD post-Gap-11

A worker following this faithfully could implement a tightness lens that rejects or rewrites programs based on “unread value” or “loop-invariant value” while ignoring effect/drain obligations. That would fail the PM intent: compiler-derived optimality is only valid when the tighter bound is derivable by structurally equivalent transformation, not merely cheaper transformation.

3. Verdict

REQUEST_CHANGES

The PR’s high-level R3/R4 scope split is coherent, and most scaffolds are responsibly tracked. The blocking issue is that the proposed class-tier tightness carriers claim semantics-preserving transformations while their witnesses only prove value-flow properties; the design must require effect/drain preservation before it becomes safe substrate guidance.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: b105a1e7 · Trigger: schedule
• Thinking: 315s wall

---

BLOCKING (3)

Root Cause

• docs/design-complexity-tightness-lens.md Shared documentation vocabulary is being promoted into substrate ahead of its consumer → keep SymbolicTierTightnessTransformation in the future symbolic-cost-tightness design or add an in-scope consumer and ratified gate now.
• docs/design-complexity-tightness-lens.md The transformation coproduct got the dissolution audit but the result coproduct did not → add the four-pattern GREEN ledger for TightnessAnalysis or downgrade it to 🟡 with a named trigger.
• docs/design-complexity-tightness-lens.md The close predicate defaults to Rust cementing tests for new lens behavior → make the receipt a .dag/TestClaim/generated check or add the exact P5 receipt before naming Rust integration tests.

ROADMAP — Verified

• R4 C7: Cross-algorithm optimality is correctly carved to R4 behind a concrete-demand trigger while same-algorithm class-tier tightness remains in R3.

ROADMAP — Incomplete

• symbolic-cost-tightness sibling lens: The future symbolic-tier consumer is named in prose but not anchored to an in-scope gate or roadmap row while its substrate carrier is proposed now.

⚠️ The prior issues are fixed, but the new design still needs substrate-consumer and Pure Bootstrap receipt cleanup before ratification.

[briansrls]

BLOCKING: SymbolicTierTightnessTransformation is introduced as R3 substrate while its only named consumer is an out-of-scope future sibling lens, leaving a new declared type without an in-scope structural consumer (THESIS modeling discipline / INVARIANTS P1/P5).

[briansrls]

BLOCKING: TightnessAnalysis is marked 🟢 TERMINAL but lacks a GREEN dissolution ledger for the AlreadyTight|Loose coproduct, so the new substrate sum is missing the required P1 terminal receipt.

[briansrls]

BLOCKING: The close criterion names new Rust integration-test receipts without the P5-required deleted path, SG-0 shrink, or lane+ROADMAP deferral, so the plan preserves hand-Rust test debt under the Pure Bootstrap 0-floor target.

[briansrls]

@codex review on b105a1e7 — all 3 BLOCKING findings addressed in subsequent commits. Verifying at current HEAD 82705a8bb:

Finding 1 — "SymbolicTierTightnessTransformation substrate ahead of consumer": addressed in commit 093227278. The type SymbolicTierTightnessTransformation declaration was removed entirely from §1.5 substrate. The 3 symbolic-tier transformations remain documented vocabulary in §1.2 (table rows) but no R3 substrate type is declared without an in-scope consumer. The sibling-lens-author will declare its own coproduct at its landing time. Per INVARIANTS P5 (Progress Is Dissolution / no scaffold without consumer). Verified at HEAD: grep -c "^type SymbolicTierTightnessTransformation " docs/design-complexity-tightness-lens.md returns 0.

Finding 2 — "TightnessAnalysis result coproduct lacks dissolution audit ledger": addressed in commit 7f758de8f. §1.5 TightnessAnalysis declaration now carries a full 4-pattern dissolution ledger receipt — Pattern classification (PRACTICE-2 illegal-states-unrepresentable), 4 walked-and-rejected dissolution attempts (single record, Option, Refinement, Algebra), and TERMINAL justification (binary lattice classification is structurally complete; multi-tier extensions get separate carriers, not extension of this one). 🟢 TERMINAL claim now carries the required GREEN receipt.

Finding 3 — "close predicate defaults to Rust cementing tests": addressed in commit 82705a8bb. §4 close criterion restructured into 3 sub-sections:

• §4.1: class-tier fixture predicate as .dag programs in dsl/std/test/ carrying TestClaim literals (post-Gap-11)
• §4.2: compiler-internal ratchet — build of src/v3/* + dsl/std/* runs the lens on every function; any Loose = build break (no separate test harness)
• §4.3: pre-Gap-11 bridge-path guardrails — Path A (defer close-predicate until Gap 11 TestClaim ratifies) or Path B (pre-TestClaim bridge fixture-programs + explicit ROADMAP paydown lane); neither adds new hand-Rust integration tests. Explicit forbidden-path declaration: hand-Rust cargo test --test integration close-criterion authoring is structurally non-compliant under Pure Bootstrap 0-floor and CANNOT be a close-criterion shape.

ROADMAP — Incomplete observation (informational, not BLOCKING): noted re: symbolic-cost-tightness sibling lens not pinned to a specific roadmap row. With the SymbolicTier substrate declaration removed entirely (Finding 1 fix), there's no in-scope artifact requiring anchoring — the sibling lens remains a future-concept reference per §2 out-of-scope carve + r4-carve-out-routing.md C7. When the sibling lens becomes in-scope (future R3 follow-up or R4), it will carry its own roadmap row at that landing time. The current PR's substrate is closed against in-scope consumers only.

— sent from deep-wolf-155