briansrls · May 10, 2026 · May 10, 2026 · May 10, 2026 · May 10, 2026 · May 10, 2026
diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md
@@ -232,12 +232,12 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 6 | `lens_testgen_dot_rs_retired` | state-check | T-LensProducer-Retirement | DECLARED | same gate as #5 |
 | 7 | `regen_lens_dot_rs_retired` | state-check | T-LensProducer-Retirement | DECLARED | gated on PB-1 bin-shim emit pattern |
 | 8 | `sg0_non_test_zero` | state-check | T-LensProducer-Retirement | DECLARED | SG-0 T-PB-A non-test ratchet = 0 (`EXPECTED_HAND_AUTHORED_NON_TEST` + `EXPECTED_HAND_AUTHORED_FRAGMENTS`) |
-| 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 | **CONSUMER_LANDED** — bounded `AlgebraicLaw` runner receipts on honest additive/multiplicative `Int` lenses (`src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag`; canonical `TestClaim.name` `l7_algebraic_laws_witnessed`; integration `r3_verification_l4_l7_l5_skeleton_test.rs`) | **PASSING** = exhaustive per-(algebra, inhabitant, law) §Acceptance coverage per `r3-structure.md` (distributivity / lattice absorption / non-`AlgebraicLawKind` laws remain substrate §P1); slice receipts ≠ ledger closure |
-| 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 |
+| 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-2 receipt added 2026-05-10** via PR #2585 (L4 add-then-branch emit/eval). | **Slice receipts (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`) + add-then-branch slice (PR #2585). **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 | **CONSUMER_LANDED** — bounded `AlgebraicLaw` runner receipts on honest additive/multiplicative `Int` lenses (`src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag`; canonical `TestClaim.name` `l7_algebraic_laws_witnessed`; integration `r3_verification_l4_l7_l5_skeleton_test.rs`); incremental coverage advanced 2026-05-10 via PR #2602. | **PASSING** = exhaustive per-(algebra, inhabitant, law) §Acceptance coverage per `r3-structure.md` (distributivity / lattice absorption / non-`AlgebraicLawKind` laws remain substrate §P1); slice receipts ≠ ledger closure |
+| 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). **PR #2603 (2026-05-10)** advances the executable scaffold but does not retire the canvas-deferral; status flip to PASSING requires fresh Director ratification post-#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 | **PASSING** (PR #2598 — TC2 Church-Rosser executable landed 2026-05-10; supersedes #2396 shape-only) | runtime prereq met via PR #2598 |
 | 13 | `tc3_pattern_a_second_mover_executable` | DimensionReport-typed | T-V-L4-L7-Direct | **CONSUMER_LANDED + PASSING** — bounded-runner second-mover proxy evaluates the embedded `succ(succ(0))` claim program under genuinely distinct applicative orders (`LeftFirst` baseline vs `RightFirst` compare projection) and Pass-asserts identical top-level `Value` via `tc3_pattern_a_second_mover_dimension_reports_equivalent_under_binary_equals` (`src/v3/compiler/src/test_runner.rs`; integration `tc3_strong_normalization_strict_fire_test.rs`). Single forward dissolution trigger: D4 eval-step / bounded-step producer + G1.a static-lens-fold producer-surface-wiring per `docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md` — when those land, the runner arm migrates to live producer-emitted reports without changing fixture or claim name. | runtime prereq (substrate-side): Descent execution proof (E5; landed) + eval-step producer (forward-only dissolution trigger; not blocking gate close) |
