briansrls · May 13, 2026
diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md
@@ -305,7 +305,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 77 | `e_p_call_pattern_lookup_authoritative` | substrate-shape | T-E-P-Producer-Broadening | **CONSUMER_LANDED** — integration `e_p_call_pattern_lookup_authoritative` (`m2_substrate_inhabitance_test.rs`) pins `per_call_pattern_at` as the lens-facing query over the per-call evidence authority | CallPattern lookup authoritative |
 | 78 | `e_p_sub_value_relation_per_call_landed` | substrate-shape | T-E-P-Producer-Broadening | **CONSUMER_LANDED** (T-E-P P1 slices 1-7 per cluster-analysis audit §1) | SubValueRelation per-call landing |
 | 79 | `complexity_lens_behaviorally_complete` | structural-fold | T-Lens-Behavioral-Parity | SATISFIED-BY-CONSTRUCTION — #2220 | symbolic CostExpr + work/span split + asymptotic classification + temporary Rust cementing receipt (`complexity_lens_behavioral_completion.rs`) until `ComplexitySummary` TestClaim literals are expressible |
-| 80 | `cost_lens_behaviorally_complete` | structural-fold | T-Lens-Behavioral-Parity | **PASSING** — gate #80 abstract-cost scope now has executable `DimensionReport<SymbolicCost>` wiring via `analyze_symbolic_cost_dimension`, `SizeVariable` value identity by `source_port`, recursive `CallPattern` consumption, and Band-C frozen-projection cementing in `cost_lens_symbolic_consumer_test.rs`; target-realization composition remains tracked separately by T-CostLens gates #37/#40/#70 | Dimension<SymbolicCost> wiring + SizeVar value semantics + cementing test |
+| 80 | `cost_lens_behaviorally_complete` | structural-fold | T-Lens-Behavioral-Parity | **PASSING** — gate #80 abstract-cost scope now has executable `DimensionReport<SymbolicCost>` wiring via `analyze_symbolic_cost_dimension`, `SizeVariable` value identity by `source_port`, recursive `CallPattern` consumption, and Band-C frozen-projection cementing in `tests/dag/t_r3_gate_87_cementing_regen_cost_symbolic.dag` through the PB-B-1 runner table; target-realization composition remains tracked separately by T-CostLens gates #37/#40/#70 | Dimension<SymbolicCost> wiring + SizeVar value semantics + cementing test |
 | 81 | `parallelism_lens_behaviorally_complete` | structural-fold | T-Lens-Behavioral-Parity / **Cluster F (T-LP-Retirement)** | **R3-LOAD-BEARING (carve-promoted-IN-R3 2026-05-09)** per Director ratification at gunbc#846 #issuecomment-4412330468; Stage 2e walker port from `workflow_parallelism.rs` → `.dag` per Cluster F sub-phase F-α (substrate-ready M-sized lane). See `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.1. Prior R4-CARVED (C1) status DISSOLVED. |
 | 82 | `effect_enumeration_lens_behaviorally_complete` | structural-fold | T-Lens-Behavioral-Parity / **Cluster F (T-LP-Retirement)** | **R3-LOAD-BEARING (carve-promoted-IN-R3 2026-05-09)** per Director ratification cascade at gunbc#846 #issuecomment-4412380947 → #4412433924 → #4412475559. Cluster F sub-phases **F-β.1 (migration-shape ratification canvas)** + **F-β.2 (atomic-migration implementation)** using existing `services.dag::Operation` carrier per locked design `docs/design-effect-enumeration-resource-threading.md` §3.2 + §6.2 ("Operation carrier already exists at services.dag:122; no new top-level carrier required"). F-β.1 canvas authoring stays in Substrate Mgr standing authority; Director ratifies surfaced migration-shape questions (Operation field reads / walker rewire surface / test-consumer breaking changes); F-β.2 worker dispatches against ratified shape. See `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.2-§1.3. Prior R4-CARVED (C2) status DISSOLVED. |
 | 83 | `lens_capability_register_zero_proxy_zero_stub` | state-check | T-Lens-Behavioral-Parity / **Cluster F sub-phase F-γ** | **DECLARED — full scope IN R3 (carve-promotion-IN-R3 2026-05-09)** per Director carve-promotion ratification at gunbc#846 #issuecomment-4412330468. Prior C3 scope-narrowing ("ZERO PROXY / ZERO STUB for in-scope lenses (complexity + cost) only") DISSOLVED — register status now fires for **ALL 4 in-R3 lenses** (complexity + cost + parallelism + effect_enum) at R3 close per carve-promotion. Cluster F sub-phase F-γ.2 (post-all-4-lenses-BEHAVIORALLY-COMPLETE cascade). See `docs/audit/r3-cluster-f-sequencing-plan-2026-05-09.md` §1.4.2. |

