D-CMR-2: lower the contract set algebra onto mask-risc (runs as extents, three levels); D-CMR-5 re-scoped

.claude/board/LATEST_STATE.md

@@ -1,3 +1,8 @@
+## 2026-10-21 — D-CMR-2 lowering in core (in PR)
+
+- **Core (new module, no contract change):** `lance_graph::fold::set_lower::{SetPlan, SortedBasis, Level, Measured, LowerError}`. A `SetExpr` is normalized (contract) and split into `Runs ∩ residual`: comparisons on an attested sorted `i32` lane (`SortedBasis`, one attestation scan) become runs by counted binary-search seeks; the rest compiles once to a mask-risc `Program` run over each run with `execute_extent`. Levels: geometry (no residual, `Count = Σ(hi−lo)`, nothing read), optics (`Count` terminal), etch (`Keep` into `Out::Mask`, outside bits cleared). `SetPlan::unsplit` is the geometry-off arm. Entry `entries/2026-10-21-d-cmr-2-lowering.md`.
+- Open: D-CMR-2b, a scratch-free `Pred` fold in mask-risc (`fused_ternlog` declines `Pred`); residual comparisons run tiled with per-tile scratch.
+
 ## 2026-10-21 — main after #1644 (merged `c05a313`)
 
 - **On main:** #1641 (D-RELALG-UNIFIED plan), #1643 (U1 `jc-batch-probe`, walk_mask follow-up), #1644 (D-CMR-1 / D-RA-2, `contract::set_algebra`; inventory delta below under 2026-10-20).

.claude/board/STATUS_BOARD.md

