briansrls · May 10, 2026 · May 7, 2026 · May 7, 2026 · May 7, 2026 · May 7, 2026
diff --git a/docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md b/docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md
@@ -118,7 +118,7 @@ The representative is **not** a coverage proof; it is a strict-fire witness for
 
 **RATIFIED** at gunbc#828 c#4413738978 (2026-05-09): specific-representative selection + scope statement above are dispatch-locked. The illustrative subject body (`fn tc3_subject_bounded_sum() -> Int = fold([1, 2, 3], 0, lambda acc x. acc + x)`) is **illustrative-not-binding**; final fixture wording is canvas-tier authoring scope at worker-dispatch time per `feedback_substrate_shape_belongs_in_mgr_canvas`. Bounded-`Cardinality(3)` shape is ratified as the binding structural constraint.
 
-Cross-Pattern-A consistency preserved across the family (TC1/TC2/TC3/TC4; R3 §1.8 row #13 / Pattern-A sibling context) — strict-mirror discipline maintained; (α)/(β) novel-substrate-introduction explicitly deferred-not-blocked to a post-R3 cycle (prior R4+ carve framing — DISSOLVED 2026-05-09 per gunbc#846 #issuecomment-4412330468 carve-promotion-IN-R3 ratification; gates R3-load-bearing per `docs/r4-carve-out-routing.md`; Class P partition cite is historical reference to PR #2437 Debt-Paydown lane).
+Cross-Pattern-A consistency preserved across the family (TC1/TC2/TC3/TC4; R3 §1.8 row #13 / Pattern-A sibling context) — strict-mirror discipline maintained; (α)/(β) novel-substrate-introduction explicitly deferred-not-blocked to a post-R3 cycle (prior R4+ carve framing — DISSOLVED 2026-05-09 per gunbc#846 #issuecomment-4412330468 carve-promotion-IN-R3 ratification; Class P partition cite is historical reference to PR #2437 Debt-Paydown lane). Scope statement remains binding for this representative.
 
 ## 7 Discipline notes (worker-tier)
 

diff --git a/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md b/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md
@@ -1,6 +1,6 @@
 # R3 Pattern-A — TC1 first executable slice (V1) Worker Brief
 
-**Status:** **HELD on Branch B η-non-vacuity** — Director η non-vacuity (Branch B) 2026-05-06 ([gunbc#828](https://github.com/gunb-ai/gunbc/issues/828)). **Scaffold landed at [PR #2184](https://github.com/gunb-ai/gunbc/pull/2184) with NotYetImplemented sentinel pending E3.c upgrade** per Director (C-modified) ratification at [gunbc#828](https://github.com/gunb-ai/gunbc/issues/828) on 2026-05-07; consumer wiring (η-pair callables + `BinaryDimensionReportEquals` predicate + integration test) cleanly authored under Option 3 hard bars (no `lens_apply` / `eval_substrate_reify` / `reflect_behavior` imports). Sentinel assertion is fail-closed-by-construction — actual implementation that runs WILL fail the NotYetImplemented assertion when Evaluator E3.c ([#1970](https://github.com/gunb-ai/gunbc/issues/1970)) lands, forcing fixture upgrade. §1.8 #11 stays **DECLARED** until E3.c merges and assertion upgrades; flip then is DECLARED → CONSUMER_LANDED → PASSING in one move. Original (pre-scaffold) HELD framing follows. **Q-Reification CLEARED 2026-05-07** ([Option A ratified](https://github.com/gunb-ai/gunbc/pull/2096), `Dag` IS the reflected program; no separate carrier). **Q-PAFS Path A** remains **ACCEPTED** (PR [#1824](https://github.com/gunb-ai/gunbc/pull/1824) merge record on `main`). **V1 (`tc1_eta_equivalence_executable`) unpairs** from Evaluator **E3 Option 3** narrow **argument-opaque** representative slice for **TC1 acceptance** — that shape yields **vacuous** `BinaryDimensionReportEquals` (constant `DimensionReport<C>`); it cannot honestly close the gate against [`r3-v-tc1-eta-equivalence-deeper-analysis.md`](r3-v-tc1-eta-equivalence-deeper-analysis.md) §What TC1 Asserts + §Strict-Fire Extension Surface. **Resume dispatch** only after lens fold consumes `Dag` via `.dag` body authority through Evaluator (real lens-over-Dag fold, non-vacuous η obligation) **or** Director-visible §1.8 / program-plan semantics revision (explicit "plumbing-only" TC1 milestone — **not** ratified 2026-05-06). **Q-Reification gate is cleared**; remaining hold is Branch B η non-vacuity only.
+**Status:** **HELD on Branch B η-non-vacuity** — Director η non-vacuity (Branch B) 2026-05-06 ([gunbc#828](https://github.com/gunb-ai/gunbc/issues/828)). **Scaffold landed at [PR #2184](https://github.com/gunb-ai/gunbc/pull/2184) with NotYetImplemented sentinel pending the non-vacuous lens-over-`Dag` producer path** per Director (C-modified) ratification at [gunbc#828](https://github.com/gunb-ai/gunbc/issues/828) on 2026-05-07; consumer wiring (η-pair callables + `BinaryDimensionReportEquals` predicate + integration test) cleanly authored under Option 3 hard bars (no `lens_apply` / `eval_substrate_reify` / `reflect_behavior` imports). Sentinel assertion is fail-closed-by-construction — actual implementation that runs WILL fail the NotYetImplemented assertion when the Evaluator-side non-vacuous producer path lands, forcing fixture upgrade. §1.8 #11 stays **DECLARED** for R3; strict-fire assertion upgrade moves to a fresh post-R3 issue after the producer path lands. **2026-05-09 Director (a)-disposition:** Evaluator E3.c ([#1970](https://github.com/gunb-ai/gunbc/issues/1970)) closed as superseded-by-deferral; the remaining path is blocked on E4/G1.b ([#1972](https://github.com/gunb-ai/gunbc/issues/1972)), currently HELD-CANVAS-DEFERRED past R3. R3-close evidence routes through the Pattern A second-mover audit slice: scaffold-with-sentinel, fail-closed structure landed, no strict-fire promotion. Original (pre-scaffold) HELD framing follows. **Q-Reification CLEARED 2026-05-07** ([Option A ratified](https://github.com/gunb-ai/gunbc/pull/2096), `Dag` IS the reflected program; no separate carrier). **Q-PAFS Path A** remains **ACCEPTED** (PR [#1824](https://github.com/gunb-ai/gunbc/pull/1824) merge record on `main`). **V1 (`tc1_eta_equivalence_executable`) unpairs** from Evaluator **E3 Option 3** narrow **argument-opaque** representative slice for **TC1 acceptance** — that shape yields **vacuous** `BinaryDimensionReportEquals` (constant `DimensionReport<C>`); it cannot honestly close the gate against [`r3-v-tc1-eta-equivalence-deeper-analysis.md`](r3-v-tc1-eta-equivalence-deeper-analysis.md) §What TC1 Asserts + §Strict-Fire Extension Surface. **Resume dispatch** only after lens fold consumes `Dag` via `.dag` body authority through Evaluator (real lens-over-Dag fold, non-vacuous η obligation) **or** Director-visible §1.8 / program-plan semantics revision (explicit "plumbing-only" TC1 milestone — **not** ratified 2026-05-06). **Q-Reification gate is cleared**; remaining hold is Branch B η non-vacuity only.
 
 **Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — absorbed formal-grounding / Pattern-A cluster (not a fourth lane; see [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure").
 
@@ -16,7 +16,7 @@
 
 | Gate ID | Gate name (canonical) | Target transition |
 | --- | --- | --- |
-| **#11** | `tc1_eta_equivalence_executable` | **DECLARED → CONSUMER_LANDED** when executable `TestClaim` + runner path land per this brief; **PASSING** when strict-fire evaluates green on CI. |
+| **#11** | `tc1_eta_equivalence_executable` | R3 slice leaves #11 **DECLARED** with fail-closed `NotYetImplemented` sentinel; **CONSUMER_LANDED / PASSING** deferred to a fresh post-R3 strict-fire issue after #1972. R3 evidence is the Pattern A second-mover audit receipt. |
 
 Gates **#12–#14** (TC2 / TC3 / RustDagIsomorphism executables) stay **DECLARED** until their **separate** worker dispatches; **do not** fold them into this PR.
 
@@ -58,8 +58,8 @@ Hold **without** widening by inertia:
 ## Implementation slices (suggested PR shape)
 
 1. **Slice 1 — wiring receipt:** Substrate + Evaluator land minimal producers/refs so both `DimensionReport<C>` sides are **typed** and **lifted** per Evaluator #1131 safe contract (no fixture-local producer identity).
-2. **Slice 2 — executable `TestClaim`:** `tc1_eta_equivalence_executable` (or ratified final name per §1.8 ledger) + suite row; integration test exercises **Pass** on representative set.
-3. **Slice 3 — ledger / doc receipt:** Update §1.8 **Status** column **DECLARED → CONSUMER_LANDED → PASSING** as CI proves; cross-link [`docs/briefs/r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) absorbed-responsibility audit row for TC1.
+2. **Slice 2 — executable `TestClaim`:** `tc1_eta_equivalence_executable` (or ratified final name per §1.8 ledger) + suite row; R3 integration test exercises the shape-valid, fail-closed `NotYetImplemented` sentinel until #1972 lands.
+3. **Slice 3 — ledger / doc receipt:** Keep §1.8 **Status** column **DECLARED** for R3, record the post-R3 #1972 strict-fire trigger, and cross-link [`docs/briefs/r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) absorbed-responsibility audit row / Pattern A second-mover audit receipt for TC1.
 
 Single PR per `feedback_brief_pr_cadence` if possible; if Substrate and Verification diffs must split, **Substrate lands first** — Verification PR must not invent carrier shapes.
 

diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md
@@ -234,7 +234,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 8 | `sg0_non_test_zero` | state-check | T-LensProducer-Retirement | DECLARED | SG-0 EXPECTED_HAND_AUTHORED_NON_TEST count = 0 |
 | 9 | `l4_emit_eval_match` | structural-fold | T-V-L4-L7-Direct | **CONSUMER_LANDED** — executable consumer exists; §Acceptance corpus coverage **incomplete** (§1.7 corpus-quantified rule) | **Slice-1 receipt (evidence, non-closure):** three Rust/Int W1 `DifferentialEquals` certification seeds Pass in CI (`r3_verification_l4_emit_eval_match.dag`, suite `r3_verification_l4_l7_direct_suite`, harness `r3_verification_l4_l7_l5_skeleton_test.rs`; canonical claim `l4_emit_eval_match`). **PASSING** = every certification-corpus program per `r3-structure.md` §Acceptance. **Ledger phrase:** per-program emit ↔ eval algebraic equality |
 | 10 | `l7_algebraic_laws_witnessed` | alg-law-witness | T-V-L4-L7-Direct | DECLARED (skeleton/staged) | exhaustive per-(algebra, inhabitant, law) coverage |
-| 11 | `tc1_eta_equivalence_executable` | DimensionReport-typed | T-V-L4-L7-Direct | **DECLARED through R3** (scaffold authored PR #2184 with NotYetImplemented sentinel per Director (C-modified) ratification at #828). **AMENDED 2026-05-09 per Director (a)-disposition**: TC1 V1 strict-fire cannot reach PASSING absent #1972 substrate canvas-tier work, which is HELD-CANVAS-DEFERRED past R3 per Substrate Mgr Path-A confirmation 2026-05-08. Gate #11 stays DECLARED through R3 close; not load-bearing for R3-thesis honest-close arithmetic (97 enumerated − 1 canvas-deferred {#11} = 96 R3-load-bearing per §1.5). Prior phrasing ("flips DECLARED → CONSUMER_LANDED → PASSING in one move on Evaluator E3.c merge") superseded — that path required #1972 substrate which is post-R3. | runtime prereq: G1.a static-rep OR G1.b generic + eta relation; #1972 canvas-tier substrate post-R3 |
+| 11 | `tc1_eta_equivalence_executable` | DimensionReport-typed | T-V-L4-L7-Direct | **DECLARED through R3** (scaffold authored PR #2184 with NotYetImplemented sentinel per Director (C-modified) ratification at #828). **AMENDED 2026-05-09 per Director (a)-disposition**: E3.c #1970 closed superseded-by-deferral; TC1 V1 strict-fire cannot reach PASSING absent #1972 substrate canvas-tier work, which is HELD-CANVAS-DEFERRED past R3 per Substrate Mgr Path-A confirmation 2026-05-08. Gate #11 stays DECLARED through R3 close; R3-close evidence routes through the Pattern A second-mover audit slice and is not load-bearing for R3-thesis honest-close arithmetic (97 enumerated - 1 canvas-deferred {#11} = 96 R3-load-bearing per §1.5). Prior phrasing ("flips DECLARED -> CONSUMER_LANDED -> PASSING in one move on Evaluator E3.c merge") superseded; strict-fire flip moves to a fresh post-R3 issue after #1972. | runtime prereq: G1.a static-rep OR G1.b generic + eta relation; #1972 canvas-tier substrate post-R3 |
 | 12 | `tc2_church_rosser_executable` | DimensionReport-typed | T-V-L4-L7-Direct | DECLARED (NEW 2026-05-06) | runtime prereq: second strategy/input order + strategy-keyed report |
 | 13 | `tc3_pattern_a_second_mover_executable` | DimensionReport-typed | T-V-L4-L7-Direct | DECLARED (NEW 2026-05-06) | runtime prereq: Descent execution proof (E5) + eval-step producer |
 | 14 | `rust_dag_isomorphism_executable` | Dag-iso | T-V-L4-L7-Direct | DECLARED (NEW 2026-05-06) | runtime prereq: shape-report producers |

diff --git a/src/v3/compiler/tests/fixtures/tc1_substrate_lens_eta_equivalence_strict_fire.dag b/src/v3/compiler/tests/fixtures/tc1_substrate_lens_eta_equivalence_strict_fire.dag
@@ -22,8 +22,11 @@
 // production/evaluation substrate" reason. Per Director (C-modified) ratification at gunbc#828
 // 2026-05-07: §1.8 gate #11 status STAYS DECLARED on this scaffold landing — the
 // NotYetImplemented sentinel is fail-closed-by-construction (an actual implementation that runs
-// WILL fail the assertion when Evaluator E3.c lands, forcing fixture upgrade). Status flips
-// DECLARED → CONSUMER_LANDED → PASSING in one move on E3.c (gunbc#1970) merge.
+// WILL fail the assertion when the non-vacuous Evaluator producer path lands, forcing fixture
+// upgrade). Director (a)-disposition 2026-05-09: E3.c (gunbc#1970) closed
+// superseded-by-deferral; the producer path is now blocked on E4/G1.b (gunbc#1972), currently
+// HELD-CANVAS-DEFERRED past R3. R3 keeps the sentinel as Pattern A second-mover audit evidence;
+// strict-fire CONSUMER_LANDED/PASSING moves to a fresh post-R3 issue after #1972.
 //
 // Hard bars (E6-G1.a Option 3 caveat #1853): no `lens_apply` / `eval_substrate_reify` /
 // `reflect_behavior` imports. Carrier shape is the ratified Q-Reification Option A `Dag`-as-
@@ -44,16 +47,16 @@ type Tc1EtaLensObservation {}
 
 // η-pair callables — both compute the same `Int` value. `eta_subject_f_eta` is the η-expanded
 // form `lambda x. apply(eta_subject_f, [x])`; the lens-fold-over-`Dag` of either should yield
-// equal `DimensionReport<Tc1EtaLensObservation>` values once Evaluator E3.c lands the
-// substrate-fact projection path. These declarations make the η-pair source-visible (Mgr/
+// equal `DimensionReport<Tc1EtaLensObservation>` values once the Evaluator substrate-fact
+// projection path lands. These declarations make the η-pair source-visible (Mgr/
 // reviewer can read non-vacuity intent off the .dag) even though runtime fold isn't wired
 // at this slice.
 fn eta_subject_f(x: Int) -> Int = x + 1
 fn eta_subject_f_eta(x: Int) -> Int = eta_subject_f(x)
 
 // Typed report refs — the unified `BinaryDimensionReportEquals` consumer envelope reads
 // these as `DeclarationRef`s and validates carrier-equivalence today. Fold-output wiring
-// is Evaluator-side per #1970 cross-Mgr split.
+// is Evaluator-side; #1970 closed superseded-by-deferral, with the remaining path tracked at #1972.
 type tc1_subject_f_report = DimensionReport<Tc1EtaLensObservation>
 type tc1_subject_eta_expanded_report = DimensionReport<Tc1EtaLensObservation>
 
@@ -62,7 +65,7 @@ type tc1_subject_eta_expanded_report = DimensionReport<Tc1EtaLensObservation>
 // source-visible η-pair witness — the runtime fold-application is Evaluator-side authority.
 data tc1_eta_equivalence_executable_claim: TestClaim = {
   name: "tc1_eta_equivalence_executable",
-  source: "// TC1 V1 strict-fire — eta-equivalent .dag programs declared in fixture module;\n// runtime lens-fold-over-Dag gated on Evaluator E3.c (gunbc#1970).\nlet _: Int = 0\n",
+  source: "// TC1 V1 scaffold-with-sentinel — eta-equivalent .dag programs declared in fixture module;\n// strict-fire evaluation deferred to post-R3 Evaluator producer path (gunbc#1972 after #1970 deferral).\nlet _: Int = 0\n",
   file_name: "tc1_eta_equivalence_executable.v3",
   predicate: BinaryDimensionReportEquals(
     tc1_subject_f_report,

diff --git a/src/v3/compiler/tests/integration/tc1_substrate_lens_eta_equivalence_strict_fire_test.rs b/src/v3/compiler/tests/integration/tc1_substrate_lens_eta_equivalence_strict_fire_test.rs
@@ -4,21 +4,25 @@
 //!
 //! V1 first slice per Pattern-A / E6-G1.a (Q-PAFS Path A ACCEPTED 2026-05-06; Q-Reification
 //! Option A ratified 2026-05-07 in PR #2096; Substrate Gate A merged 2026-05-07 in PR #2079).
-//! Cross-Mgr split per Evaluator E3.c (gunbc#1970): Verification authors the .dag-side η-pair +
-//! lens consumer envelope; Evaluator wires lens-fold-over-`Dag` substrate-fact projection.
+//! Cross-Mgr split: Verification authors the .dag-side η-pair + lens consumer envelope; Evaluator
+//! wires the non-vacuous lens-fold-over-`Dag` substrate-fact projection. Director (a)-disposition
+//! 2026-05-09: E3.c (gunbc#1970) closed superseded-by-deferral; the remaining producer path is
+//! tracked at E4/G1.b (gunbc#1972), currently HELD-CANVAS-DEFERRED past R3.
 //!
 //! Today's runner returns `NotYetImplemented` with the canonical "structural shape is valid"
 //! reason (`eval_binary_dimension_report_equals_shape` in `src/v3/compiler/src/test_runner.rs`).
 //! Per Director (C-modified) ratification at gunbc#828 2026-05-07: §1.8 gate #11 status STAYS
 //! DECLARED on this scaffold landing; the NotYetImplemented sentinel is fail-closed-by-
-//! construction (any actual implementation that runs WILL fail this assertion when E3.c lands,
-//! forcing fixture upgrade). Status flips DECLARED → CONSUMER_LANDED → PASSING in one move on
-//! Evaluator E3.c (gunbc#1970) merge + assertion upgrade.
+//! construction (any actual implementation that runs WILL fail this assertion when the producer
+//! path lands, forcing fixture upgrade). R3 keeps the sentinel as Pattern A second-mover audit
+//! evidence; strict-fire CONSUMER_LANDED/PASSING moves to a fresh post-R3 issue after #1972.
 
 use v3_compiler::compile_to_dag;
 use v3_compiler::test_runner::{ClaimResult, TestRunner};
 use v3_compiler::CompileError;
 
+use crate::common::run_on_larger_stack;
+
 const FIXTURE_SOURCE: &str =
     include_str!("../fixtures/tc1_substrate_lens_eta_equivalence_strict_fire.dag");
 const FIXTURE_PATH: &str =
@@ -27,6 +31,12 @@ const SUITE_NAME: &str = "tc1_substrate_lens_eta_equivalence_strict_fire_suite";
 
 #[test]
 fn tc1_strict_fire_suite_has_canonical_executable_claim_with_valid_binary_shape() {
+    run_on_larger_stack(|| {
+        tc1_strict_fire_suite_has_canonical_executable_claim_with_valid_binary_shape_inner()
+    });
+}
+
+fn tc1_strict_fire_suite_has_canonical_executable_claim_with_valid_binary_shape_inner() {
     let dag = match compile_to_dag(FIXTURE_SOURCE, FIXTURE_PATH) {
         Ok(dag) => {
             assert!(
@@ -49,9 +59,11 @@ fn tc1_strict_fire_suite_has_canonical_executable_claim_with_valid_binary_shape(
         results[0].claim_name, "tc1_eta_equivalence_executable",
         "claim name must be the §1.8 #11 canonical gate name"
     );
-    // Today: shape-valid NotYetImplemented (runner waits on Evaluator E3.c / gunbc#1970).
-    // When E3.c lands, this assertion flips from NotYetImplemented to Pass — that is the
-    // §1.8 #11 CONSUMER_LANDED → PASSING transition without further fixture edits.
+    // Today: shape-valid NotYetImplemented (runner waits on the Evaluator producer path;
+    // #1970 closed superseded-by-deferral, remaining path tracked at #1972).
+    // R3 intentionally keeps this sentinel as scaffold-with-sentinel evidence. When #1972 lands
+    // in post-R3 work, the fresh strict-fire issue flips this assertion from NotYetImplemented to
+    // Pass as the §1.8 #11 CONSUMER_LANDED -> PASSING transition.
     assert!(
         matches!(
             &results[0].result,