R3 §1.8 gate #10: canonical l7_algebraic_laws_witnessed consumer + ledger

docs/r3-program-plan.md

@@ -179,7 +179,7 @@ Mgrs author per-gate spec citing the (a)/(b)/(c) satisfaction; closure-ledger en
 |---|---|---|
 | T-Tier3-Dissolution | `tier3_*_mirror_dissolved` (state-check) | + `tier3_dissolution_demonstration_executes` — at least one Tier3-mirror-consumer .dag program runs end-to-end via Evaluator |
 | T-LensProducer-Retirement | retirement gates (state-check) | + `lens_producer_retirement_executable_witness` (per PB Mgr poke-hole 2026-05-06 F3 — reframed from `_demonstration`) — execution-ready witness DEFERRED to Row-4 equivalence receipt landing per `docs/design-pb-runtime-interpreter.md` §5.1 + convergence matrix; near-term demo = retirement state-check + doc receipts; "demonstration" status re-promotes when Row-4 + Item 4 receipts exist |
-| T-V-L4-L7-Direct | `l4_emit_eval_match` (**§1.8 #9** — **CONSUMER_LANDED** on Rust/Int W1 slice; **not §1.8 PASSING** until full certification corpus per `r3-structure.md` §Acceptance); `l7_algebraic_laws_witnessed` still staged (closure bar = exhaustive L4 corpus + per-(algebra, inhabitant, law) L7 coverage per `r3-structure.md` §"Lane structure") | Executable seeds + §1.7 corpus rule: slice **Pass** receipts ≠ acceptance **PASSING**; full lane demonstration remains gated on corpus exhaustion + L7 |
+| T-V-L4-L7-Direct | `l4_emit_eval_match` (**§1.8 #9** — **CONSUMER_LANDED** on Rust/Int W1 slice; **not §1.8 PASSING** until full certification corpus per `r3-structure.md` §Acceptance); `l7_algebraic_laws_witnessed` (**§1.8 #10** — **CONSUMER_LANDED** on bounded `AlgebraicLaw` `Int` slice per §1.8 ledger Notes; **not §1.8 PASSING** until exhaustive per-(algebra, inhabitant, law) L7 coverage per `r3-structure.md` §"Lane structure") | Executable seeds + §1.7 corpus rule: slice **Pass** receipts ≠ acceptance **PASSING**; full lane demonstration remains gated on corpus exhaustion + exhaustive L7 |
 | T-V-L5-Corpus | `l5_cross_target_consistency` ✓ | (existing) |
 | T-FixedPoint | `pb_self_compile_fixed_point` ✓ | (existing) |
 | T-Numeric-Construction | substrate-shape gates only | + `numeric_construction_demonstration` — end-to-end program using `Int<32>` + `Real<64>` round-trip executes |
@@ -233,7 +233,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 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 | DECLARED (skeleton/staged) | exhaustive per-(algebra, inhabitant, law) coverage |
+| 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 |
 | 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 |

src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag

@@ -54,10 +54,15 @@ data r3_verification_l7_algebraic_laws_skeleton: TestClaim = {
 // `Identity`). Lattice meet/join **associativity/commutativity** tags are **not** green-lit here on
 // `Int` `+` (that would read as lattice laws without meet/join carriers). Bounded-lattice /
 // Boolean-algebra / free-monoid identity placeholders likewise stay **out** of the passing matrix.
-data r3_l7_semigroup_associativity: TestClaim = {
-  name: "r3_l7_semigroup_associativity",
+//
+// §1.8 gate #10 canonical `TestClaim.name` / declaration id (`docs/r3-program-plan.md`): bounded
+// `AlgebraicLaw::Associativity` on honest `Int` `+` (Semigroup slice). **PASSING** on the §Acceptance
+// ledger remains exhaustive per-(algebra, inhabitant, law) coverage per `r3-structure.md`; this row
+// is the executable consumer hook matching gate id `l7_algebraic_laws_witnessed`.
+data l7_algebraic_laws_witnessed: TestClaim = {
+  name: "l7_algebraic_laws_witnessed",
   source: "fn r3_l7_semigroup_associativity_op(a: Int, b: Int) -> Int = a + b\n",
-  file_name: "r3_l7_semigroup_associativity.v3",
+  file_name: "l7_algebraic_laws_witnessed.v3",
   predicate: AlgebraicLaw(Associativity, r3_l7_semigroup_associativity_op),
   requires: []
 }
@@ -195,7 +200,7 @@ data r3_verification_l7_algebra_skeleton_suite: TestSuite = {
 data r3_verification_l7_algebra_matrix_suite: TestSuite = {
   name: "r3_verification_l7_algebra_matrix_suite",
   claims: [
-    r3_l7_semigroup_associativity,
+    l7_algebraic_laws_witnessed,
     r3_l7_monoid_identity,
     r3_l7_commutative_monoid_commutativity,
     r3_l7_group_identity,

src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs

@@ -6,11 +6,13 @@
 //! (`docs/r3-program-plan.md` §1.7 corpus-quantified rule — ledger **PASSING** awaits full corpus).
 //! Plus a mixed-lineage `NotYetImplemented` control. Lane 1 L7 exercises bounded `Associativity`,
 //! `Commutativity`, and `Identity` operational witnesses on **honest additive vs multiplicative `Int`
-//! lenses** (`+` vs `*`). The L7 matrix suite locks claims whose **Int lens semantics match the
-//! tagged obligation** (e.g. multiplicative `Identity` uses `*`); lattice / Boolean / free-monoid
-//! obligations and lattice meet/join law tags stay **out** of the passing matrix until faithful
-//! carriers exist (`dsl/std/algebra.dag`, INVARIANTS §P1 / MODELING M9); see fixture **Receipt limits**
-//! — this is not ROADMAP exhaustive L7 closure. Lane 2 / L5 rows remain intentionally deferred where noted.
+//! lenses** (`+` vs `*`). Canonical §1.8 gate **#10** `l7_algebraic_laws_witnessed` maps to the matrix
+//! lead row (`AlgebraicLaw::Associativity` on `Int` `+`). The L7 matrix suite locks claims whose **Int
+//! lens semantics match the tagged obligation** (e.g. multiplicative `Identity` uses `*`); lattice /
+//! Boolean / free-monoid obligations and lattice meet/join law tags stay **out** of the passing
+//! matrix until faithful carriers exist (`dsl/std/algebra.dag`, INVARIANTS §P1 / MODELING M9); see
+//! fixture **Receipt limits** — slice receipts ≠ ROADMAP exhaustive L7 closure. Lane 2 / L5 rows
+//! remain intentionally deferred where noted.
 //! Matrix: `docs/briefs/r3-v-l7-algebra-coverage-matrix.md`.
 
 use std::sync::OnceLock;
@@ -43,11 +45,12 @@ const L7_FIXTURE_PATH: &str =
     "src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag";
 const L7_SUITE: &str = "r3_verification_l7_algebra_skeleton_suite";
 const L7_CLAIM: &str = "r3_verification_l7_algebraic_laws_skeleton";
+const L7_GATE_CLAIM: &str = "l7_algebraic_laws_witnessed";
 const L7_MATRIX_SUITE: &str = "r3_verification_l7_algebra_matrix_suite";
 /// Claims wired into [`L7_MATRIX_SUITE`] — honest **additive vs multiplicative Int** slices only
 /// (`+` vs `*`); no lattice / monoid inhabitant rows (see fixture receipt limits).
 const L7_MATRIX_PASS_CLAIMS: &[&str] = &[
-    "r3_l7_semigroup_associativity",
+    L7_GATE_CLAIM,
     "r3_l7_monoid_identity",
     "r3_l7_commutative_monoid_commutativity",
     "r3_l7_group_identity",
@@ -227,7 +230,32 @@ fn r3_verification_l7_algebraic_law_identity_skeleton_passes_bounded_witness() {
     });
 }
 
-/// Bounded-runner receipt for [`L7_MATRIX_SUITE`] only — **not** exhaustive `l7_algebraic_laws_witnessed` / ROADMAP coverage.
+/// §1.8 gate #10 canonical claim id — bounded `AlgebraicLaw::Associativity` on `Int` `+` (matrix lead row).
+#[test]
+fn l7_algebraic_laws_witnessed_passes_bounded_associativity_witness() {
+    run_on_larger_stack(|| {
+        let dag = cached_compile(L7_FIXTURE, L7_FIXTURE_PATH, &L7_DAG);
+        let claim_decl = dag.declaration_by_name(L7_GATE_CLAIM).unwrap_or_else(|| {
+            panic!("missing `{L7_GATE_CLAIM}` in {L7_FIXTURE_PATH}");
+        });
+        let claim = TestClaimValue::from_declaration(claim_decl).unwrap_or_else(|reason| {
+            panic!("`{L7_GATE_CLAIM}` should lower to a structural TestClaim: {reason}");
+        });
+        assert_eq!(
+            claim.claim_name, L7_GATE_CLAIM,
+            "canonical gate claim name must match §1.8 gate id"
+        );
+        let evaluation = TestRunner::new(dag).run_claim(&claim);
+        assert_eq!(evaluation.claim_name, L7_GATE_CLAIM);
+        assert!(
+            matches!(evaluation.result, ClaimResult::Pass),
+            "expected AlgebraicLaw::Associativity bounded witness Pass on Int `+`, got {:?}",
+            evaluation.result
+        );
+    });
+}
+
+/// Bounded-runner receipt for [`L7_MATRIX_SUITE`] only — **not** exhaustive §Acceptance / ROADMAP coverage.
 ///
 /// One [`TestRunner::run_suite`] covers every [`L7_MATRIX_PASS_CLAIMS`] row (including semigroup
 /// associativity and commutative-monoid commutativity) plus embedded-source `a + b` / `a * b`