diff --git a/docs/v3-lens-capability-register.md b/docs/v3-lens-capability-register.md
@@ -38,7 +38,7 @@ A lens is only "done" when **both** axes are at their strongest grade for the sc
 | Lens | Structural | Behavioral | v2 counterpart | v3 output | What v2 has that v3 drops |
 |---|---|---|---|---|---|
 | `complexity.dag` | TERMINAL | COMPLETE | `src/v2/complexity.dag` (5488L) | `v3.std.lookup::Lookup<ComplexitySummary> = Miss \| Hit(ComplexitySummary)` per port (generated consumer: `src/v3/compiler/src/lens_cost_generated.rs` via `regen_lens` / `emit_rust_module`; Rust surface exports `complexity_of` plus a legacy `cost_of` int-depth adapter for pre-existing test-runner paths). `ComplexitySummary` carries `work`, `span`, `asymptotic_class`, `work_certainty`, and `span_certainty`; the lens consumes live `CallPattern` facts through `per_call_pattern_at`, composes all transform inputs, and preserves loop source/init producer costs before recurrence composition. | N/A — behavioral-completion substrate landed in #2220: symbolic work/span costs, SizeVariable display names, certainty, asymptotic classification, and recurrence consumption are present; frozen-oracle cementing for the published `ComplexitySummary` carrier is the temporary Rust receipt at `src/v3/compiler/tests/integration/cementing/complexity_lens_behavioral_completion.rs` until `.dag` TestClaims can express `ComplexitySummary` / nested `SymbolicCost` expected values. |
