R3 Verification

docs/briefs/r3-v-pattern-a-tc1-v1-worker.md

@@ -1,12 +1,16 @@
 # R3 Pattern-A — TC1 first executable slice (V1) Worker Brief
 
-**Status:** DISPATCH-READY — **Q-PAFS Path A ACCEPTED** 2026-05-06 (Brian Director countersign; **authority** = committed [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 rows at `HEAD`; PR [#1824](https://github.com/gunb-ai/gunbc/pull/1824) is the **merge record** on `main`). Policy-layer fork closed; implementation still coordinates **Evaluator E3** (**E6-G1.a** static lens fold) in the **same release step** as this slice.
+**Status:** **HELD** — **Q-Reification** STOP + **Director η non-vacuity (Branch B)** 2026-05-06 ([gunbc#828](https://github.com/gunb-ai/gunbc/issues/828)). **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 **Q-Reification + ReflectedProgram\<T\>** (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). **Pre-auth queue:** patch this brief when Q-Reification / carrier land — do **not** replace wholesale.
 
 **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").
 
 **Ratified scope narrative (engineering brief):** [`docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md`](r3-v-tc1-eta-equivalence-deeper-analysis.md) §"DESIGN — Q-PAFS first executable slice (Pattern-A / TC1)" **Path A** — TC1 **static representative** via **E6-G1.a** (finite Director-visible lens set + fixed eta pair; `BinaryDimensionReportEquals` consumer envelope per [`docs/briefs/r3-v-pattern-a-coverage-rollup.md`](r3-v-pattern-a-coverage-rollup.md)).
 
-**Program plan:** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 rows **Q-PAFS**, **Q-Pattern-A-First-Slice-Subscope**, **Q-EVAL-Lens-Fold-First-Slice** — **ACCEPTED 2026-05-06 (Path A / G1.a)**.
+**Program plan (single operational authority):** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 — rows **Q-PAFS** + **Q-EVAL-Lens-Fold-First-Slice** **Status** columns hold **policy ACCEPTED (Path A / G1.a)** **and** **implementation supersession**: TC1 V1 **HELD** until Q-Reification + non-vacuous η path (or explicit §1.8 plumbing-only revision — **not** ratified). **This brief elaborates worker mechanics only** — it **does not** override or restate dispatch authority independently of that table (**INVARIANTS** §P2 / modeling-discipline Practice 5).
+
+**Director routing:** **Q-Reification** propagates via Director audit ([gunbc#828](https://github.com/gunb-ai/gunbc/issues/828)); Verification consumes outcome and patches this brief when the §10.3 table moves.
+
+**PR #1844 caveat:** Director-confirmed **strict** argument-opacity (`read`/`validate` ignore `Dag`/`Behavior`; fixed witness) — Branch B stands. If Evaluator revises to **thread behavior-shaped evidence** before report formation despite opaque leaf bodies, re-open Verification analysis before dispatch.
 
 ## §1.8 closure predicate (this slice)
 
@@ -20,16 +24,17 @@ Gates **#12–#14** (TC2 / TC3 / RustDagIsomorphism executables) stay **DECLARED
 
 | Preference | Worker | Condition |
 | --- | --- | --- |
-| **Primary** | **bold-crane-790** ([gunbc#1748](https://github.com/gunb-ai/gunbc/issues/1748)) | When child session is active **and** **V6** (`bridge_retirement_ledger_zero` audit cadence) reaches a **clean checkpoint** acceptable to Verification Mgr — then route **V1** implementation PR(s) through bold-crane. |
-| **Alternate** | **New worker** (spawn per `feedback_idle_workers_dispatchable_directly`) | If bold-crane remains saturated on **V6** or session stays archived — do **not** block V1 on crane availability; Brian / Director staffing read authorizes substitute. |
+| **Primary** | **bold-crane-790** ([gunbc#1748](https://github.com/gunb-ai/gunbc/issues/1748)) | **Track A** ( **V6** ledger audit, TC2/TC3/RustDagIso, partner-scope PRs per schedule): when session active **and** **V6** reaches a **clean checkpoint** acceptable to Verification Mgr — route **those** PRs through bold-crane. **`tc1_eta_equivalence_executable` / TC1 V1 slice excluded** until Branch B hold clears (above). |
+| **Alternate** | **New worker** (spawn per `feedback_idle_workers_dispatchable_directly`) | If bold-crane saturated on **V6** or archived — substitute for **non-TC1-V1** Track A work; do **not** interpret as TC1 dispatch unblock. |
+| **TC1 V1** | bold-crane (when **unheld**) | Same primary pin resumes **only** when **Q-Reification + ReflectedProgram\<T\>** (or revised §1.8 TC1 semantics) satisfies non-vacuous η per Director ratification. |
 
 **cool-heron-521** remains on **V2 / V4 / V5** prep per partition; **not** the default home for V1 unless explicitly redirected.
 
 ## Scope (in)
 
 - First **executable** TC1 slice under **Path A** only: static representative **E6-G1.a**; consumer remains **`BinaryDimensionReportEquals`** over two typed `DimensionReport<C>` reports once producers exist.
 - Verification-owned: **TestClaim** wiring, integration tests, fixture **naming** for strict-fire slice, and **coverage** of the ratified representative set (no universal quantification in V1).
-- Coordinated same-step landing of **Evaluator E3** / **E6-G1.a** (Evaluator Mgr [#1743](https://github.com/gunb-ai/gunbc/issues/1743)) — Verification does **not** own evaluator internals; this brief names the **interface** dependency.
+- **After** **Q-Reification** resolution + **non-vacuous** lens-over-Dag path: coordinated landing with **Evaluator E3** / producer shape ([#1743](https://github.com/gunb-ai/gunbc/issues/1743)) when interface satisfies §Strict-Fire minimum semantics — Verification does **not** own evaluator internals. **Not** paired with **argument-opaque** Option 3 slice for TC1 gate closure (Director Branch B).
 
 ## Scope (out) — STOP+PING
 
@@ -46,7 +51,7 @@ Hold **without** widening by inertia:
 
 | Dependency | Owner | Why |
 | --- | --- | --- |
-| **E6-G1.a static lens fold** | Evaluator Mgr | Two structurally named programs produce typed `DimensionReport<C>` through evaluator-owned fold — **same release step** as V1 slice per ACCEPTED bundle. |
+| **E6-G1.a / E3 producer** | Evaluator Mgr | Fold must yield reports that **depend on reflected program shape** enough for **non-vacuous η-invariance** — **not** satisfied by **argument-opaque** `read`/`validate` (PR #1844 strict shape). **Blocked** until **Q-Reification** + **ReflectedProgram\<T\>** (or equivalent) lands **and** STOP clears; then TC1 V1 may re-pair on **ratified** producer contract. |
 | **T-Substrate-Lens-Primitive + lens producer retirement progress** | Substrate / PB lanes | Path A assumes existing fold machinery; no parallel `lens_apply` interpretation for the fold receipts. |
 | **Representative lens set + eta pair declaration refs** | Substrate (facts) + Verification (fixture refs) | Finite, Director-visible set enumerated in `.dag` / declarations — not “all `Lens<C>`” in V1. |
 

docs/briefs/r3-v-pattern-a-tc2-v1-worker.md

@@ -0,0 +1,75 @@
+# R3 Pattern-A — TC2 first executable slice (Church-Rosser / strategy-order) Worker Brief
+
+**Status:** **PRE-AUTH DISPATCH-READY** — brief authored **ahead of** runtime triggers (Brian directive: pre-authored queue). **No strict-fire Implementation dispatch** until §Dependencies clear. **Independent of TC1 V1 Branch B hold** — TC2 is **strategy-order / Church-Rosser** obligation, not η-equivalence; do **not** block TC2 prep on TC1 Q-Reification unless shared **unified predicate** or **fold** substrate lands single PR (then coordinate sequencing only).
+
+**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — absorbed formal-grounding / Pattern-A cluster (see [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure").
+
+**Engineering analysis (research):** [`docs/briefs/r3-v-tc2-church-rosser-analysis.md`](r3-v-tc2-church-rosser-analysis.md) — coverage inputs for the **strategy-order** leg of unified `BinaryDimensionReportEquals` (Director Option 2 / [#828](https://github.com/gunb-ai/gunbc/issues/828)).
+
+**Program plan (single operational authority):** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 — **Q-PAFS** Path **A** remains the **policy** anchor for Pattern-A ordering (TC1 first slice **policy**); **TC1 V1 implementation supersession** (Branch B) is **TC1-only**. **This brief** elaborates **gate #12** `tc2_church_rosser_executable` per [`docs/r3-structure.md`](../r3-structure.md) §"Acceptance" — **does not** override §10.3 table (**INVARIANTS** §P2).
+
+**Consumer envelope:** `BinaryDimensionReportEquals` over two **typed** `DimensionReport<C>` reports produced under **two named executable evaluation strategies** for the **same** program + lens fold — roll-up: [`docs/briefs/r3-v-pattern-a-coverage-rollup.md`](r3-v-pattern-a-coverage-rollup.md).
+
+## §1.8 closure predicate (this slice)
+
+| Gate ID | Gate name (canonical) | Target transition |
+| --- | --- | --- |
+| **#12** | `tc2_church_rosser_executable` | **DECLARED → CONSUMER_LANDED** when executable `TestClaim` + runner path land per this brief; **PASSING** when strict-fire evaluates green on CI. |
+
+**Do not** fold TC2 into **TC1 V1** PRs or deferred-claim widening — separate worker dispatch per [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md) gate table.
+
+## Worker pin (Verification Mgr partition)
+
+| Preference | Worker | Condition |
+| --- | --- | --- |
+| **Primary** | **bold-crane-790** ([gunbc#1748](https://github.com/gunb-ai/gunbc/issues/1748)) | Route **TC2 V1** implementation PR(s) when §Dependencies **and** **V6** / Track A staffing allow — **after** Substrate+Evaluator preconditions land; same Track A pin as schedule §2 **A**. |
+| **Alternate** | **New worker** | If bold-crane saturated — substitute per `feedback_idle_workers_dispatchable_directly`; do **not** invent parallel `lens_apply` interpretation. |
+
+## Scope (in)
+
+- Executable **TC2** slice: **≥2 closed `EvalStrategy` (or equivalent) inhabitants** + **strategy-keyed** `DimensionReport<C>` producers + **structural equality** via unified predicate **strategy-order modifier** (not a TC2-isolated `TestPredicate` name).
+- Verification-owned: **TestClaim** wiring, integration tests, fixture naming for strict-fire slice once Substrate predicate shape exists.
+- **Tractability default (research ordering):** prefer **second strategy = second `InputEvaluationOrder` under eager applicative** (e.g. `RightFirst` vs `LeftFirst`) before full **normal-order** / thunk path — per [`r3-v-tc2-church-rosser-analysis.md`](r3-v-tc2-church-rosser-analysis.md) §1.
+
+## Scope (out) — STOP+PING
+
+| Item | Discipline |
+| --- | --- |
+| **TC2-specific parallel predicate** | **STOP+PING** — consume **unified** `BinaryDimensionReportEquals` + **strategy-order modifier** only (Director Option 2). |
+| **Deferred fixture rewrite** | **STOP+PING** — `tc2_evaluation_order_independence_deferred.dag` stays staging until prerequisites land ([`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md)). |
+| **Vacuous strategy “equality”** | **STOP+PING** — both strategies must **actually** affect evaluation / memo keys where claimed; no constant-report shortcut (same spirit as TC1 Branch B, **strategy** axis). |
+
+## Dependencies (hard)
+
+Mapped from [`r3-v-tc2-church-rosser-analysis.md`](r3-v-tc2-church-rosser-analysis.md) §4 — all must be **green** before strict-fire **PASSING**:
+
+| ID | Dependency | Owner | Why |
+| --- | --- | --- | --- |
+| P1 | PR-A.2 evaluator state carriers | Evaluator | `EvalFrame` / `EvalStateStack` substrate path |
+| P2 | PR-A.3 strategy + memo **implemented** | Evaluator | closed `EvalStrategy` + memo keying |
+| P3 | PR-B.1 eager body evaluator | Evaluator | baseline execution |
+| P4 | **Second executable strategy** (or input order) | Evaluator | TC2 **bundle blocker** per formal-grounding TC bundle |
+| P5 | `fold_lens<C>` (or equivalent) → `DimensionReport<C>` | Substrate + Evaluator | lens fold authority |
+| P6 | Unified generalized predicate + **strategy-order modifier** | Substrate | evolves from `LensOutputEquals` per Director #828 |
+
+## Dispatch triggers (mechanical)
+
+1. **P4 + P6** land on `main` (or Director-visible equivalent) — **Evaluator + Substrate** issue/PR receipts linked from [#1743](https://github.com/gunb-ai/gunbc/issues/1743) / Substrate inbox as appropriate.
+2. **Worker available** — **bold-crane-790** (or substitute) per partition.
+3. **Verification Mgr** issues **sub-issue** under **#1748** + `addSubIssue` wire + inbox pointer (per Director workflow 2026-05-06).
+
+## Implementation slices (suggested PR shape)
+
+1. **Slice 1 — substrate/evaluator receipt:** second strategy + modifier hook produces two typed reports on a **fixed** representative program + lens set (finite, Director-visible).
+2. **Slice 2 — executable `TestClaim`:** `tc2_church_rosser_executable` + integration **Pass**.
+3. **Slice 3 — ledger / doc receipt:** §1.8 status column **DECLARED → CONSUMER_LANDED → PASSING**; cross-link [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) TC2 row.
+
+**Substrate lands first** if carrier split — Verification PR must not invent predicate variant (**INVARIANTS** §P1).
+
+## Cross-refs
+
+- Analysis: [`r3-v-tc2-church-rosser-analysis.md`](r3-v-tc2-church-rosser-analysis.md)
+- TC bundle: [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md)
+- Deferred fixture: `src/v3/compiler/tests/fixtures/tc2_evaluation_order_independence_deferred.dag`
+- Evaluator: [`r2-evaluator-manager.md`](r2-evaluator-manager.md) (TC2 row); inbox [#1743](https://github.com/gunb-ai/gunbc/issues/1743)
+- TC1 worker (ordering neighbor, different gate): [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md)

docs/briefs/r3-verification-manager.md

@@ -96,6 +96,7 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl
 - [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md) — Lane 2 standby brief.
 - [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md) — Lane 3 standby brief.
 - [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md) — Pattern-A V1 (TC1 first executable slice; Q-PAFS Path A **ACCEPTED** 2026-05-06).
+- [`r3-v-pattern-a-tc2-v1-worker.md`](r3-v-pattern-a-tc2-v1-worker.md) — Pattern-A TC2 (`tc2_church_rosser_executable`) dispatch-ready worker brief (**PRE-AUTH**; strategy-order / Church-Rosser slice).
 - [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) — absorbed-responsibility TC1/TC2/TC3 bundle (NOT a lane; audit-cadence artifact per `r3-structure.md` §"Manager structure" Item 2 3-lane authority).
 
 **Pending (post-spawn manager authors autonomously):**