@@ -255,10 +255,10 @@ Plan: `.claude/plans/d-cmr-concept-chain-normalization-v1.md`. Parent: D-CMR-RES
 |---|---|---|---|
 | **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 | Shipped (#1644, `c05a313`): `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-2** | Lowering: runs → extents, residual → predicates per run; measurement levels geometry / optics / etch | In PR (branch `claude/eager-albattani-iufugq`): `lance_graph::fold::set_lower::{SetPlan, SortedBasis, Level, Measured}`; geometry reads nothing, optics/etch run the residual per run via `execute_extent`. The scratch-free `Pred` fold in mask-risc is D-CMR-2b, not built (`entries/2026-10-21-d-cmr-2-lowering.md`) | == 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 |
-| **D-CMR-5** | **⛔ VIOLATION — GATHER. DO NOT BUILD. CORRECT: D-HOLO-H14c / H14d.** Preimage `f⁻¹(S)` under a proven mapping (the hop) | Queued | == row oracle; many-to-one image refused |
+| **D-CMR-5** | **BLOCKED: lawful design proposed (operator 2026-10-21).** Preimage `f⁻¹(S)` as a co-addressed transposed tile fold over a version-witnessed projection of `f`, built in preparation by a sequential same-table scan with frozen-codebook endpoint translation (ADMISSION B; reusable across queries). `S` enters only as a membership plane translated into the same frozen coordinates. No seek or load of `f` keyed by `S`'s values or a previous fold (Q1 = C), no `Gather`, no scatter terminal. R1 (`rmap` `rebind` / `discover` escape-driven seeks) stays option C. ⊘ Was: "VIOLATION — GATHER. DO NOT BUILD" (entry `2026-10-21-d-cmr-5-rescope.md`) | BLOCKED — needs a contract-level attested witness for the frozen codebook (`rmap::Witness` is a probe-local stand-in); no preimage operator exists; not admitted, not ready to build | == row oracle; program checked Gather-free with a silence twin; attest / projection / query costs reported apart; a many-to-one `f` gives a valid distinct-source preimage (tested) and a bag-sensitive Count/Sum over it is refused (tested); refusal on a stale or missing witness |
 | **D-CMR-6** | Rule catalogue + fixpoint driver: complement, relational difference | Queued | Experiments A, D, E; each guard removal fails |
 | **D-CMR-7** | NAL frontend: aperture → `Runs` | Queued (after NAL lands in core) | NAL W2 tests unchanged |
 | **D-CMR-8** | Equality-saturation probe (`egg`/`egglog` as references) | Queued (only if rules compete) | compared against D-CMR-6; no dependency without evidence |

.claude/board/entries/2026-10-21-d-cmr-2-lowering.md

@@ -0,0 +1,21 @@
+# 2026-10-21 — D-CMR-2: the contract set algebra lowered onto mask-risc
+
+**Status:** TEST-PINNED (in PR, branch `claude/eager-albattani-iufugq`). **Basis:** plan `d-cmr-concept-chain-normalization-v1.md` §3.4 and the D-CMR-2 row; ADMISSION B (`2026-10-20-six-decisions.md` §1) for the seeks.
+
+- **Where:** `crates/lance-graph/src/fold/set_lower.rs` (`lance_graph::fold::set_lower`). Core already depends on the contract and mask-risc unconditionally; no new dependency.
+- **Split:** `SetPlan::new(&SetExpr, n_rows, Option<&SortedBasis>)` normalizes, then takes `Runs` from comparisons on the attested sorted lane (an exact basis-only expression, or the basis conjuncts of a top-level `And`) and leaves the rest as the residual. Mixed `Or`s stay residual and spend no seeks.
+- **Costs apart:** `SortedBasis::attest_reads` (one scan, n keys), `SetPlan::seeks` (one binary search per boundary), `Measured::{extents, extent_rows}` (query side).
+- **Levels:** geometry answers from the runs alone; optics runs the residual program (`Count`) per run via `execute_extent`; etch runs it with `Keep` into `Out::Mask`, bits outside the runs cleared.
+- **Tests (6):** 400 random nested expressions over a sorted basis lane, an unsorted lane, a code lane and two planes (N = 1000, not a word multiple): count and set equal the row oracle at every level and for `unsplit`, both levels exercised, runs narrow the extents (anti-vacuity). Geometry runs against `Planes` with no lanes and no masks and reports 0 extents (≤ 6 seeks). Experiment C (basis range + unsorted predicate → one run + residual, extent under half the rows). Non-basis range stays residual (silence twin). Unsorted basis and row-count mismatches refused.
+- **Disable runs** (`cargo test -p lance-graph --lib set_lower`):
+
+  | probe | red |
+  |---|---|
+  | geometry off (no residual still runs a program) | `geometry_reads_no_plane_lane_or_extent` |
+  | split off (`new` = `unsplit`) | geometry, Experiment C, oracle anti-vacuity |
+  | basis-lane check off (any lane's comparison becomes runs) | Experiment C, silence twin, oracle |
+  | `keep` does not clear the destination | oracle (`keep`) |
+
+- **Not done:** D-CMR-2b, a scratch-free `Pred` fold in mask-risc. `fused_ternlog` declines `Pred`, so a residual comparison runs tiled with per-tile scratch (bounded by `TILE_WORDS`, never population-sized). No rows/words-read counter exists in mask-risc; the geometry claim is proven by running against empty planes instead.
+
+OPEN: D-CMR-2b (mask-risc fused predicate fold; changes `ir.rs` / `exec.rs`, coordinate on EXO-50 first); a `u32` / facet sorted basis (`SealedFacetLane`) instead of an `i32` lane.

.claude/board/entries/2026-10-21-d-cmr-5-rescope.md

@@ -0,0 +1,17 @@
+# 2026-10-21 — D-CMR-5 re-scoped: preimage via frozen coordinates, still BLOCKED
+
+**Status:** DECISION (operator, 2026-10-21, in session `session_013z2e1YXkm6o6HNrDn5BPWA`; also relayed on EXO-50 as `gpt-ada-01/003`). **Basis:** read-only check of D-CMR-5 against the global→local registers (this session; `crates/mork-pathmap-probe/src/rmap.rs`, `crates/crepe-plan-probe/examples/walk_tile.rs`), the ADMISSION ruling (`2026-10-20-six-decisions.md` §1).
+
+Operator's words: "Der entscheidende Unterschied ist, ob ein Wert nur in eine bereits festgelegte Koordinate übersetzt wird oder darüber bestimmt, welche Zeile einer Relation gelesen wird."
+
+| question | ruling |
+|---|---|
+| Q1: seek `f`'s attested sorted key with range bounds taken from `S` (or a previous fold) | **C, not admitted.** Foreign values steer the reads of `f`; a sorted index and doing it in preparation change nothing. Independent literal / intrinsic same-table key-range seeks on `f` stay B. |
+| Q2: translate `S`'s global ids into tile coordinates through a frozen codebook | **B, conditionally.** Pure representation translation, provided it only produces an `S` membership plane, triggers no relational access to `f`, and the mapping is attested, version-bound and fully accounted. |
+
+- **Design direction (not an admission):** a once-built, version-bound projection of `f` (sequential same-table scan, frozen-codebook endpoint translation) may be reused across queries; `S` is translated into the same coordinates; `f⁻¹(S)` is a co-addressed transposed fold. Reading `f` selectively by the values found in `S` stays forbidden.
+- **Two existing registers:** R1 (`rmap` `Focus` + `Csr` + `rebind`) seeks with escapes / values from another column, so it stays option C and is not legalized. R2 (`walk_tile`, D-RU-6) has the admissible shape, but its witness is the probe-local `rmap::Witness`.
+- **Many-to-one:** not an error for the set-valued preimage; `Count(f⁻¹(S))` over distinct source coordinates is valid. Refuse a bag-sensitive aggregation that set deduplication would destroy, unless a separately proven multiplicity-preserving aggregation exists.
+- **Still BLOCKED:** no contract-level attestation for the codebook; no preimage operator exists (`rmap::hop` computes the image). The plan row's former "CORRECT: H14c/H14d" pointed at the co-addressing principle, not a hop implementation.
+
+OPEN: the contract-level codebook witness (version, map generation / seal, coordinate-domain identity, scope / completeness, invalidation).

.claude/board/entries/README.md

@@ -25,12 +25,14 @@ 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.
 
-399 entries, 2026-08-06 .. 2026-10-21.
+401 entries, 2026-08-06 .. 2026-10-21.
 
 | date | entry id | finding | file |
 |---|---|---|---|
 | 2026-10-21 | `D-RU-6-LAB-1` |  | [2026-10-21-d-ru-6-tile-walk-probe.md](2026-10-21-d-ru-6-tile-walk-probe.md) |
 | 2026-10-21 | `D-RU-6-LAB-2` |  | [2026-10-21-d-ru-6-sparse-compute.md](2026-10-21-d-ru-6-sparse-compute.md) |
+| 2026-10-21 | `D-CMR-5` |  | [2026-10-21-d-cmr-5-rescope.md](2026-10-21-d-cmr-5-rescope.md) |
+| 2026-10-21 | `D-CMR-2` |  | [2026-10-21-d-cmr-2-lowering.md](2026-10-21-d-cmr-2-lowering.md) |
 | 2026-10-20 | `D-RU-1` |  | [2026-10-20-u1-jc-batch.md](2026-10-20-u1-jc-batch.md) |
 | 2026-10-20 | `thought-git-replay-api-write-rubicon` |  | [2026-10-20-thought-git-replay-api-write-rubicon.md](2026-10-20-thought-git-replay-api-write-rubicon.md) |
 | 2026-10-20 | `ADR-2026-10-20-SIX` |  | [2026-10-20-six-decisions.md](2026-10-20-six-decisions.md) |

.claude/plans/d-cmr-concept-chain-normalization-v1.md

@@ -213,7 +213,7 @@ when the first floating-point or quantized column arrives, not before.
 | D-CMR-2 | **Lowering** to mask-risc: runs → extents, residual → predicates within each run, the three measurement levels. Level 2 for residual comparisons needs predicate fusion in mask-risc (`fused_ternlog` declines `Pred` today) | == row oracle; a `Count` with no residual reads zero rows (instrumented); disabling level 1 or 2 keeps answers |
 | D-CMR-3 | **Quack normalization pass:** over `Filter`, computing set values (ranges on a proven basis → `Runs`, other leaves → `Res`, `sql_where` first). Extent hoisting falls out of this (Experiment C) | answers identical to today's `lower` path on the quack suite; a range on another basis stays residual (negative control) |
 | D-CMR-4 | **Two dimensions:** `Rect` over composite coordinates, linearized row-major or in Morton order | rectangle `∩` == bitset oracle; run count within the stated bound |
-| D-CMR-5 | **⛔ VIOLATION — GATHER. CORRECT: `d-holo-h14c-thought-first-v1.md` / `d-holo-h14d-logic-mask-read-v1.md`.** **Preimage** `f⁻¹(S)` under a proven mapping (the hop) | == row oracle; a many-to-one image is refused |
+| D-CMR-5 | **BLOCKED: lawful design proposed (operator 2026-10-21).** Preimage `f⁻¹(S)` as a co-addressed transposed tile fold over a version-witnessed projection of `f`, built in preparation by a sequential same-table scan with frozen-codebook endpoint translation (ADMISSION B; reusable across queries). `S` enters only as a membership plane translated into the same frozen coordinates. No seek or load of `f` keyed by `S`'s values or a previous fold (Q1 = C), no `Gather`, no scatter terminal. R1 (`rmap` `rebind` / `discover` escape-driven seeks) stays option C. ⊘ Was: "VIOLATION — GATHER. DO NOT BUILD" (entry `2026-10-21-d-cmr-5-rescope.md`) | == row oracle; program checked Gather-free with a silence twin; attest / projection / query costs reported apart; a many-to-one `f` gives a valid distinct-source preimage (tested) and a bag-sensitive Count/Sum over it is refused (tested); refusal on a stale or missing witness |
 | D-CMR-6 | **Rule catalogue and fixpoint driver**: complement, relational difference `Sum(A) − Sum(A∧B) → Sum(A∧¬B)` | Experiments A, D, E; each guard removal fails |
 | D-CMR-7 | **NAL normalization pass:** aperture → `Runs` over the R2IL program, R2IL route unchanged (after NAL lands in core) | NAL W2 tests unchanged |
 | D-CMR-8 | **Equality-saturation probe** (`egg`, `egglog` as references only) | only if rules compete; compared against D-CMR-6; no dependency without evidence |

crates/lance-graph/src/fold.rs

@@ -11,5 +11,10 @@
 //! A capability that is missing here is missing in one of the three crates.
 
 pub use lance_graph_mask_risc as mask_risc;
+
+/// D-CMR-2: the contract's set algebra lowered onto mask-risc (runs as
+/// extents, residual as a program, three measurement levels). A lowering,
+/// not a second algebra: the rules live in `lance_graph_contract::set_algebra`.
+pub mod set_lower;
 pub use lance_graph_quack as quack;
 pub use lance_graph_r2il as r2il;