-| `cost.dag` | TERMINAL | COMPLETE | v2 `CostExpr` (embedded in `complexity.dag`) | `v3.std.lookup::Lookup<SymbolicCost> = Miss \| Hit(SymbolicCost)` per port (generated consumer: `src/v3/compiler/src/lens_cost_symbolic_generated.rs` via `regen_lens` / `emit_rust_module`; Rust surface re-exports `SymbolicCostLookup` as a type alias for `Lookup<SymbolicCost>`); E-C stages `std.computation::CallPattern` / `LoweringTarget`; E-I stages `std.induction::SubValueRelation` / `CostBound`; E-P provides the side-table `v3_compiler::dag::per_call_descent_evidence` producer and `per_call_pattern_at` query; E-M method carrier parity is closed by structural subsumption. `Dimension<SymbolicCost>` wiring is executable through `v3_compiler::analyze_symbolic_cost_dimension`, which returns `DimensionReport<SymbolicCost>` over the same generated `symbolic_cost_of` authority. **T-CostLens-Composition alpha/epsilon disposition** remains separate: §1.8 gates **#38** `coercion_cost_equals_complexity_by_construction` + **#39** `no_coercion_cost_dimension` are structurally satisfied by construction; gates **#37** / **#40** / **#70** cover target-realization composition and executable predicate/demo receipts outside this target-agnostic abstract-cost lens. | N/A for gate #80 scope — `SizeVariable` carries value identity by `source_port` with presentation-only `display_name`; recursive `CallPattern` consumption, happy-path `DimensionReport<SymbolicCost>::DimensionOk` composition over `symbolic_cost_of`, and same-source frozen projection cementing are pinned by `src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs`. Target-specific concrete realization composition remains tracked by T-CostLens-Composition gates #37/#40/#70, not as a behavioral gap in `cost.dag`'s abstract `SymbolicCost` lens. |
+| `cost.dag` | TERMINAL | COMPLETE | v2 `CostExpr` (embedded in `complexity.dag`) | `v3.std.lookup::Lookup<SymbolicCost> = Miss \| Hit(SymbolicCost)` per port (generated consumer: `src/v3/compiler/src/lens_cost_symbolic_generated.rs` via `regen_lens` / `emit_rust_module`; Rust surface re-exports `SymbolicCostLookup` as a type alias for `Lookup<SymbolicCost>`); E-C stages `std.computation::CallPattern` / `LoweringTarget`; E-I stages `std.induction::SubValueRelation` / `CostBound`; E-P provides the side-table `v3_compiler::dag::per_call_descent_evidence` producer and `per_call_pattern_at` query; E-M method carrier parity is closed by structural subsumption. `Dimension<SymbolicCost>` wiring is executable through `v3_compiler::analyze_symbolic_cost_dimension`, which returns `DimensionReport<SymbolicCost>` over the same generated `symbolic_cost_of` authority. **T-CostLens-Composition alpha/epsilon disposition** remains separate: §1.8 gates **#38** `coercion_cost_equals_complexity_by_construction` + **#39** `no_coercion_cost_dimension` are structurally satisfied by construction; gates **#37** / **#40** / **#70** cover target-realization composition and executable predicate/demo receipts outside this target-agnostic abstract-cost lens. | N/A for gate #80 scope — `SizeVariable` carries value identity by `source_port` with presentation-only `display_name`; recursive `CallPattern` consumption, happy-path `DimensionReport<SymbolicCost>::DimensionOk` composition over `symbolic_cost_of`, and same-source frozen projection cementing are pinned by `src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_cost_symbolic.dag` through the PB-B-1 runner table. The host-wrapper regression test `src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs` remains the residual Rust receipt for `per_call_pattern_at` and `analyze_symbolic_cost_dimension`, not the COMPLETE-row cementing authority. Target-specific concrete realization composition remains tracked by T-CostLens-Composition gates #37/#40/#70, not as a behavioral gap in `cost.dag`'s abstract `SymbolicCost` lens. |
 | `cost_target_realization.dag` | TERMINAL | **N/A** | None (v3-native; ε path consumer of `declaration_by_name` substrate accessor introduced by Slice 1a.0 / PR #2194) | Per-category meta-type `Declaration?` resolvers — `type_realization_meta(d)` / `callable_realization_meta(d)` / `operator_realization_meta(d)` / `behavior_realization_meta(d)` / `type_instantiation_realization_meta(d)` / `pattern_realization_meta(d)` (six total, covering all `*Realization` carriers in `src/v3/std/emit_model.dag`) — using `declaration_by_name` for name-keyed lookup. Slice 1a.1 of T-CostLens-Composition follow-on (#2141 ε scope per gunbc#2181 ratification): minimum-viable consumer-proof per INVARIANTS P2 closure of codex BLOCKING surfaced post-merge on Slice 1a.0. Slice 1a.2 adds Rust-side `v3_compiler::realization_cost::RealizationCostTable`, which filters realization declarations by `meta_tag`, requires `ValueBody.Structural.fields`, matches the active `language`, and extracts typed `target` / `op` keys plus `cost: Int`. Generated consumer: `src/v3/compiler/src/lens_cost_target_realization_generated.rs`. | N/A — ε path consumer-evidence-only; not a v2 mirror. ε composition (abstract `SymbolicCost` × per-target realization-cost) deferred to Slice 1a.3+. |
 | `effect_enumeration.dag` | TERMINAL | **PARTIAL** | None (v3-native) | `EffectEnumerationReport { facts, coverage_gaps, redundant_reads, transaction }` derived from the five `Behavior` variants and callable type-signature shape; generated consumer target: `src/v3/compiler/src/lens_effect_enumeration_generated.rs` via `regen_lens` / `emit_rust_module` | Audit verdict is path (ii): live primitives still require ambient resource/transport metadata rather than returned-modified-resource signatures (`dsl/std/resources.dag`, `dsl/std/primitives.dag`, `dsl/extdeps/shell.dag`, `dsl/extdeps/github/auth.dag`). Full `OperationEffect` retirement, resource-threading migration, and caller-side effect-set pinning are follow-up work. |
 | `idempotency.dag` | TERMINAL | **COMPLETE** | None (v3-native) | `WorkflowIdempotencyReport` via `lane2_workflow_at` + `std.effects::lane2_workflow_idempotency_report` | — (behavioral authority for the `WorkflowEffect` walk is `lane2_workflow_idempotency_report` in `src/v3/std/effects.dag`. `workflow_idempotency.rs` is still **parallel staging** for native `Dag` entry — same projection, hand mirror until an explicit dissolution removes it or routes through generated-only code; INVARIANTS P2 cleanup, not “two competing semantics.”) |
@@ -64,7 +64,7 @@ v2's complexity analysis imports carriers from `dsl/std/`. **E-T, E-C, and E-I h
 - `std.induction::SubValueRelation` (+ `CostBound`, `PolynomialExponent`, …) — staged by E-I (`src/v3/std/induction.dag`)
 - **E-P producer receipt:** side-table producer (`v3_compiler::dag::per_call_descent_evidence`, `src/v3/compiler/src/dag.rs`) covers the live lowered callable-edge classes pinned by `m2_substrate_inhabitance_test::e_p_per_call_descent_evidence_*`; `TransformNode` remains unwidened.
 
-The cost-lens call-site consumer and same-source cementing receipt have landed for the R3 gate #80 abstract `SymbolicCost` scope: `cost.dag` consumes `per_call_pattern_at` for recursive callable transforms, and `analyze_symbolic_cost_dimension` exposes happy-path `DimensionReport<SymbolicCost>::DimensionOk` composition over the generated `symbolic_cost_of` carrier on the cementing fixtures. Remaining T-CostLens work around target realization (#37/#40/#70) composes this abstract cost with target-specific realization rows; that is a separate consumer path, not a reason to downgrade `cost.dag` itself.
+The cost-lens call-site consumer and same-source cementing receipt have landed for the R3 gate #80 abstract `SymbolicCost` scope: `cost.dag` consumes `per_call_pattern_at` for recursive callable transforms, `analyze_symbolic_cost_dimension` exposes happy-path `DimensionReport<SymbolicCost>::DimensionOk` composition over the generated `symbolic_cost_of` carrier, and `t_r3_gate_87_cementing_regen_cost_symbolic.dag` is the `.dag` Band-C receipt for literal and countdown fixtures. Remaining T-CostLens work around target realization (#37/#40/#70) composes this abstract cost with target-specific realization rows; that is a separate consumer path, not a reason to downgrade `cost.dag` itself.
 
 ### Method semantics receipt (E-M closed by structural subsumption)