diff --git a/docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md b/docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md
index 0e251d7c37d..9f6df1935e8 100644
--- a/docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md
+++ b/docs/audit/r3-phase2-corrective-sweep-dispatch-plan-2026-05-14.md
@@ -62,7 +62,7 @@ graph TD
end
subgraph "Phase 2.8 — Cluster M per-test design (Mgr-tier)"
- P28[2.8 Per-test inventory pre-dispatch
122 TEST entries]
+ P28[2.8 Per-test design pre-dispatch
HOLD pending T-α/β/γ/δ framework
scope: T-γ-class only ~2-4 docs]
end
subgraph "Phase 2.7 — Root-cause systemic fix"
@@ -144,7 +144,7 @@ This is the discipline §5.2 will codify. By applying it to Phase 2 itself, we v
5. **Fifth (Phase 2.5)**: Gap 9 canvas authoring (parallel-eligible)
6. **Sixth (Phase 2.3)**: Track A reclassification (after 2.1 + 2.2)
7. **Seventh (Phase 2.6)**: Cluster F Phase 2 coord (parallel-eligible)
-8. **Eighth (Phase 2.8)**: Cluster M Phase 3 per-test design enumeration (parallel-eligible; blocks Cluster M Phase 3 worker dispatch downstream)
+8. **Eighth (Phase 2.8)**: Cluster M Phase 3 per-test design enumeration — **HOLD pending operator-ratified test-deletion framework T-α/T-β/T-γ/T-δ** per Director msg_92b03a78; post-framework scope is per-T-γ-class enumeration only (~2-4 docs); blocks Cluster M Phase 3 worker dispatch on T-γ classes downstream
9. **Ninth (Phase 2.7)**: §5.2 process discipline (synthesis; last; consumes evidence from 2.1-2.8)
Director-tier ratify + admin-merge per operator broad-authorization on each PR open.
@@ -385,9 +385,9 @@ This section audits whether every file currently in `EXPECTED_HAND_AUTHORED_NON_
| **Class-level design only** (per-test inventory deferred to "mid-flight") | 122 | All 122 TEST entries route through Cluster M Phase 3 Coordinator framework with 6 class stubs: cementing-test (~20-25) / reflected-Dag (~25-30) / generic-DimReport (~20-25) / boundary (~10) / R1C-D-E (~3) / L4-L7-L5 (~5). Each class has a worker brief (some STUB, some DIRECTOR-SCAFFOLD); **per-test inventory + pilot/bulk split is filled in at Phase 3 dispatch time, NOT pre-dispatch.** ⚠ |
| Per-test design citation | 0 | Per the Coordinator brief §2: *"Each class is a parallel-dispatchable worker batch. Coordinator finalizes the class stubs as Phase 3 begins"* — by design, per-test mapping is mid-flight, not pre-flight. |
-**Gap**: 122 TEST entries have CLASS-level design but no per-test design at dispatch-readiness. Per operator discipline ("no worker starts without design ready"), the Cluster M Coordinator's "finalize-at-dispatch" pattern is NOT compliant — needs pre-dispatch per-test inventory authoring.
+**Gap**: 122 TEST entries have CLASS-level design but no per-test design at dispatch-readiness. Per operator discipline ("no worker starts without design ready"), the Cluster M Coordinator's "finalize-at-dispatch" pattern is NOT compliant — needs pre-dispatch per-test design authoring per the ratified subset.
-**Recommended remediation**: new phase (Phase 2.8 — Cluster M Phase 3 per-test design enumeration) before Cluster M Phase 3 worker dispatch begins. Coordinator authors per-test inventory + pilot/bulk split as static pre-dispatch artifact, NOT mid-flight finalization.
+**Recommended remediation** (revised per Director msg_92b03a78 framework-coordination directive 2026-05-14): Phase 2.8 was originally scoped to "static per-test inventory for all 122 entries" but is now **HOLD pending operator-ratified test-deletion framework T-α/T-β/T-γ/T-δ**. Director's testgen-subsumption framing reduces per-test L2.5 scope from ~13 docs → ~2-4 docs (only T-γ classes that aren't testgen-subsumable). Per §1 Phase 2.8 row at line 36: post-framework-ratification, Phase 2.8 deliverable is **per-T-γ-class enumeration only** (NOT all 6 classes; testgen-subsumable classes don't need per-test L2.5), scope ~2-4 docs aligned with the test-deletion framework's substrate-prereq mapping. PM premature-dispatch corrected via msg_77355877 (tidy-ram-467 not blocked on the original 122-entry inventory).
### §9.3 Per-stage L2.5 domain-model authoring status
@@ -415,7 +415,7 @@ This section audits whether every file currently in `EXPECTED_HAND_AUTHORED_NON_
| Gap | Files affected | Remediation | In Phase 2? |
|---|---|---|---|
| **NON_TEST (b)-class generic §1.1 prereq** instead of specific PB-X lane | ~25-30 NON_TEST entries (bootstrap/regen cluster) | **Phase 2.3** (Track A reclassification) | ✓ COVERED |
-| **TEST entries with class-level design only** (per-test inventory mid-flight) | 122 TEST entries | **NEW: Phase 2.8** — Cluster M Phase 3 per-test design enumeration pre-dispatch | ✗ GAP — need new Phase |
+| **TEST entries with class-level design only** (per-test inventory mid-flight) | 122 TEST entries (subset: T-γ-class only post-framework) | **Phase 2.8** — Cluster M Phase 3 per-test design enumeration **HOLD pending operator-ratified test-deletion framework T-α/T-β/T-γ/T-δ** (Director msg_92b03a78 testgen-subsumption framing reduces scope to per-T-γ-class enumeration ~2-4 docs) | ✓ COVERED via Phase 2.8 (scope-corrected) |
| **L2.5 per-stage models NOT authored** for 7 of 9 PB-X lanes | All pipeline-stage + adjacent retirement work | **Per-lane L2.5 authoring stream** — Director (PB-6 in flight) + warm-wolf-698 expanded scope (PB-Substrate / PB-Bootstrap-Process / PB-Runtime / PB-Lib+PB-Build) | ✗ GAP — parallel workstream, NOT in Phase 2 sweep |
### §9.5 Pre-dispatch authority-gate (recommended Phase 2.7 §5.2 codification)
diff --git a/docs/design-complexity-tightness-lens.md b/docs/design-complexity-tightness-lens.md
new file mode 100644
index 00000000000..1d12f064ca7
--- /dev/null
+++ b/docs/design-complexity-tightness-lens.md
@@ -0,0 +1,593 @@
+---
+status: PM-authored design substrate (deep-wolf-155)
+authority_parent: Operator briansrls 2026-05-14 ratification — "compiler-derived-optimal enforcement, not user-budget enforcement" + IN-R3 scope-expansion ratified via AskUserQuestion
+director_ratification: PENDING (gate-row shape: sub-promise under #79 OR new §1.8 row)
+authoring_date: 2026-05-14
+prereq_gates: §1.8 #79 complexity_lens_behaviorally_complete + close-plan Gap 11 LogCost/ProductCost/SumCost composition
+---
+
+# Design — Complexity Tightness Lens
+
+## §0. Operator framing
+
+Operator 2026-05-14 distinguished two complexity-checking shapes:
+
+1. **User-budget enforcement (current)**: User declares budget intent ("≤ ClassLinear"); compiler observes actual; errors if actual exceeds declared budget. Current `EnforcedApplication` shape.
+2. **Compiler-derived-optimal enforcement (wanted)**: User writes code with no budget (or any budget); compiler proves a STRUCTURALLY-EQUIVALENT TIGHTER bound is derivable via semantics-preserving transformations; errors if actual is loose against the derivable tight bound.
+
+Operator quote (paraphrased): "what i wanted was — 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.'"
+
+This doc specifies the compiler-derived-optimal shape as a NEW lens-tier feature: **Structural Tightness Lens**.
+
+## §1. Feature spec
+
+### §1.1 Lens output
+
+For any program scope (function body / region / module), the tightness lens produces a discriminated result — the variant tag + named improvement witness IS the proof relationship (no two-adjacent-class-fields shape):
+
+```
+data TightnessAnalysis
+ = AlreadyTight {
+ actual: AsymptoticClass, // = tight by construction; no derivation needed
+ }
+ | Loose {
+ improvement: AsymptoticStrictDominance, // named improvement witness: dominator strictly dominates dominated (see §1.5)
+ first_transformation: ClassTierTightnessTransformation, // ≥1 enforced structurally (no empty/disconnected derivation); class-tier-only by type
+ additional_transformations: List, // optional ordered tail; class-tier-only by type
+ }
+```
+
+**Section context is application-level, not lens-output level** (per briansrls INLINE BLOCKING PR #3067 2026-05-14 at line 384): previous shape carried `section: SectionRef` inside each variant, which forced the `Monoid` identity to invent a synthetic `` — `SectionRef` has only `DeclarationScope { declaration: ... }` and `NodeScope { declaration: ..., node: ... }` variants at `src/v3/std/lens_application.dag:66-68`, no empty value. Fix: section moves to the application wrapper (`EnforcedTightness.section` at §1.5 — already present), matching the live `EnforcedApplication { ..., section: SectionRef }` and `IntrospectApplication { ..., section: SectionRef }` pattern at `src/v3/std/lens_application.dag:176-203`. The lens output (`TightnessAnalysis`) carries only the tightness conclusion; the section context comes from the EnforcedTightness/future-IntrospectTightness wrapper.
+
+The discrimination + improvement witness encodes the Loose-vs-AlreadyTight precondition into the type:
+- `AlreadyTight` cannot carry a transformation (no field exists) — no spurious derivation.
+- `Loose` cannot exist without ≥1 transformation (`first_transformation` is non-optional) — no empty derivation.
+- `Loose` cannot exist without a named `AsymptoticStrictDominance` improvement witness — the relation `actual > tight ∧ actual ≠ tight` is a named-carrier obligation, not two adjacent fields that admit `(ClassLinear, ClassLinear)` or `(ClassLinear, ClassQuadratic)` inversions.
+
+The four illegal states `actual == tight ∧ transformations non-empty`, `actual > tight ∧ transformations empty`, `actual == tight ∧ Loose tag`, and `actual < tight ∧ Loose tag` are blocked at the carrier level — three by the discriminated-sum + ≥1-transformation enforcement (no implementation discretion possible), and the inverted/equal-pair cases via the named `AsymptoticStrictDominance` carrier. **Substrate-honesty qualifier (per cursor APPROVE_WITH_COMMENTS PR #3067 2026-05-14)**: `AsymptoticStrictDominance` is 🟡 SCAFFOLD per Gap 11 trigger (see §1.5) — its `dominator ≠ dominated ∧ asymptotic_dominates(dominator, dominated)` invariant is currently held by lens-side construction discipline (Practice 6 API enforcement) until Gap 11 finalizes the strict-dominance proof witness shape. The named-carrier-vs-adjacent-fields step IS the type-level move; full Practice-2 ("structurally impossible") for the inverted/equal-pair cases is achieved when AsymptoticStrictDominance becomes 🟢 TERMINAL post-Gap-11.
+
+### §1.2 Transformation vocabulary
+
+The §1.5 substrate models the patterns as two type-level-distinct coproducts (`ClassTierTightnessTransformation` + `SymbolicTierTightnessTransformation` — see §1.5 declarations). The table below enumerates the shared documentation-level vocabulary; the types are split so each lens's `Loose.first_transformation` field structurally cannot carry a wrong-tier variant:
+
+Per-transformation tier classification (class-tier vs symbolic-tier-only) — class-tier transformations can produce an `AsymptoticStrictDominance` improvement at the lattice level; symbolic-tier-only transformations tighten the symbolic cost expression but keep the same class:
+
+| Transformation | Pattern recognized | Tightening | Tier |
+|---|---|---|---|
+| `LoopHoisting` | Computation inside loop independent of loop variable | O(n*m) → O(n+m) when inner cost is non-constant | **class-tier** (e.g., n,m both ClassLinear: ClassPolynomial(2) → ClassLinear) |
+| `DeadCodeElimination` | Subgraph with **no semantic consumer** (no value, effect, drain, or returned-modified-resource downstream — see `SemanticDeadnessWitness` in §1.5) | removes the subgraph's cost contribution entirely | **class-tier** (when dead subgraph dominates the class) |
+| `ConstantBoundPropagation` | Inner-loop bound provably independent of outer-loop variable | O(n*m) → O(n) when m proved constant | **class-tier** (ClassPolynomial(2) → ClassLinear) |
+| `LoopFusion` | Sequential loops with compatible iteration spaces over same data | O(n+m) → O(max(n,m)) when iteration spaces identical | **symbolic-tier only** (`n+m` and `max(n,m)` are same class; ClassLinear → ClassLinear in BoundedLattice) |
+| `AggregationRecognition` | Explicit accumulator with associative-reduce shape | substrate-folded to declarative `sum`/`fold` op | **symbolic-tier only** (pattern recognition; folding to declarative form does not change the lattice class) |
+| `MapFilterFoldFusion` | Chained collection ops sharing iteration space | O(n)+O(n)+O(n) → O(n) single-pass | **symbolic-tier only** (all chain elements + fused result are same class; ClassLinear → ClassLinear in BoundedLattice) |
+
+The vocabulary is shared across the lens family. This lens (class-level `lens_complexity_tight` producing `TightnessAnalysis` per §1.5) emits `Loose` only when an `AsymptoticStrictDominance` improvement is derivable — restricting to the 3 class-tier transformations above. The 3 symbolic-tier-only transformations are deferred to a future symbolic-cost-tightness sibling lens (per §2 out-of-scope carve), which produces `Loose` for same-class symbolic tightening that the class-level lens correctly reports as `AlreadyTight`.
+
+**Per openai-pro BLOCKING PR #3067 #11790 2026-05-14**: original 6-row table without tier classification admitted the design tension where `Loose.first_transformation` could carry a symbolic-tier-only variant. **Per codex BLOCKING PR #3067 #11795 2026-05-14**: original tier-by-implementation-discipline was insufficient — must be type-level enforced. Fix: §1.5 substrate splits `TightnessTransformation` into `ClassTierTightnessTransformation` (3 arms: LoopHoisting / DeadCodeElimination / ConstantBoundPropagation) and `SymbolicTierTightnessTransformation` (3 arms: LoopFusion / AggregationRecognition / MapFilterFoldFusion). The class-level `Loose.first_transformation` field is typed `ClassTierTightnessTransformation` — symbolic-tier variants are structurally non-instantiable at the type level (Practice 2 / modeling-discipline). The vocabulary in this table is shared at the documentation tier across the lens family; the types are split at the substrate tier.
+
+### §1.3 Diagnostic
+
+When the lens produces a `Loose` variant (variant tag + `improvement: AsymptoticStrictDominance` witness IS the precondition check — no runtime `actual > tight` comparison; structurally enforced via the discriminated TightnessAnalysis at §1.1):
+
+```
+TightnessViolation: code as written is {loose.improvement.dominator} but
+structurally-derivable tight bound is {loose.improvement.dominated}.
+Applicable transformations:
+ [{loose.first_transformation}, ...loose.additional_transformations].
+ --> {span_at_the_loose_region}
+```
+
+`AlreadyTight` variants emit no diagnostic — structurally cannot enter the violation path.
+
+- **Severity**: `Error` (always-on for compiler-internal; per-`EnforcedTightness` declared for user programs)
+- **Layer-1 kind label**: `TightnessViolation` (new diagnostic class)
+- **Span**: points at the loose region of code (the function or sub-expression where the transformation would apply)
+
+### §1.4 Enforcement tiers (operator-ratified 2026-05-14)
+
+**Compiler-internal code** (`src/v3/*`, `dsl/std/*`): **always-on**. Every compiler-authored function ratchet-checks tightness as part of build. Any tightness violation is a build-break. This is the SELF_HOSTING.md "compiler is canonical example" framing made operational — the compiler's own code is the most-aggressively-checked codebase in the project.
+
+**User programs**: opt-in via `EnforcedTightness` data declaration (CONCRETE non-generic carrier; Output type-locked to `TightnessAnalysis` per codex BLOCKING PR #3067 2026-05-14 — see §1.5 for the carrier shape + example use-site at §1.5 instantiation block). Backwards-compatible with existing programs; users opt their functions in as they're ready.
+
+### §1.5 Substrate carriers
+
+New `.dag` declarations needed (grounded against existing lens-application substrate at `src/v3/std/lens_application.dag:176-182`; `EnforcedTightness` is intentionally a structurally distinct 1-param self-comparison carrier, not a mirror of `EnforcedApplication`'s 3-param user-budget shape):
+
+```
+// In src/v3/std/complexity_tightness.dag (or analogous):
+
+// 🟡 SCAFFOLD until Gap 11 LogCost/ProductCost/SumCost composition lands.
+//
+// Coproduct classification per `feedback_coproduct_dissolution` 4-pattern audit
+// (addresses openai-pro BLOCKING PR #3067 2026-05-14 — modeling-discipline
+// requirement that new N≥2 coproducts carry classification + dissolution-attempt
+// record + named SCAFFOLD trigger):
+//
+// **Pattern**: STRUCTURE — variants are different structural shapes of the same
+// role ("semantics-preserving transformations the lens recognizes in the DAG to
+// derive a tighter bound"). Each variant identifies a distinct structural
+// pattern (sequential-loop / loop-invariant-subgraph / dead-subgraph /
+// constant-bound-inner-loop / associative-reduce / chained-collection-ops).
+//
+// **4 dissolution attempts walked-and-rejected before settling on this coproduct**:
+//
+// Attempt 1 — single `Transformation` type with `String` label: REJECTED per
+// INVARIANTS.md P1 (Modeling Faithfulness). A string label is not structural;
+// downstream consumers cannot programmatically verify which transformation
+// applies. Same class as `feedback_opaque_strings_attract_heuristics`.
+//
+// Attempt 2 — Refinement-class hierarchy (`Transformation` refines into named
+// subtypes): REJECTED — transformations don't have a refinement relation.
+// LoopFusion is not a refinement of LoopHoisting (they're parallel structural
+// patterns over disjoint DAG shapes, not subtype-shaped).
+//
+// Attempt 3 — Algebra (sum of primitive operations on DAG): REJECTED —
+// transformations aren't algebraically composable in a meaningful sense.
+// LoopFusion + LoopHoisting is not a sum-shaped algebraic operation;
+// the variants are parallel-applicable choices over distinct structural
+// patterns, not summands of a primitive-operation algebra.
+//
+// Attempt 4 — Parametric `Refinement`: REJECTED — per-variant
+// evidence payload differs structurally (LoopFusion needs
+// IterationSpaceEquivalence with 2 spaces; LoopHoisting needs
+// LoopInvariance with variable-independence facts; DeadCodeElimination
+// needs NoConsumer with port-consumption facts; etc.). Cannot be a uniform
+// parametric refinement; the evidence shape IS the variant discriminator.
+//
+// **Named SCAFFOLD-→-TERMINAL trigger**: Gap 11 LogCost/ProductCost/SumCost
+// composition lands AND per-variant evidence-payload fields finalize against
+// the composition algebra. At that point: revisit + upgrade to 🟢 TERMINAL.
+// If during finalization the structural pattern reveals additional variants
+// (e.g., AssociativeCommutativeFold as a sibling of AggregationRecognition,
+// or LoopSwap as a sibling of LoopFusion), they enter as new arms per the
+// same Structure-pattern discrimination — coproduct stays open to new
+// structural-pattern variants discovered post-Gap-11.
+//
+// Per-variant evidence-payload INLINED into each variant arm (NOT a parallel
+// TransformationEvidence coproduct, per codex BLOCKING #11751 PR #3067 2026-05-14:
+// parallel coproducts admit invalid pairings — e.g., LoopFusion arm could pair
+// with NoConsumer evidence). Inlining makes the pairing type-enforced.
+//
+// All variant payloads cite LIVE substrate types per `feedback_corrections_must_grep_verify_source`
+// (codex BLOCKING #11751 PR #3067 2026-05-14):
+// - `SymbolicCost` per `src/v3/std/algebra.dag:190` (NOT `SymbolicCostExpr` — non-live)
+// - `NodeId` per `src/v3/std/substrate.dag:5` (NOT `NodeRef` — non-live)
+// - `SizeVariable` per existing T-CostLens substrate (cited in close-plan §1.8 row #80)
+// Per openai-pro BLOCKING PR #3067 2026-05-14: bare `List` for
+// role-specific node-pairs was too loose (admitted wrong-arity/role
+// instantiations); proof obligations stated in comments were not type-enforced.
+// Fix: role-specific named NodeId fields (NOT bare List) + typed
+// proof-witness carriers (one per variant, NOT a parallel coproduct).
+
+// Per codex BLOCKING PR #3067 #11795 2026-05-14: original single
+// `TightnessTransformation` coproduct admitted `Loose.first_transformation`
+// pairing with the 3 symbolic-tier-only variants (LoopFusion /
+// AggregationRecognition / MapFilterFoldFusion). The §1.2 tier classification
+// described the constraint, but it was only Practice-6 API enforcement
+// (lens-implementation construction discipline), not Practice-2 structural
+// enforcement. Fix: split the coproduct into TWO TYPE-LEVEL DISTINCT
+// coproducts so the class-level lens cannot accept a symbolic-tier variant
+// at the type level. The class-level Loose carrier references
+// `ClassTierTightnessTransformation` (3 arms); the future symbolic-cost-
+// tightness sibling lens (per §2 out-of-scope carve) will reference
+// `SymbolicTierTightnessTransformation` (3 arms). No common parent type —
+// vocabulary is shared at the §1.2 documentation level, not the type-system
+// level, because the two lenses' Loose variants are structurally different.
+
+type ClassTierTightnessTransformation // produces AsymptoticStrictDominance in BoundedLattice
+ = LoopHoisting {
+ enclosing_loop_node: NodeId // role: outer loop containing the invariant subgraph
+ invariant_subgraph_node: NodeId // role: subgraph proved loop-invariant
+ independent_size_variables: List // size-vars proved independent of loop var
+ // Strengthened witness obligation per openai-pro BLOCKING PR #3067 2026-05-14:
+ // hoisting must preserve semantics across value-flow AND effect-flow AND
+ // drain-flow. A subgraph that reads no loop variable can still carry a
+ // WorkflowEffect (src/v3/std/effects.dag) whose multiplicity changes if
+ // hoisted out of the loop (runs once vs N times — different program semantics).
+ semantic_invariance_witness: LoopSemanticInvarianceWitness // structural witness: subgraph has (a) no loop-var value dependency AND (b) no effect/drain whose multiplicity matters AND (c) no returned-modified-resource dependency on iteration; shape TBD post-Gap-11
+ }
+ | DeadCodeElimination {
+ dead_subgraph_node: NodeId // role: subgraph with no downstream value/effect/drain consumer
+ // Strengthened witness obligation per openai-pro BLOCKING PR #3067 2026-05-14:
+ // "no value consumer" alone admits illegal removal. A Port with no downstream
+ // VALUE consumer can still carry a WorkflowEffect (src/v3/std/effects.dag) or
+ // a drain obligation that is semantically required. Witness must prove
+ // semantic deadness (no value AND no effect/drain AND no returned-modified-
+ // resource consumer) — not just value-flow deadness. Renamed from
+ // NoConsumerWitness → SemanticDeadnessWitness.
+ semantic_deadness_witness: SemanticDeadnessWitness // structural witness: subgraph has zero value consumers AND zero effect-output consumers AND zero drain obligations AND zero returned-modified-resource threading; shape TBD post-Gap-11
+ }
+ | ConstantBoundPropagation {
+ outer_loop_node: NodeId // role: outer loop over variable size
+ inner_loop_node: NodeId // role: inner loop with constant-bound
+ inner_bound: SymbolicCost // proved variable-independent of outer-loop SizeVariable
+ // Strengthened witness obligation per openai-pro BLOCKING PR #3067 2026-05-14:
+ // bound-independence must cover both SymbolicCost (value-axis) AND the
+ // inner-loop's effect/drain multiplicity (a constant-bounded loop runs a
+ // constant number of times — semantics are preserved as long as the inner
+ // loop's effect/drain doesn't depend on the outer iteration).
+ bound_independence_witness: ConstantBoundSemanticWitness // structural witness: inner_bound has no SymbolicCost dependency on outer SizeVariable AND inner-loop effect/drain has no causality on outer iteration index; shape TBD post-Gap-11
+ }
+
+type SymbolicTierTightnessTransformation // produces same-class symbolic-cost tightening; future symbolic-cost-tightness sibling lens carrier
+ = LoopFusion {
+ // Loop fusion = SIBLING/SEQUENTIAL loops with compatible iteration spaces
+ // (NOT outer/inner nested-loop relationship — that's ConstantBoundPropagation's
+ // shape). Per openai-pro BLOCKING PR #3067 2026-05-14: outer/inner naming
+ // misled toward nested-loop semantics; corrected to sequential first/second.
+ first_loop_node: NodeId // role: first sequential loop in fusion sequence
+ second_loop_node: NodeId // role: second sequential loop (compatible iteration space)
+ space_a: SymbolicCost // first-loop iteration-space cost expression
+ space_b: SymbolicCost // second-loop iteration-space cost expression
+ equivalence_witness: IterationSpaceEquivalenceWitness // structural witness: space_a ≡ space_b + sequential-not-nested + no inter-loop dependency-order blocker; shape TBD post-Gap-11
+ }
+ | AggregationRecognition {
+ accumulator_subgraph_node: NodeId // role: subgraph implementing the accumulator pattern
+ associative_op_node: NodeId // role: +/min/max operation node at reduce-point
+ associativity_witness: AssociativeReduceWitness // structural witness: op is associative per algebra.dag laws; shape TBD post-Gap-11
+ }
+ | MapFilterFoldFusion {
+ // Pipeline chain has minimum cardinality 2 (single map/filter/fold doesn't
+ // fuse). Per openai-pro BLOCKING PR #3067 2026-05-14: bare `List`
+ // admitted 0/1 nodes + non-pipeline nodes + duplicates + wrong ordering
+ // via prose-only comment. Fix: structural ≥2 enforcement via first +
+ // second + rest decomposition (rest is empty for exactly-2 chains).
+ first_pipeline_node: NodeId // role: first map/filter/fold node in chain (ordered position 1)
+ second_pipeline_node: NodeId // role: second map/filter/fold node (ordered position 2)
+ additional_pipeline_nodes: List // role: optional ordered tail (positions 3, 4, ...) — empty for exactly-2 chains
+ shared_iteration_cost: SymbolicCost // common iteration-space cost across chain elements
+ shared_space_witness: SharedIterationSpaceWitness // structural witness: chain elements share iteration space + are all map/filter/fold operation nodes + ordering preserved; shape TBD post-Gap-11
+ }
+
+// 🟡 SCAFFOLD per-variant proof-witness types — concrete shapes finalize
+// post-Gap-11 SymbolicCost / ProductCost / SumCost composition + lens-tier
+// implementation surface. Each witness type encodes ONE specific structural
+// proof obligation; NOT a generic Proof coproduct (avoids the
+// parallel-evidence-admits-invalid-pairings class codex BLOCKING #11751
+// flagged). Witness construction is lens-side; consumers receive the witness
+// as a structurally-valid proof receipt, not a "compiler-said-so" promise.
+//
+// Per openai-pro BLOCKING PR #3067 2026-05-14: witness names + obligations
+// now explicitly cover SEMANTIC PRESERVATION across value-flow AND effect-flow
+// AND drain-flow. Previous narrower names (LoopInvarianceWitness covering only
+// value-flow; NoConsumerWitness covering only value-consumer Ports) admitted
+// transformations that change semantics by changing effect/drain multiplicity.
+// Effect/drain substrate: src/v3/std/effects.dag (WorkflowEffect, EffectShape).
+//
+// Concrete shapes ratified per Substrate Mgr canvas during PB-X-tightness-lens
+// implementation worker dispatch (post-Gap-11). Current SCAFFOLD shapes — each
+// witness names its full semantic obligation in the comment, not just the
+// "value-flow" subset:
+//
+// type IterationSpaceEquivalenceWitness {
+// /* TBD per Gap-11 SymbolicCost equivalence-decidability algorithm.
+// Obligation: space_a ≡ space_b (symbolic cost) AND sequential-not-nested
+// AND no inter-loop value/effect/drain dependency-order blocker. */
+// }
+// type LoopSemanticInvarianceWitness {
+// /* TBD post-Gap-11 + EffectShape composition surface.
+// Obligation: invariant_subgraph has (a) no value-flow dependency on
+// loop variable (Port read-set analysis); (b) no effect whose
+// multiplicity changes when run once vs N times (WorkflowEffect
+// analysis per std/effects.dag); (c) no drain obligation that depends
+// on iteration count; (d) no returned-modified-resource threading
+// that requires per-iteration repetition. */
+// }
+// type SemanticDeadnessWitness {
+// /* TBD per Port consumption-walk + Effect-output walk + Drain-obligation
+// analysis algorithms.
+// Obligation: dead_subgraph has zero downstream consumers across ALL of:
+// (a) value-flow Ports; (b) effect outputs (WorkflowEffect surfaces per
+// std/effects.dag); (c) drain obligations (resource-end nodes); (d)
+// returned-modified-resource threads. */
+// }
+// type ConstantBoundSemanticWitness {
+// /* TBD per SymbolicCost variable-independence analysis + effect/drain
+// causality analysis.
+// Obligation: inner_bound has (a) no SymbolicCost dependency on outer
+// SizeVariable; (b) inner-loop effect/drain has no causality edge from
+// outer iteration index. */
+// }
+// type AssociativeReduceWitness { /* TBD per algebra.dag associativity-decidability surface */ }
+// type SharedIterationSpaceWitness { /* TBD per chain-fusion algorithm output */ }
+//
+// All 6 carriers are 🟡 SCAFFOLD; SCAFFOLD-→-TERMINAL trigger = Gap 11 lands +
+// lens-implementation worker dispatches resolve concrete witness fields + the
+// effect-flow/drain-flow analysis surfaces ratify per Substrate Mgr canvas.
+
+// Type-enforced pairing: each variant arm carries the EXACT role-named fields
+// + per-variant proof-witness type applicable to that transformation.
+// LoopFusion cannot pair with SemanticDeadness evidence; ConstantBoundPropagation
+// cannot pair with AssociativeReduce evidence. No parallel TransformationEvidence
+// coproduct + no bare List admitting wrong arities.
+
+// 🟡 SCAFFOLD per Gap 11 SymbolicCost composition trigger — named witness
+// carrier for "asymptotic strict dominance" (the relation
+// `asymptotic_dominates(dominator, dominated) ∧ dominator ≠ dominated`).
+//
+// Grounds against existing substrate:
+// - AsymptoticClass inhabits BoundedLattice per
+// src/v3/std/algebra.dag:418 — partial order is defined by the lattice.
+// - asymptotic_dominates(a, b) at src/v3/std/algebra.dag:428 — implements
+// the lattice's `a ≥ b` relation (reflexive). Strict dominance = `≥ ∧ ≠`.
+//
+// Per openai-pro BLOCKING PR #3067 #11790 2026-05-14: previous Loose carrier
+// had `actual: AsymptoticClass` + `tight: AsymptoticClass` as TWO ADJACENT
+// FIELDS with no structural proof of strict dominance. Admitted illegal pairs:
+// - `Loose { actual: ClassLinear, tight: ClassLinear, ... }` (equal — not strict)
+// - `Loose { actual: ClassLinear, tight: ClassQuadratic, ... }` (inverted — not dominance)
+// - `Loose { actual: ClassUnknown, tight: ClassConstant, ... }` (incomparable
+// in some readings — relies on lens construction discipline alone)
+// Fix: name the relation as a carrier. Role-named fields `dominator` (= former
+// `actual`) and `dominated` (= former `tight`) make the ordering explicit.
+//
+// SCAFFOLD content: current shape has named fields ordered by role but no
+// type-level proof of the dominance relation between them (no AsymptoticClass-
+// pair-witnesses tier in std yet). Construction discipline = lens-side
+// (Practice 6 API enforcement): `lens_complexity_tight` constructs
+// `AsymptoticStrictDominance` only when `asymptotic_dominates(dominator,
+// dominated) ∧ dominator ≠ dominated` is structurally verified against
+// SymbolicCost composition. Consumers receive the named witness as a
+// proof-relation receipt (NOT a "compiler-said-so" promise), same discipline
+// as the 6 transformation-evidence witnesses below.
+//
+// SCAFFOLD → TERMINAL trigger: Gap 11 SymbolicCost composition + lattice-
+// strict-ordering proof shape ratified per Substrate Mgr canvas. Concrete
+// post-Gap-11 shape: likely carries a `SymbolicCostDifferenceWitness` or
+// equivalent lattice-strict-ordering proof carrier per the chosen Gap 11
+// composition algebra.
+type AsymptoticStrictDominance {
+ dominator: AsymptoticClass // role: strictly larger class (= former `actual`)
+ dominated: AsymptoticClass // role: strictly smaller class (= former `tight`)
+ // Future SCAFFOLD-→-TERMINAL field (post-Gap-11): strict_dominance_proof: SymbolicCostStrictDominanceWitness
+}
+
+// 🟢 TERMINAL at the tightness-analysis scope. Discriminated result —
+// variant tag + named improvement witness IS the derivation predicate
+// (AlreadyTight ≡ actual == tight; Loose ≡ asymptotic_dominates(actual, tight)
+// ∧ actual ≠ tight, expressed structurally via AsymptoticStrictDominance).
+//
+// Per openai-pro BLOCKING PR #3067 #11790 2026-05-14: previous shape with
+// adjacent `actual`/`tight` fields admitted four illegal states (equal pair,
+// inverted pair, equal-pair with Loose tag, inverted-pair with Loose tag).
+// Fix: replace adjacent class fields with named AsymptoticStrictDominance
+// improvement witness above. Plus prior fix (openai-pro #11789): discriminate
+// the result + structural ≥1 transformation enforcement.
+// Per briansrls INLINE BLOCKING PR #3067 2026-05-14 at design-complexity-
+// tightness-lens.md:384: previous shape carried `section: SectionRef` inside
+// both variants, but SectionRef at src/v3/std/lens_application.dag:66-68 has
+// only `DeclarationScope { declaration: ... }` and `NodeScope { declaration:
+// ..., node: ... }` variants — no empty/identity value. The Monoid<
+// TightnessAnalysis> identity element needed a synthetic
+// placeholder which is ungrounded substrate (INVARIANTS P1).
+// Fix: section context moves OUT of TightnessAnalysis into the application
+// wrapper (EnforcedTightness.section below). Matches the live
+// EnforcedApplication/IntrospectApplication pattern at lens_application.dag:
+// 176-203 — lens output is per-tightness-conclusion; section is per-
+// application context wrapping the lens application.
+type TightnessAnalysis
+ = AlreadyTight {
+ actual: AsymptoticClass // = tight by construction; no separate tight field
+ }
+ | Loose {
+ improvement: AsymptoticStrictDominance // named witness: dominator strictly dominates dominated (see above)
+ first_transformation: ClassTierTightnessTransformation // ≥1 enforced — no empty derivation possible; class-tier-only by type (codex BLOCKING #11795)
+ additional_transformations: List // ordered tail; empty for single-transformation derivations; class-tier-only by type
+ }
+
+// Self-comparison carrier — STRUCTURALLY DISTINCT from EnforcedApplication
+// (which is user-budget comparison). Tightness is self-comparison: lens
+// produces discriminated TightnessAnalysis (AlreadyTight carries actual only;
+// Loose carries `improvement: AsymptoticStrictDominance` + ≥1 transformation
+// derivation); enforcement
+// dispatches on the variant tag. No user-declared budget field.
+//
+// Per codex BLOCKING #11751 PR #3067 2026-05-14: previous 3-param mirror of
+// EnforcedApplication created structural mismatch
+// — Budget type param was unused (no budget field) → admits invalid states.
+// Director ratification msg_d45523da had locked-in 3-param mirror as compromise;
+// codex correctly flagged that the compromise is incomplete. Resolved here:
+// distinct carrier shape for self-comparison; lens carrier is Lens