D-CMR-1 / D-RA-2: the contract owns single-table set algebra; relalg delegates

.claude/board/ISSUES.md

@@ -78,7 +78,7 @@
 
 ## ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN — `normalize` can leave a program wider than as written (2026-10-16)
 
-**Status:** OPEN. **Basis:** MEASURED (D-HOLO-H14d stage 1, `crates/holo-h14d-probe`, 2 of 2,000 generated programs).
+**Status:** RESOLVED in PR (D-CMR-1, branch `claude/eager-albattani-iufugq`): absorption is matched against flattened sibling sets in `contract::set_algebra::normalize`; TEST-PINNED by `absorption_after_de_morgan_matches_flattened_siblings` (contract) and `tests/absorption_n17.rs` (relalg), both disable-verified red. **Was:** OPEN. **Basis:** MEASURED (D-HOLO-H14d stage 1, `crates/holo-h14d-probe`, 2 of 2,000 generated programs).
 
 - `¬(x ∧ (x ∨ y))` with `x = P1 ∧ P4` should reduce by absorption to `¬x = ¬P1 ∨ ¬P4`. `lance-graph-relalg::normalize` pushes the negation inward first (De Morgan), flattens, and returns `¬P1 ∨ ¬P4 ∨ ((¬P1 ∨ ¬P4) ∧ ¬P5 ∧ ¬P7)`: the dual absorption pattern `a ∨ (a ∧ b)` is present but `a` is spread across the flattened `Or`, so the rule no longer matches.
 - Consequence: the rewritten program needs more scratch slots than the original; the original answers, the rewrite is refused (`MAX_SLOTS` = 8). Answers are never wrong; only width.

.claude/board/LATEST_STATE.md

@@ -1,3 +1,12 @@
+## 2026-10-20 — D-CMR-1 / D-RA-2: single-table set algebra in the contract (in PR)
+
+- **Contract (new module):** `set_algebra::{SetExpr, Res, Cmp, normalize, Runs, OutOfUniverse}`. `SetExpr` = `All | Empty | Sym(u32) | Res(Res) | And | Or | Not`; `Sym` is an opaque two-valued set (no storage layout named), `Res` a residual predicate on one lane. `normalize` is the one implementation of the single-table rewrites (De Morgan, associative flattening, idempotence, complement pairs, per-lane interval fusion and merge, absorption matched against flattened siblings). `Runs` = sorted disjoint half-open row intervals with `∩ ∪ ∖` and `complement(universe)`, refused (`OutOfUniverse`) past the declared universe. No dependency added; no lowering, join or gather.
+- **relalg:** `normalize` converts `Rel` ↔ `SetExpr` (`Plane(i)` ↔ `Sym(i)`) and delegates; public API unchanged; the 16 pre-existing tests pass unchanged. Closes `ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN` (N17). Entry `entries/2026-10-20-d-cmr-1-set-algebra.md`.
+
+### Current Contract Inventory — net delta (`set_algebra.rs`)
+
+- `lance_graph_contract::set_algebra::{Cmp, Res, SetExpr, normalize, Runs, OutOfUniverse}` — see above. 10 tests: differential `normalize` vs materialized bitsets (3,000 random nested expressions, anti-vacuity on rewrite rate), no leaf growth, N17 and its dual, partial-cover silence twin, flatten-before-depth, De Morgan / complement pairs, `Runs` laws vs bitsets (universes 0..100), explicit-universe refusal.
+
 ## 2026-10-20 — main after #1626 (merged `bc8012da`)
 
 - **On main:** #1621 (`fcd1f60e`, D-RMAP focus probe and native join), #1622 (`4dbd0853`, plans D-RST and D-RPR), #1623 (`8b570ed3`, D-RMAP-2 tile-GEMM cell, polyfill tier), #1624 (`7d2722bd`, consolidation, plan links, D-RPR-1 handoff probe), #1625 (`37b866ee`, BF16 byte count), #1626 (`bc8012da`, D-RMAP-2 on the AMX tier). All six have arc entries.

.claude/board/STATUS_BOARD.md