-| 14 | `rust_dag_isomorphism_executable` | Dag-iso | T-V-L4-L7-Direct | DECLARED (NEW 2026-05-06) | runtime prereq: shape-report producers |
+| 14 | `rust_dag_isomorphism_executable` | Dag-iso | T-V-L4-L7-Direct | **PASSING** (PR #2571 — fail-closed Rust DAG isomorphism gate landed 2026-05-10) | runtime prereq met via PR #2571 |
 | 15 | `l5_cross_target_consistency` | structural-fold | T-V-L5-Corpus | DECLARED | corpus-driven; depends on L4 + Shape A grounding |
 | 16 | `pb_self_compile_fixed_point` | fixed-point | T-FixedPoint | CONSUMER_LANDED (R1 horizon; R3 stronger interpretation) | bit-identical stage0 + emitted artifact |
 | 17 | `numeric_abstract_carriers_landed` | substrate-shape | T-Numeric-Construction | DECLARED | Magnitude (`dsl/std/magnitude.dag`) → Nat (`dsl/std/nat.dag`) → Int (`dsl/std/integer.dag`) → **`Rational = Field<FieldOfFractions<Int>>`** (`dsl/std/rational.dag`) → **`Real = ApproximateField<FieldOfFractions<Int>>`** (`dsl/std/float.dag`; STOP Option A — **not** `ApproximateField<Rational>`). Authority: [`docs/design-numeric-construction.md`](design-numeric-construction.md) + [`docs/r3-structure.md`](r3-structure.md) §T-Numeric-Construction. Hand-written integration ratchet: `real_default_alias_resolves_to_approximate_field_over_field_of_fractions_of_int`. **CONSUMER_LANDED** not claimed: INVARIANTS §P2 requires a **generated** consumer of the declared surface (see §1.7). |
@@ -254,7 +254,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 28 | `omni_layers_share_one_node_tree` | structural-fold | T-Omni-Shape-B | **CONSUMER_LANDED + PASSING** | `m1_5_omni_shape_b_openapi_test.rs` `omni_layers_share_one_node_tree` — one `compile_to_dag` per workflow; Shape A `emit_rust` + canonical route extraction + Shape B OpenAPI YAML + Markdown + SQL DDL projections share the same `Dag` |
 | 29 | `anthropic_wire_typed_serde_alignment` | substrate-shape | T-Anthropic-Wire | **PASSING** (PR #2208 G5 Anthropic re-dispatch + PR #2164 variant-aware projection; ratchets `anthropic_request_coproduct_wire_contracts_emit_targeted_serde` at `src/v2/tests/src/pipeline.rs:6482` + `anthropic_messages_request_body_json_matches_messages_wire_tags` at `src/v2/tests/src/pipeline.rs:6918` green at HEAD `9d9f7d786` per cluster-I close-shape per [`docs/audit/r3-cluster-analysis-2026-05-09.md`](audit/r3-cluster-analysis-2026-05-09.md) §2 row I; 200-body residual tracked separately by `structural_coverage_gap_anthropic_messages_200_residual` / coproduct slice 3 brief, NOT in #29 scope) | typed end-to-end |
 | 30 | `anthropic_unit_enum_role_serialization_correct` | structural-fold | T-Anthropic-Wire | **CONSUMER_LANDED** (PR #2208 G5 Anthropic re-dispatch; refresh per cluster-analysis audit §1) | role enum serializes correctly |
-| 31 | `bridge_source_span_file_participation_retired` | state-check | T-Bridge-Retirement | DECLARED | typed-identity-surface authority |
+| 31 | `bridge_source_span_file_participation_retired` | state-check | T-Bridge-Retirement | **PASSING** (PR #2586 — correction file participation bridge retired 2026-05-10) | typed-identity-surface authority |
 | 32 | `bridge_mark_bootstrap_secret_nominal_opacity_retired` | state-check | T-Bridge-Retirement | **PASSING** | `dsl/std/types.dag` `type Secret nominal_opaque = String` + `src/v3/std/bridge_ledger.dag` row `Retired` + unit ratchet `dag.rs::bridge_mark_bootstrap_secret_nominal_opacity_retired` (bootstrap snapshots carry `Declaration.nominal_opacity` on `Secret`); historical name-keyed bootstrap bridge removed (#1272 / #937 lineage) |
 | 33 | `bridge_canonical_lens_name_dispatch_retired` | state-check | T-Bridge-Retirement | DECLARED | DeclarationRef/typed identity |
 | 34 | `bridge_include_str_side_channels_retired` | state-check | T-Bridge-Retirement | DECLARED | substrate query surface |
@@ -266,16 +266,16 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 40 | `symbolic_cost_expr_equals_executable` | SymbolicCost-typed | T-CostLens-Composition | DECLARED — ε path RATIFIED 2026-05-07 (Q-Cost-Composition-Layering canvas); closes via Verification Mgr (#2075) ratchet authoring on Rust-side composition consumer + executable predicate per ε path | runtime prereq: cost lens consumer per ε |
 | 41 | `v2_oracle_no_remaining_test_consumers` | state-check | T-V2-Retirement | DECLARED | no .rs test consumes src/v2/ |
 | 42 | `v2_directory_deleted` | state-check | T-V2-Retirement | DECLARED | src/v2/ removed from workspace |
-| 43 | `auto_parallelism_independent_binds_emit_parallel` | demonstration | T-Free-Consequences-Demonstration | DECLARED | bind-independent → parallel emit |
-| 44 | `auto_parallelism_dependent_binds_pending_lens_fail_closed` | demonstration | T-Free-Consequences-Demonstration | DECLARED | dependent-bind fixture fails closed on pending scalar parallelism lens until real schedule lands |
-| 45 | `auto_parallelism_branch_arms_serialize` | demonstration | T-Free-Consequences-Demonstration | DECLARED | branch arms sequenced |
-| 46 | `auto_loop_parallelism_provable_independence_emits_parallel` | demonstration | T-Free-Consequences-Demonstration | DECLARED | opt-in `Lens<Iteration-Independence>` |
-| 47 | `auto_loop_parallelism_unproven_falls_back_sequential` | demonstration | T-Free-Consequences-Demonstration | DECLARED | no heuristic auto-parallelization |
-| 48 | `auto_loop_parallelism_dependence_emits_sequential` | demonstration | T-Free-Consequences-Demonstration | DECLARED | provable dependence → sequential |
-| 49 | `auto_memoization_repeated_pure_call_cached` | demonstration | T-Free-Consequences-Demonstration | DECLARED | composes Lens<Purity>·Lens<Cost> |
-| 50 | `auto_memoization_no_caching_for_one_shot` | demonstration | T-Free-Consequences-Demonstration | DECLARED | no scaffolding for single-call |
-| 51 | `cross_target_optimization_constant_fold_consistent` | structural-fold | T-Free-Consequences-Demonstration | DECLARED | structural cost-shrink across targets |
-| 52 | `cross_target_optimization_cost_structurally_derived` | structural-fold | T-Free-Consequences-Demonstration | DECLARED | cost-lens reading structurally derived |
+| 43 | `auto_parallelism_independent_binds_emit_parallel` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2495 — parallel emit for independent binds landed 2026-05-10) | bind-independent → parallel emit |
+| 44 | `auto_parallelism_dependent_binds_pending_lens_fail_closed` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2523 — dependent binds emit sequential landed 2026-05-10) | dependent-bind fixture fails closed on pending scalar parallelism lens until real schedule lands |
+| 45 | `auto_parallelism_branch_arms_serialize` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2527 — branch arms serialize landed 2026-05-10) | branch arms sequenced |
+| 46 | `auto_loop_parallelism_provable_independence_emits_parallel` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2529 — loop iteration independence emits parallel landed 2026-05-10) | opt-in `Lens<Iteration-Independence>` |
+| 47 | `auto_loop_parallelism_unproven_falls_back_sequential` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2532 — unproven falls back sequential landed 2026-05-10) | no heuristic auto-parallelization |
+| 48 | `auto_loop_parallelism_dependence_emits_sequential` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2535 — dependence emits sequential landed 2026-05-10) | provable dependence → sequential |
+| 49 | `auto_memoization_repeated_pure_call_cached` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2536 — repeated pure call cached landed 2026-05-10) | composes Lens<Purity>·Lens<Cost> |
+| 50 | `auto_memoization_no_caching_for_one_shot` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2547 — one-shot memoization witness landed 2026-05-10) | no scaffolding for single-call |
+| 51 | `cross_target_optimization_constant_fold_consistent` | structural-fold | T-Free-Consequences-Demonstration | **PASSING** (PR #2577 — constant-fold cost witness executable landed 2026-05-10) | structural cost-shrink across targets |
+| 52 | `cross_target_optimization_cost_structurally_derived` | structural-fold | T-Free-Consequences-Demonstration | **PASSING** (PR #2578 — structural cost receipt landed 2026-05-10) | cost-lens reading structurally derived |
 | 53 | `workflow_substrate_carriers_landed` | substrate-shape | T-Workflow-As-Data | **CONSUMER_LANDED (partial)** (PR #2160 — WorkflowSecret + CronExpression β-ratified; refresh per cluster-analysis audit §1; remaining sub-carriers tracked in T-WAD slice queue) | `std.workflow` carriers |
 | 54 | `timing_lens_carrier_landed` | substrate-shape | T-Workflow-As-Data | **CONSUMER_LANDED** (PR #2360 — Substrate T-Workflow-As-Data timing-lens carrier post-T-LBP COMPLETE) | `Lens<TimingMeasurement>` carrier |
 | 55 | `shared_external_attachment_pattern_documented` | substrate-shape | T-Workflow-As-Data | DECLARED | `WorkflowObservationAnchor` + 6 invariants |
@@ -292,7 +292,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 66 | `lens_producer_retirement_executable_witness` | demonstration | T-LensProducer-Retirement | DECLARED (NEW 2026-05-06) | DEFERRED to Row-4 receipts per PB Mgr F3 |
 | 67 | `numeric_construction_demonstration` | demonstration | T-Numeric-Construction | DECLARED (NEW 2026-05-06) | `Int<32>` + `Real<64>` round-trip |
 | 68 | `anthropic_wire_demonstration` | demonstration | T-Anthropic-Wire | DECLARED (NEW 2026-05-06) | deterministic mock; live-API NOT closure gate |
-| 69 | `bridge_retirement_demonstration` | demonstration | T-Bridge-Retirement | **CONSUMER_LANDED** — integration `bridge_retirement_demonstration` (`canonical_lens_bridge_ratchet_test.rs`) | typed-identity-surface executes through `LensOutputEquals` using fixture-local `DeclarationRef` resolution + production `apply_lens_declaration` |
+| 69 | `bridge_retirement_demonstration` | demonstration | T-Bridge-Retirement | **PASSING** (PR #2551 — bridge retirement demonstration landed 2026-05-10) | integration `bridge_retirement_demonstration` (`canonical_lens_bridge_ratchet_test.rs`); typed-identity-surface executes through `LensOutputEquals` using fixture-local `DeclarationRef` resolution + production `apply_lens_declaration` |
 | 70 | `cost_lens_demonstration` | demonstration | T-CostLens-Composition | DECLARED — ε path RATIFIED 2026-05-07 (Q-Cost-Composition-Layering canvas at PR #2181); closes via Rust-side composition fixture demonstrating end-to-end cost reading per ε in T-CostLens follow-on slice | ≥2 algebra-instances + ≥1 recursive call |
 | 71 | `v3_self_host_demonstration` | demonstration | T-V2-Retirement | DECLARED (NEW 2026-05-06) | bootstrap PB-Runtime trampoline runs end-to-end |
 | 72 | `e_p_producer_demonstration` | demonstration | T-E-P-Producer-Broadening | **CONSUMER_LANDED** — integration `e_p_producer_demonstration` (`m2_substrate_inhabitance_test.rs`) | unary recursive self-call: `SubValueRelation` + scalar `per_call_pattern_at` → `lower_call_pattern` / `DescentEvidence::Strict` (multi-arg per-port vectors: other E-P tests) |