@@ -243,7 +243,7 @@ Plan: `.claude/plans/relalg-v1.md`. Crate: `crates/lance-graph-relalg` (own work
 | **D-HOLO-H14c** | Thought-first positional reads `Thought(t)[Table(a)[i] : Table(b)[i]]`: point projection, presence/Hamming populations through mask-risc, explicit terminal rows; memory and fragmentation of positional tables; Lance 13 masked I/O; coordinate identity across rewrites (sub-ids -1 … -6) | Measured 2026-10-15 (v4, entry 2026-10-15-d-holo-h14c-thought-first): acceptance A–E met (tables consulted == k for every U; k = 2 read at U = 31 0.90–1.16x U = 2); C vs B on query-shaped reads mixed; uniform 1 % positional tables ≈ 93x payload resident (flagged); Lance prediction holds (uniform 1 % mask 1.00x bytes, clustered 0.24x); stale maps omit silently, refused by the version check; returned to the operator | tables consulted == requested lanes for every touched count; at k = 2, U = 31 read <= 1.25x U = 2; populations load no value; no row materialized outside the terminal; no wrong coordinate across rewrites; Lance prediction (1 % uniform mask does not halve bytes_read, 1 % clustered does) |
 | **D-HOLO-H14d** | C's own operation in four stages, C only: (1) relalg symbolic reduction of the thought's set expression, (2) materialize `R = P_a ∧ P_b ∧ A` (or `∨`) over presence planes, (3) Lance 13 read pruned by `R`, (4) COUNT/EXISTS from `R` or the operation on `T_a[i], T_b[i]` for survivors; sub-ids -1 … -5 | Measured 2026-10-16 (v4, entry 2026-10-16-d-holo-h14d-logic-mask-read): stage 1 decides 675/2,000 programs with 0 runs, 396 answered only after the rewrite, 2 widened (ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN), passes 1,065 vs 5,898; R costs 2–10 ns per 64-address word; Lance scans exactly |R| everywhere, bytes 1.00x at uniform 1 % full tile, 0.19x clustered 1 %, 0.01–0.12x inside a 1,024/8,192 aperture; payload ~6 ns per lane load, reads == |R| × k, not flat at small |R| (fixed word scan; prediction 4 falsified); fused Σ ~1.3 ns per value; point query 8–45 ns hot; returned to the operator | `R` == per-address reference; rewritten == as written on 2,000 programs; payload reads == |R| × k; Lance rows == |R| with reference values; five disable runs red |
 | **D-RA-1** | `Rel` + `normalize` + `symbolic` + R2IL lowering | Shipped #1546 `c21bd165` (11 tests, 11 disable runs red; four comparisons on one lane 8 → 2 ops; 70/2,000 small descriptions refused as written, all run rewritten) | == row oracle over 400 generated descriptions × 5 measures |
-| **D-RA-2** | Rules into the contract set IR (D-CMR-1/-6); relalg keeps only lowering or is deleted | DECISION 2026-10-20: option A, the contract owns the single-table set-algebra rewrites; relalg keeps relational planning, joins and lowering (`entries/2026-10-20-six-decisions.md` §2). No general relational AST for JC or Quack (`d-relalg-unified-v1.md` § Decisions). Next: D-CMR-1 | relalg tests pass unchanged against the contract IR |
+| **D-RA-2** | Rules into the contract set IR (D-CMR-1/-6); relalg keeps only lowering or is deleted | DECISION 2026-10-20: option A, the contract owns the single-table set-algebra rewrites; relalg keeps relational planning, joins and lowering (`entries/2026-10-20-six-decisions.md` §2). No general relational AST for JC or Quack (`d-relalg-unified-v1.md` § Decisions). In PR with D-CMR-1: relalg `normalize` delegates to `contract::set_algebra::normalize`; repointing crepe follows D-CMR-6 | relalg tests pass unchanged against the contract IR |
 | **D-RA-3** | Datalog rules as algebra values; names are labels resolved through the label codebook, never strings in a rule — council v3 (2026-10-16) places the Datalog VALUES in `metta::datalog`; D-RA-2 still gates relalg | Queued (after D-RA-2) | codebook-built rules == hand-written `Rel`; unknown label refused at resolution |
 | **D-RA-4** | **⛔ VIOLATION — GATHER. DO NOT BUILD. CORRECT: D-HOLO-H14c / H14d.** Bound recursion via external frontier driver over D-CMR-5 preimage | Queued (after D-CMR-5) | == row-oracle closure; frontier past bound refused |
 
@@ -254,7 +254,7 @@ Plan: `.claude/plans/d-cmr-concept-chain-normalization-v1.md`. Parent: D-CMR-RES
 | D-id | scope | status | gate / falsifier |
 |---|---|---|---|
 | **D-CMR-0** | Plan, identity matrix, inventory, board rows | Shipped #1532 (docs) | docs only; every inventory row cites code |
-| **D-CMR-1** | Set-theory IR core in the contract: `Runs` (∩ ∪ ∖, complement), residual `Res`, measures; pure | Queued — first architecture PR after the D-RA-2 decision (`entries/2026-10-20-six-decisions.md` §2) | algebra laws vs materialized bitsets as oracle |
+| **D-CMR-1** | Set-theory IR core in the contract: `Runs` (∩ ∪ ∖, complement), residual `Res`, measures; pure | In PR (branch `claude/eager-albattani-iufugq`): `contract::set_algebra::{SetExpr, Res, Runs, normalize}`; measures not yet (`entries/2026-10-20-d-cmr-1-set-algebra.md`) | algebra laws vs materialized bitsets as oracle |
 | **D-CMR-2** | Lowering: runs → extents, residual → predicates per run; measurement levels geometry / optics / etch | Queued (after D-CMR-1; lowering reaches mask-risc through core via `lance_graph::fold`, #1537 — there is no contract → mask-risc edge) | == row oracle; `Count` without residual reads zero rows |
 | **D-CMR-3** | Quack frontend: `Filter` → set IR (extent hoisting falls out) | Queued | identical answers on the quack suite; other-basis range stays residual |
 | **D-CMR-4** | Two dimensions: `Rect` over composite coordinates, row-major or Morton runs | Queued | rectangle ∩ == bitset oracle |

.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md

@@ -0,0 +1,21 @@
+# 2026-10-20 — D-CMR-1 / D-RA-2: the contract owns single-table set algebra
+
+**Status:** TEST-PINNED (in PR, branch `claude/eager-albattani-iufugq`). **Basis:** `ADR-2026-10-20-SIX` §2 (`entries/2026-10-20-six-decisions.md`).
+
+- **Moved:** relalg's rewrite rules to `lance_graph_contract::set_algebra::normalize`, unchanged except absorption. relalg's `normalize` converts `Rel` ↔ `SetExpr` (`Plane(i)` ↔ `Sym(i)`, `Atom` ↔ `Res`) and delegates. `symbolic`, `run`, lowering and the public API are unchanged. The contract stays dependency-free.
+- **Absorption** is matched against flattened sibling sets, removing one child at a time against the children still kept, in two forms: (1) a member of the dual child is a sibling, or a junction of siblings; (2) a sibling junction's members all occur in the dual child (`x ∨ (x ∧ y)` with `x` itself a conjunction). That closes N17 (`ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN`) for `x` a leaf, an `And` or an `Or`. Form 2 was found by crepe-plan-probe's N17 pin (CI `probe`), which this PR flips to assert the reduction.
+- **`Runs`:** sorted, disjoint, half-open intervals with `∩ ∪ ∖`, each one merge pass, O(n + m). `complement(universe)` refuses a set that reaches past the universe.
+- **Regression:** the 16 pre-existing relalg tests pass unchanged. 3 tests are new: `conversion_round_trips` plus 2 in `tests/absorption_n17.rs`.
+- **Disable runs** (commands: `cargo test --manifest-path crates/lance-graph-relalg/Cargo.toml --no-fail-fast` and `cargo test -p lance-graph-contract --lib set_algebra`):
+
+  | probe | what breaks |
+  |---|---|
+  | contract `normalize` returns its input | 10 of 14 `rewrites.rs` tests, and both N17 tests in relalg |
+  | absorption form 1 off | only the N17 tests: one in relalg, two in the contract |
+  | absorption form 2 off | only `absorption_of_a_superset_conjunction` |
+  | `max` dropped in the `union` merge | `runs_obey_the_set_laws_against_bitsets` |
+  | absorption on a partial cover (`all` → `any`) | the silence twin, and the bitset differential (an unsound rule) |
+
+- **Scope held:** no joins, gathers, positional addressing, recursion, D-MPS-8 or `graph_hop`. Measures (`Count`/`Sum` on `Runs`) are not in this PR.
+
+OPEN: D-CMR-6 catalogue; repointing crepe and Quack at the contract.

.claude/board/entries/README.md

@@ -25,7 +25,7 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately
 opposite directions; the stranding this convention prevents shows up in
 exactly one of them, never both.
 
-396 entries, 2026-08-06 .. 2026-10-20.
+397 entries, 2026-08-06 .. 2026-10-20.
 
 | date | entry id | finding | file |
 |---|---|---|---|
@@ -48,6 +48,7 @@ exactly one of them, never both.
 | 2026-10-20 | `D-RMAP-2-AMX` |  | [2026-10-20-d-rmap-2-amx-tier.md](2026-10-20-d-rmap-2-amx-tier.md) |
 | 2026-10-20 | `D-RMAP-2-AMX-RERUN` | §5a-AMX re-measured on a second AMX host | [2026-10-20-d-rmap-2-amx-remeasured.md](2026-10-20-d-rmap-2-amx-remeasured.md) |
 | 2026-10-20 | `D-RELALG-UNIFIED` |  | [2026-10-20-d-relalg-unified.md](2026-10-20-d-relalg-unified.md) |
+| 2026-10-20 | `D-CMR-1` |  | [2026-10-20-d-cmr-1-set-algebra.md](2026-10-20-d-cmr-1-set-algebra.md) |
 | 2026-10-20 | `D-SRAM-2` |  | [2026-10-20-crepe-rule-optimizer-spike.md](2026-10-20-crepe-rule-optimizer-spike.md) |
 | 2026-10-20 | `ce64-isa-not-storage` |  | [2026-10-20-ce64-isa-not-storage.md](2026-10-20-ce64-isa-not-storage.md) |
 | 2026-10-20 | `arm-b-prepare` |  | [2026-10-20-arm-b-prepare.md](2026-10-20-arm-b-prepare.md) |

crates/crepe-plan-probe/tests/pipeline.rs

@@ -674,14 +674,15 @@ fn l_renamed_and_noisy_rules_give_the_same_plan() {
 // M. The H14d absorption case
 // ---------------------------------------------------------------------------
 
-/// `normalize` still misses `¬(x ∧ (x ∨ y)) = ¬x` (H14d, 2026-10-16) — but
-/// only when `x` is itself an `And` or `Or`. Measured here: with `x` a plane or
-/// a comparison it reduces correctly; with `x = p0 ∧ p2` De Morgan and
-/// flattening run first and the absorption no longer matches. A relalg defect,
-/// pinned here, not fixed in the optimizer. This spike never builds the shape:
-/// it only emits an `And` of planes (no `Not`, no `Or`).
+/// `¬(x ∧ (x ∨ y)) = ¬x` (H14d, 2026-10-16). Until D-CMR-1 `normalize` missed
+/// it when `x` was itself an `And` or `Or`: De Morgan and flattening ran first
+/// and absorption no longer matched. Fixed upstream in
+/// `lance_graph_contract::set_algebra::normalize` (absorption against
+/// flattened siblings and sub-junctions), which relalg now delegates to; this
+/// pin flipped with it. Not fixed in the optimizer. This spike never builds the
+/// shape: it only emits an `And` of planes (no `Not`, no `Or`).
 #[test]
-fn m_the_known_absorption_gap_is_untouched_and_not_produced() {
+fn m_the_known_absorption_gap_is_closed_and_not_produced() {
     let absorbed = |x: Rel| {
         let e = Rel::Not(Box::new(Rel::And(vec![
             x.clone(),
@@ -691,12 +692,12 @@ fn m_the_known_absorption_gap_is_untouched_and_not_produced() {
     };
     assert!(absorbed(Rel::Plane(0)), "leaf x reduces");
     assert!(
-        !absorbed(Rel::And(vec![Rel::Plane(0), Rel::Plane(2)])),
-        "compound x: fixed upstream? update this pin"
+        absorbed(Rel::And(vec![Rel::Plane(0), Rel::Plane(2)])),
+        "compound x (And) must reduce since D-CMR-1"
     );
     assert!(
-        !absorbed(Rel::Or(vec![Rel::Plane(0), Rel::Plane(2)])),
-        "compound x: fixed upstream? update this pin"
+        absorbed(Rel::Or(vec![Rel::Plane(0), Rel::Plane(2)])),
+        "compound x (Or) must reduce since D-CMR-1"
     );
     // What this spike produces: duplicates collapse, nothing widens.
     let ours = Rel::And(vec![Rel::Plane(0), Rel::Plane(1), Rel::Plane(0)]);

crates/lance-graph-contract/src/lib.rs

@@ -190,6 +190,7 @@ pub mod scenario;
 pub mod scheduler;
 pub mod selection;
 pub mod sensorium;
+pub mod set_algebra;
 pub mod settlement;
 /// D-BLW-5 payload-law DTO (`ShapeRankPayload`, `RemeasureKey`, `RemeasureLedger`) —
 /// distribution shape × Prozentrang, never the raw statistic. See module docs.