diff --git a/.claude/board/IDEAS.md b/.claude/board/IDEAS.md index 9640dc320..8bb8e7775 100644 --- a/.claude/board/IDEAS.md +++ b/.claude/board/IDEAS.md @@ -283,6 +283,7 @@ deduplicated set where MeTTa returns a bag. `[P2 domain:dr-math D-DRMC]` After X15, `dr-math-binding-probe` admits a recipe only through an opaque `RecipeCertificate` that a certified compiler issues; none exists, so every admission ends in `NoCertifiedCompiler` (`entries/2026-10-22-coresearch-drmc-stack.md` § Applied, #1703). The boundary needs three parts: a typed relational statement language over ClassView domains, egglog laws over it whose proofs a checker independent of the producer re-checks, and a check that the lowering preserves the statement. First law: associativity of Boolean relation composition, already measured as a probe (D-DRMC-5, #1707: 14 orders, one relation). Kill: the statement language cannot type the composition D-DRMC-5 already runs. Scope question for the operator: how far the boundary goes (LEDGER-REVISION-2026-10-23e Q2). +**Amended 2026-10-23 (D-ONNX-RELALG-CAP S0):** "none exists" is scoped too broadly. The single-operand `admit_recipe` path still ends in `NoCertifiedCompiler` (`recipe.rs`). `relcomp::certify_reassociation` (#1707) IS an issuer: it covers associativity of Boolean-Distinct relation composition, egglog-proved, digest-bound (correction #1738), and its certificates re-execute on fresh frames (#1740). Still missing: an independent proof checker; any second law; the multi-binding catalogue; any production path. The egglog dependency floats on `branch = "main"`, and no certificate field names the prover revision. **Fruit:** Heavy **Status:** Open @@ -291,6 +292,7 @@ After X15, `dr-math-binding-probe` admits a recipe only through an opaque `Recip `[P1 domain:dr-math D-DRMC]` Pre-registered in `entries/2026-10-22-coresearch-drmc-stack.md`, none run. X6: `validity: None` must refuse or report `Unattested`, never silently mean all-known. X7: a compile-fail test that no `PopulationReport` → premise conversion exists. X8: two certified bindings for one key (today the first falls back). X16: a law found on class 1 must not reach class 22 (2 counterexamples) unchecked. X18: a census may veto ACT-R eligibility, never qualify it. Each is one falsifier on an existing crate; X6, X7 and X18 are the cheapest. +**Amended 2026-10-23 (D-ONNX-RELALG-CAP S0):** one half of X8 has run. #1740 (`c42140b7`, `dr-math-binding-probe/tests/x8_fresh_frame.rs`, 7/7) re-executes a D-DRMC-5 certificate on independently issued fresh frames with 0 egglog calls. The half named above, two certified bindings for one key in the `egglog-r2il-probe` catalogue (whose `insert` overwrites), is untouched: #1740 changes no catalogue file. X6, X7, X16 and X18 are still unrun. **Fruit:** High-signal **Status:** Open diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index ac14b2832..233d3810c 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,7 @@ +## 2026-10-23 — d-onnx-relalg-cap-v1 — ONNX as an import membrane over the existing substrate → `.claude/plans/d-onnx-relalg-cap-v1.md` + +**Status:** PROPOSAL, documentation only (S0). S1..S5 PLANNED, not authorized. The original DR64³ plan was not found; the DR64³ section is a new, labelled proposal. relalg takes only the Boolean/compare/reduce fragment; the home for value maths is OPEN (OP-ONNX-1), and so is the importer dependency (OP-ONNX-2). Entry: `entries/2026-10-23-d-onnx-relalg-cap-s0.md`. + ## 2026-10-23 — catch-up: plans from #1660–#1708 had no index entry **Status:** INDEX CATCH-UP; no plan status changes. Each status below is the plan's own status line on `main` at `b342d47c`. diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index f3f668af4..681f89c5a 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,7 +1,7 @@ ## 2026-10-23 — main after #1741 (merged `59538865`) -- **On main since #1725:** L1 for D-DRMC-5 (#1740): a reassociation certificate executes on a fresh frame without egglog. The Julia e-graphs coresearch map (#1741). #1726–#1739 have no per-PR records yet. -- **Contract inventory delta:** none; lab crates and board only. +- **On main since #1725:** Palette256 compose and learned-LUT probes (#1726, #1731), the BREADCRUMBS / TORQUE / GOLDSTAUB ledgers and `fruits_index.py` (#1729), the thought-git squash gate and Probe D (#1736, #1739, lab, `thought-git-probe`), the D-DRMC-5 fresh-frame reuse L1 (#1740, lab, `dr-math-binding-probe`), the "no certified compiler" scope correction (#1738), and coresearch maps (#1737, #1741). Per-PR records: `PR_ARC_INVENTORY.md`. +- **Contract inventory delta:** none. Every PR in this range is a lab crate, a probe, a ledger or a board entry. ## 2026-10-23 — main after #1725 (merged `b342d47c`) diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md index 2d40aff70..c6fa43ea1 100644 --- a/.claude/board/PR_ARC_INVENTORY.md +++ b/.claude/board/PR_ARC_INVENTORY.md @@ -1,5 +1,7 @@ + + ## 2026-10-23 — lance-graph PR #1741 (merged `59538865`, branch `board/coresearch-julia-egraphs-20261023`, head `dcef8cc1`) — board: coresearch map, Julia e-graphs vs egglog/datafrog/Ascent; Lisp vs Prolog for MeTTa - **Added:** board only. @@ -14,6 +16,52 @@ - **Docs:** entries `2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md`, `…-result.md`. - **Confidence:** MEASURED (lab). +## 2026-10-23 — lance-graph PR #1739 (merged `9a458cae`, branch `ccr-d3ce1263-ied9yh`, head `52fab2cd`) — thought-git-probe: Probe D (D-TGA-5D), protected readers of a squash + +- **Added:** `crates/thought-git-probe` (`src/lib.rs`, new `src/squash.rs`, `tests/protected_readers.rs`, `tests/squash_gate.rs`); the D-TGA-5 squash gate moved into `src/squash.rs`; probe renamed D-TGA-6 -> D-TGA-5D. +- **Docs:** entry `2026-10-23-d-tga-5d-protected-readers-preregistration.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1738 (merged `05b3516e`, branch `ccr-d3ce1263-ied9yh`, head `dca7c758`) — correction: "no DR64 certificate" scoped to the single-operand admit_recipe path + +- **Added:** correction in `crates/dr-math-binding-probe/RECIPE_ADMISSION.md` and in `entries/2026-10-23-coresearch-thought-git-markov.md`: `relcomp::certify_reassociation` (#1707) issues certificates; only `admit_recipe` ends in `NoCertifiedCompiler`. No code. +- **Locked / deferred:** see the PR body; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1737 (merged `64bd1902`, branch `board/coresearch-thought-git-markov-20261023`, head `38989f66`) — board: /coresearch map — thought-git accumulation as a large Markov chain (CC2 map and gap map) + +- **Added:** board only. +- **Docs:** entries `2026-10-23-coresearch-thought-git-markov-cc2.md`, `2026-10-23-cc2-proof-compiling-gap-map.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1736 (merged `1b87a27e`, branch `ccr-d3ce1263-ied9yh`, head `6ad966d1`) — probe(D-TGA-5): squash the chain of origin into the most-updated lane, gated on contradiction; blame survives + +- **Added:** `crates/thought-git-probe/tests/squash_gate.rs`; board IDEAS/FRUITS/STATUS_BOARD rows. +- **Docs:** entries `2026-10-23-d-tga-5-squash-gate-preregistration.md`, `2026-10-23-coresearch-thought-git-markov.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1731 (merged `55e6777a`, branch `lab/exo129-learned-lut-composition-20261023`, head `e207e5ca`) — probe(EXO-129): a learned 256×256 table does not compose where the codebook is not closed + +- **Added:** `crates/bgz-tensor/tests/exo129_learned_lut_probe.rs`. +- **Docs:** entry `2026-10-23-exo129-learned-lut-preregistration.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1729 (merged `8f610a85`, branch `board/ledgers-torque-goldstaub-20261023`, head `4a3685f1`) — board: BREADCRUMBS / TORQUE / GOLDSTAUB ledgers, amended closeout table, generated FRUITS.md + +- **Added:** `.claude/board/{BREADCRUMBS,TORQUE,GOLDSTAUB,FRUITS}.md`; `.claude/tools/append_only_gate.py`, `.claude/tools/fruits_index.py`; `.github/workflows/append-only-gate.yml`; `CLAUDE.md` closeout-table amendment; `.claude/BOOT.md`, `.claude/settings.json`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1726 (merged `19c1324a`, branch `lab/ps2-pl3-lut-composition-20261023`, head `9f1370b2`) — probe(P-S2): a Palette256 compose table does not survive two hops + +- **Added:** `crates/bgz-tensor` (`src/attention.rs`, `tests/p_s2_compose_chain_probe.rs`). +- **Docs:** entry `2026-10-23-ps2-compose-chain-preregistration.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. ## 2026-10-23 — lance-graph PR #1725 (merged `b342d47c`, branch `lab/pd4-refit-base-rate-20261022`, head `57fbec40`) — probe(P-D4): refit the base rate inside each bootstrap draw; the post-hoc gate does not pass diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index d75554930..2a9fe79e0 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,13 @@ +## D-ONNX-RELALG-CAP — ONNX as import membrane (2026-10-23) + +Plan `d-onnx-relalg-cap-v1.md`, PROPOSAL. Only S0 is in a PR. + +| D-id | scope | status | gate / falsifier | +|---|---|---|---| +| **D-ONNX-0** | S0 capstone plan, coverage matrix, open-points register OP-ONNX-1..14 | In PR (docs only) | consistent with code at `59538865`; no DR64³ claim | +| **D-ONNX-1** | S1 intake probe: ONNX-subset reader with typed refusals; Boolean/compare/reduce fragment onto relalg | Queued (not authorized) | onnxruntime differential (a test, not a proof); waits on OP-ONNX-1, OP-ONNX-2 | +| **D-ONNX-3** | S3 DR64³ R1/R2 contraction probe (new proposal) | Queued (not authorized) | four arms bit-exact; waits on OP-ONNX-4 | + ## D-DRMC — DR × math binding probe, law frontier (2026-10-23) Lab only (`crates/dr-math-binding-probe`). Charter and probes: #1700, #1707, #1708; L1 in #1740. @@ -394,8 +404,8 @@ Plan: `.claude/plans/ce64-hypothesis-layers-v1.md`. Plateau: `.claude/knowledge/ | **D-TGA-2** | Read plane R and status | Queued | a read outside R is never reported stale | | **D-TGA-3** | rebase (four masks, no data moved) | Queued | rebase-then-squash == from-scratch re-run on v+1, including a deletion in main (retract then re-derive); disables: no stale re-run, no conflict check, no retraction | | **D-TGA-4** | land through the revision gate into the next Lance version (D-HL-8) | Queued | landing a thought that is behind is refused | -| **D-TGA-5** | squash_into (partial squash) and blame | Shipped (lab, #1736: `crates/thought-git-probe/src/squash.rs` + `tests/squash_gate.rs`, `entries/2026-10-23-d-tga-5-squash-gate-preregistration.md`; most-updated target, contradiction/divergence gate, blame over lanes, P8 Commit-only, 6 disables red) | blame returns original sources after slot reuse (slot reuse not yet covered) | -| **D-TGA-5D** | Probe D: protected readers of a squash (Final / Intermediate / Contradictions / Divergences / Multiplicity) | In PR (lab: `tests/protected_readers.rs`, `entries/2026-10-23-d-tga-5d-protected-readers-preregistration.md`; 7 tests, 5 disables red) | a protected reader the retained data cannot answer refuses the squash; intermediate reads are never retainable | +| **D-TGA-5** | squash_into (partial squash) and blame | Shipped (lab, #1736: `crates/thought-git-probe/tests/squash_gate.rs`; the gate moved into `src/squash.rs` in #1739; `entries/2026-10-23-d-tga-5-squash-gate-preregistration.md`; most-updated target, contradiction/divergence gate, blame over lanes, P8 Commit-only, 6 disables red) | blame returns original sources after slot reuse (slot reuse not yet covered) | +| **D-TGA-5D** | Probe D: protected readers of a squash (Final / Intermediate / Contradictions / Divergences / Multiplicity) | Shipped (lab, #1739 merged `9a458cae`: `crates/thought-git-probe/src/squash.rs` + `tests/protected_readers.rs`, `entries/2026-10-23-d-tga-5d-protected-readers-preregistration.md`; 7 tests, 5 disables red) | a protected reader the retained data cannot answer refuses the squash; intermediate reads are never retainable | | **D-TGA-6** | MergeQueue | Queued | independent thoughts == landed by hand in FIFO order; a thought reading another negated lands after it; a cycle through negation refused at enqueue | | **D-TGB-0** | thought git basics: fixtures per write-intention outcome, squash-stack and anomaly fixtures, absent-not-zero fixture, from-scratch oracle (`thought-git-basics-v1.md`) | Shipped (lab, #1630; probe `crates/thought-git-probe`, 19 tests; `PREREGISTRATION.md`) | 5 oracle disables verified red-then-green; every signal has a can-fire and a can-stay-silent case on real contract code; the pearl half on edges moves to D-TGB-3 | | **D-TGB-1** | slot pool, autonomous: taken by `branch`, freed by `squash`/`discard`/`land` (the write is the Rubicon decision, 2026-10-20) | Shipped (lab, #1630/#1631; `crates/thought-git-probe/src/slots.rs`). Slot pool only: no production land, rebase or persistence (D-TGB-2..5 Queued) | at 63 taken `branch` picks a FIFO or least-used candidate, squashes it along its dependency chain if it has one, else evicts it (DECISIONS 2026-10-20; was: squash unremarkable first, else refuse); stale handles refused; 6 tests | diff --git a/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md b/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md new file mode 100644 index 000000000..c136d3a12 --- /dev/null +++ b/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md @@ -0,0 +1,41 @@ +# 2026-10-23 — D-ONNX-RELALG-CAP — S0 result: ONNX as import membrane, DR64³ plan not found + +**Status:** S0 documentation; no code. Plan: `.claude/plans/d-onnx-relalg-cap-v1.md`. Read at `origin/main` `59538865`; ONNX facts at upstream commit `0c8af065` (ONNX 1.23.0 = IR 14, ai.onnx opset 28; default domain 203 operators, 155 ops + 48 functions; `ai.onnx.ml` 19). + +## What was searched + +- The repo for `DR64³`, `DR256³`, `64×64×64`, `64x64x64` (`grep -rIl`). +- Branches and PRs: branch `ccr-e97e5d58-1bkumg-cartesian12`; GitHub PR search "cartesian". +- Rust crates for any ONNX dependency (onnx/ort/tract/burn/rten/onnxruntime/wonnx/inkwell/llvm/cranelift) and for `ModelProto`/`GraphProto`/opset in `*.rs`. +- relalg, R2IL, mask-risc, contract set algebra, `dr-math-binding-probe`, `dir-rmap-probe` (read with file:line). + +## What was found + +- DR64³ / DR256³ original plan: NOT FOUND. 0 files contain any of the strings. The branch above is CartesianAddress12/Quad8 shader work. 23 "cartesian" PRs, none is a DR64³ plan. The 12-stage PR sequence is not found. The one 18-bit figure in the repo is the "18-bit hot envelope = 262,144" mailbox working set (`.claude/knowledge/delta-card-addressing-integration-map.md`), a working-set size, not an identity. Other 262144 hits are byte counts, CSV values and index spaces. +- The plan's DR64³ section is a NEW, labelled proposal (R1 chain contraction, R2 triangle), not recovered history. Sizes 32 KiB / 2 MiB are arithmetic only. +- No ONNX dependency or parser exists in the Rust tree. onnxruntime 1.29.0 is installed in the container's Python; protoc 3.21.12 is installed; `onnx.reference` cannot run without the C++ extension. +- relalg is single-table Boolean selection plus four I32 aggregates (`crates/lance-graph-relalg/src/ir.rs`). The "mathematical polyfill landing zone" proposal holds only for the Boolean/compare/reduce fragment. + +## BLOCKING corrections adopted (opusC) + +1. B1: ONNX is an import membrane only; no new AST, no ONNX rewrite pass or interpreter. "Mathematical polyfill landing zone" is dropped. +2. B2: per-op admission table, default REFUSED; value-derived addressing ops (`Gather*`, `Scatter*`, `NonZero`, `Unique`, `Compress`) refused under ADMISSION B. +3. B3: no float law admitted; float ops lower as written or are refused. +4. B4: every stage has a proof-engine column; "certified" only for egglog-proved Boolean-Distinct composition associativity (#1707, reuse #1740); the "256³ Validate" stage is a differential test. + +## Open points + +- OP-ONNX-1: home for value maths (operator). +- OP-ONNX-2: importer dependency options A-E (operator). +- OP-ONNX-3: DR64³/DR256³ original plan missing. +- OP-ONNX-4: bit-position scan versus D-RU-6 / ADMISSION B. +- OP-ONNX-5: no independent proof checker. +- OP-ONNX-6: certificate rebinding beyond #1740 (focus/scope/ABI/geometry). +- OP-ONNX-7: prover revision not recorded (egglog `branch = "main"`): a certificate-identity gap, not a dependency defect. +- OP-ONNX-8: onnxruntime int32 `ReduceSum` saturation unexplained. +- OP-ONNX-9: `dr-mathematical-compiler-v1.md` calls egglog's self-check "independent". +- OP-ONNX-10: `dr-mathematical-compiler-v1.md` versus D-RA-2. +- OP-ONNX-11..13: R2 closing-view check placement; `observe_focus` scope omission; refusal granularity and strings in the contract. +- OP-ONNX-14: which proof object datafrog, Ascent or MeTTa/MORK/PathMap would produce; the operator rule names them, but only egglog produces one here today. + +D-ONNX-RELALG-CAP | STATUS: open | OUTCOME: S0 plan and this entry; 4 BLOCKING corrections adopted; DR64³ original plan not found | OPEN: OP-ONNX-1..14 diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index b2a1176c8..08cd9ef8d 100644 --- a/.claude/board/entries/README.md +++ b/.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. -453 entries, 2026-08-06 .. 2026-10-23. +454 entries, 2026-08-06 .. 2026-10-23. | date | entry id | finding | file | |---|---|---|---| @@ -37,6 +37,7 @@ exactly one of them, never both. | 2026-10-23 | `EXP-DRMC-L1-PREREG` | L1 (CC2 Law Frontier): a certified reassociation reused on a fresh frame (D-DRMC-5 + X8) — pre-registration | [2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md](2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md) | | 2026-10-23 | `D-TGA-5D` | | [2026-10-23-d-tga-5d-protected-readers-preregistration.md](2026-10-23-d-tga-5d-protected-readers-preregistration.md) | | 2026-10-23 | `D-TGA-5` | | [2026-10-23-d-tga-5-squash-gate-preregistration.md](2026-10-23-d-tga-5-squash-gate-preregistration.md) | +| 2026-10-23 | `D-ONNX-RELALG-CAP` | S0 result: ONNX as import membrane, DR64³ plan not found | [2026-10-23-d-onnx-relalg-cap-s0.md](2026-10-23-d-onnx-relalg-cap-s0.md) | | 2026-10-23 | `coresearch-thought-git-markov` | | [2026-10-23-coresearch-thought-git-markov.md](2026-10-23-coresearch-thought-git-markov.md) | | 2026-10-23 | `coresearch-thought-git-markov-cc2` | | [2026-10-23-coresearch-thought-git-markov-cc2.md](2026-10-23-coresearch-thought-git-markov-cc2.md) | | 2026-10-23 | `coresearch-julia-egraphs` | | [2026-10-23-coresearch-julia-egraphs.md](2026-10-23-coresearch-julia-egraphs.md) | diff --git a/.claude/plans/d-onnx-relalg-cap-v1.md b/.claude/plans/d-onnx-relalg-cap-v1.md new file mode 100644 index 000000000..e22bde8de --- /dev/null +++ b/.claude/plans/d-onnx-relalg-cap-v1.md @@ -0,0 +1,187 @@ +# D-ONNX-RELALG-CAP — ONNX as import membrane over the existing substrate (S0) + +**Status:** PROPOSAL, documentation only, 2026-10-23. No code in this plan's PR. Read at `origin/main` `59538865`. ONNX facts are read from the upstream clone at commit `0c8af065` and cited as `onnx::line`. Stages S1..S5 are PLANNED and not authorized. + +**Corrected statement (replaces the original proposal wording).** ONNX is a read-only interchange membrane. An imported model is refused unless every op is in an explicit admitted subset. Admitted ops lower, as written, onto existing contract set-algebra forms and R2IL/Quack/mask-risc terminals through relalg's planning and lowering. Value-indexed ops (`Gather*`, `Scatter*`, `NonZero`, `Unique`, `Compress`), training graphs and float reassociation are refused. The only certified law remains Boolean-Distinct reassociation (egglog, #1707). Every other stage is a differential test. DR64³ and DR256³ are unimplemented proposals with no measured figures. (Source: opusC, "Minimal corrected capstone sentence", adjusted to add `Compress`, which opusA §1 lists as unsupported.) + +**Operator rule (binding), from the brief:** "There is no proof without egglog / eggcc / datafrog / ascent, or at least MeTTa over MORK over a PathMap oracle. Anything planned past it is a hallucination." Hand-written Rust reference evaluators and onnxruntime differentials are TESTS, not proofs. + +**The proposal "lance-graph-relalg is the mathematical polyfill landing zone" holds ONLY for the Boolean/compare/reduce fragment** (opusA §2). Value mathematics (arithmetic, `MatMul`, `Exp`/`Tanh`/`Mish`) has NO existing home. That is an OPEN decision for the operator (OP-ONNX-1), not a gap to fill silently. + +D-RA-2, verbatim (`.claude/plans/d-relalg-unified-v1.md`): "D-RA-2 = A: Die kanonische Single-Table-Set-Algebra und ihre Rewrite-Regeln gehören in `lance-graph-contract`. `relalg` behält Lowering und relationale Planung. Keine allgemeine relationale AST für JC oder Quack einführen." + +## 1. What exists + +| Capability | State | Evidence | +|---|---|---| +| relalg `Rel` = All/Empty/Plane/Atom/And/Or/Not; `Measure` = Count/Sum/Min/Max/Keep over I32 lanes | SHIPPED | `crates/lance-graph-relalg/src/ir.rs` | +| relalg atoms compare a lane to a constant only (`I32{lane,op,t}`, `U32{lane,eq,v}`) | SHIPPED | `crates/lance-graph-relalg/src/ir.rs` | +| relalg normalize delegates to the contract set algebra | SHIPPED | `crates/lance-graph-relalg/src/normalize.rs` | +| relalg lowers through R2IL `FoldDialect` to mask-risc; "recursion (μ) and the hop (preimage) are not built" | SHIPPED / NOT BUILT | `crates/lance-graph-relalg/src/lib.rs` | +| relalg is "Not a third frontend syntax" | CHARTER | `crates/lance-graph-relalg/src/lib.rs` | +| relalg value arithmetic, matmul, nonlinear functions | NOT BUILT | BRIEF verified facts (`join_body.rs` is a GYO alpha-acyclicity check only) | +| mask-risc lanes `I32\|U32\|U64\|Strided`, no float lane | SHIPPED | `crates/lance-graph-mask-risc/src/value.rs` | +| R2IL scalar arithmetic is scalar×scalar; lane-vs-lane refused `LaneVersusLane` | SHIPPED | `crates/lance-graph-r2il/src/lib.rs` | +| R2IL refuses `BLEND`, `SCATTER_OR` (`Unimplemented`) and unsigned `IntLess`/`IntLessEqual` (`NoUnsignedLaneCompare`) | SHIPPED (refusals) | `crates/lance-graph-r2il/src/lib.rs` | +| mask-risc `Terminal::BlendI32` kernel, not wired to relalg | LAB (kernel exists, unwired) | `crates/lance-graph-mask-risc/src/ir.rs` | +| Boolean-Distinct composition associativity certified by egglog (`admit_composition_assoc`, `prove_reassociation`, `certify_reassociation`) | SHIPPED (lab crate) | `crates/dr-math-binding-probe/src/relcomp.rs` | +| Certificate reuse on fresh frames, 0 egglog calls, 7/7 | SHIPPED (lab, #1740) | `crates/dr-math-binding-probe/tests/x8_fresh_frame.rs`; `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md` | +| DR64 register, `MethodSignature`/`Axis`, `Frame`/`Focus`/`Scope` guards | LAB | `crates/dr-math-binding-probe/src/lib.rs` | +| DR256 register (`SLOTS = 256`, `Row = [u64; 4]`), `Qr`, `Composer::compose` | LAB | `crates/dir-rmap-probe/src/focus.rs`; `src/qr.rs`; `src/compose.rs` | +| Independent proof checker | BLOCKED (none exists) | BRIEF; `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md` ("no independent proof checker") | +| eggcc | BLOCKED (docs/.arxiv only, no code) | BRIEF | +| datafrog, ascent, crepe, MORK, PathMap | LAB (deps/oracles) | BRIEF (crepe-plan-probe, lance-graph-metta, mork-pathmap-probe) | +| ONNX importer (any ONNX crate, `ModelProto`/`GraphProto`/`opset` in `*.rs`) | NOT BUILT | BRIEF: no crate depends on onnx/ort/tract/burn/rten/onnxruntime/wonnx/inkwell/llvm/cranelift; no `ModelProto`/`GraphProto`/opset in `*.rs` | +| bool-tensor ⇄ mask-plane pack/unpack | NOT FOUND (grep only) | opusA §1 facts, §6 item 5 | +| DR64³ / DR256³ plan or code | NOT FOUND | §6 below; BRIEF | + +## 2. Six distinct concerns and their owner surface + +| Concern | Owner surface in this repo | Source | +|---|---|---| +| Graph interchange | ONNX `ModelProto`/`GraphProto` read at the membrane only; no new AST | opusC B1; `onnx:docs/IR.md:35` | +| Mathematical semantics | `lance-graph-contract` set algebra (single-table); mathematical truth is the contract's | `crates/lance-graph-contract/src/set_algebra.rs`; `.claude/board/entries/2026-10-20-six-decisions.md` §2 | +| Addressing and binding | DR64 `MethodSignature`/`Axis`/`Frame`/`Focus`/`Scope` (lab); ClassView; ADMISSION = B | `crates/dr-math-binding-probe/src/lib.rs`; `.claude/plans/d-relalg-unified-v1.md` | +| Physical execution | R2IL `FoldDialect` → mask-risc; `ndarray::simd` kernels; Quack | `crates/lance-graph-relalg/src/lib.rs`; `crates/lance-graph-quack/src/lib.rs` | +| Learned transitions | typed methods over declared relationships, never a source of mathematical truth (operator rule in BRIEF); CausalEdge64 plasticity; ONNX `training_info` refused | BRIEF; `crates/causal-edge/src/layout.rs`; `onnx:docs/IR.md:110,515` | +| Proof and certification | egglog certificate for Boolean-Distinct composition only | `crates/dr-math-binding-probe/src/relcomp.rs` | + +## 3. ONNX coverage matrix (family level) + +Facts: default domain 203 operators (155 ops + 48 functions), `ai.onnx.ml` 19; ai.onnx opset 28 is the highest with a schema; IR 14 (scoutB §2-3; `onnx:docs/Versioning.md:204` row `1.23.0|14|28|5|1`). Classes: **D** directly representable (restricted), **C** compositionally representable, **K** needs a specialized physical kernel, **P** needs a mathematical polyfill (no home), **X** external backend, **R** refused. Default for every op not named here is **R**. + +Restriction for every D/C row: rank-1, length = `n_rows`, no broadcasting, int32/uint32/bool only, scalar constant right operand (opusA §1, last paragraph). Broadcasting is declared multidirectional (`onnx:docs/Operators.md:659`). + +| Family | Class | Lands on | Semantic difference | +|---|---|---|---| +| `Not`, `And`, `Or` (bool) | D | `Rel::Not/And/Or` → `Measure::Keep` → `INT_NOT/AND/OR` (`crates/lance-graph-relalg/src/lower.rs`) | broadcasting refused; bytes⇄bits pack is new intake code | +| `Xor` | C | `(a∧¬b)∨(¬a∧b)`; contract `SetExpr` has no Xor variant (`crates/lance-graph-contract/src/set_algebra.rs`) | result set identical (two-valued) | +| `Equal`, `Less`, `Greater`, `LessOrEqual`, `GreaterOrEqual`, int32 vs scalar constant | D | `Atom::I32` (`crates/lance-graph-relalg/src/ir.rs`; `lower.rs`) | `LessOrEqual`/`GreaterOrEqual` are ONNX functions (`onnx:docs/Operators.md:183,191`): match by op name, do not expand. Output is a mask, not tensor(bool) bytes | +| `Equal` uint32 vs scalar | D | `Atom::U32{eq}` (`ir.rs`) | — | +| `Less`/`Greater` on uint32; lane-vs-lane; float/fp16/bf16/double; int8/16/64; string | R | refused `NoUnsignedLaneCompare` (`crates/lance-graph-r2il/src/lib.rs`); no float lane (`crates/lance-graph-mask-risc/src/value.rs`) | float NaN is two-valued false, not UNKNOWN: relalg's NNF `Not` push-down is unsound with NaN (opusC N1; `crates/lance-graph-relalg/tests/rewrites.rs`). Float comparisons do not enter `Rel`/`SetExpr` | +| `ReduceSum` int32, all axes | C, only in the non-overflow domain | `Measure::Sum` → `Answer::Sum(i64)` (`lower.rs`) | three overflow semantics: ONNX output dtype = input dtype (`onnx:docs/Operators.md:32053-32054`); reference wraps (`onnx:onnx/reference/ops/op_reduce_sum.py:26`); onnxruntime 1.29.0 observed saturating (mechanism OPEN); relalg widens to i64. Out-of-i32 result → refusal `OverflowDomain` | +| `ReduceSum` partial axes; uint32/int64/float | R | Sum is I32-lane only (`ir.rs`) | — | +| `ReduceMin`/`ReduceMax` int32, all axes | C | `Measure::Min/Max` → `Option` (`lower.rs`) | empty reduction: ONNX yields dtype max/min (`onnx:docs/Operators.md:31444`; `onnx:onnx/reference/ops/op_reduce_min.py:38-44`); adapter `None → i32::MAX/MIN`. Float NaN propagation not representable | +| `ReduceSum(Cast(cond, INT64))` row-count pattern | C | `Measure::Count` → `POP_COUNT` (`lower.rs`) | exact 2-node pattern; output int64 | +| `Where` | K (blocked) | `Terminal::BlendI32` (`crates/lance-graph-mask-risc/src/ir.rs`); R2IL refuses `BLEND` (`crates/lance-graph-r2il/src/lib.rs`) | I32 lanes, lane-vs-lane, value-producing; outside `Rel` | +| `Gather`, `GatherElements`, `GatherND`, `ScatterElements` and other Scatter*, `NonZero`, `Unique`, `Compress`, `TopK` indices, any index-tensor input | R (ADMISSION B) | none | value-derived addressing: `onnx:docs/Operators.md:15895` (Gather) (ScatterElements) (NonZero) (Unique). ADMISSION = B: "A position derived from another relational column or table is not admissible as a read address" (`.claude/board/entries/2026-10-20-six-decisions.md` §1). `Compress` writes compacted values; `Keep` writes a mask only (`ir.rs`) | +| `Add/Sub/Mul/Div/Mod/Pow/Neg/Abs`, elementwise | P | none (R2IL arithmetic is scalar×scalar; `INT_SUB` unchecked at `crates/lance-graph-r2il/src/lib.rs`, ADD/MULT checked at) | home OPEN (OP-ONNX-1) | +| `MatMul`, `Gemm`, `Einsum` | K / X | `ndarray::simd::gemm_f64_tiled` is f64 only (ndarray `src/simd.rs`); f32 delegates to the external `matrixmultiply` crate | ONNX `MatMul` is a sum-product over numeric dtypes, not Boolean composition; no float law is admitted (§4). Boolean relation composition is `relcomp::compose`, which no ONNX op names | +| `Exp`, `Log`, `Tanh`, `Sigmoid`, `Erf`, trig | P | `simd_exp_f32` is a clamped approximation, `#[allow(dead_code)]` (ndarray `src/simd.rs`); `simd_ln_f32` is a scalar loop | numpy ULP semantics are not identical; no `tanh` found (grep only) | +| `Mish`, `Gelu`, `Softmax`, `Relu`, `LayerNormalization` (48 Function-table rows, `onnx:docs/Operators.md:169-218`) | P | bottoms out in Exp/Tanh/Log/Mul | functions may be inlined (`onnx:docs/IR.md:35`) | +| `Shape`, `Size`, `Reshape`, `Squeeze`, `Unsqueeze`, `Flatten`, `Identity`, `Constant` | OPEN | none | intake-time folding possible; unverified | +| `If`, `Loop`, `Scan`, `Sequence*`, `Optional*`, `String*`, `Random*`, `ImageDecoder`, `Quantize/Dequantize*`, `Conv*`, `*Pool`, RNN/LSTM/GRU, `ai.onnx.ml.*` | R / X | none | control flow and subgraphs are a computational-graph format (`onnx:docs/IR.md:35,181-212`) | + +**Per-op admission table (opusC B2).** Each ONNX op is classed CO-ADDRESSED (element-wise, `Not/And/Or`, `Equal` over same-table lanes) / SAME-TABLE-SEEK-UNDER-B (only with an `attest_cost` witness, which has no contract type yet: `.claude/board/ISSUES.md`) / REFUSED. Default is REFUSED. + +## 4. Intake: what must survive, and how to word compatibility + +Fields that must survive (proto2, `onnx:onnx/onnx.proto:9`). Missing or unknown identity/version → refuse, never default: +- Identity/version: `ModelProto.ir_version`; `opset_import` → `OperatorSetIdProto.domain`, `.version`; `NodeProto.op_type`, `.domain`, `.overload`. The (domain, opset) resolution rule is OPEN (not read). +- Local functions: `ModelProto.functions` → `FunctionProto.name`, `domain`, `overload`, `opset_import`, `attribute`/`attribute_proto`/, `node`, `value_info`. +- Types/shapes: `ValueInfoProto.type` → `TypeProto.Tensor.elem_type`, `shape`; `Dimension.dim_value`/`dim_param`/`denotation`. A symbolic `dim_param` must bind to the table's `n_rows`, or refuse. +- Tensors: `GraphProto.initializer`, `sparse_initializer`; `TensorProto.dims`, `data_type`, `raw_data`, `external_data`, `data_location`. +- Attributes: `AttributeProto.name`, `type`, `ref_attr_name`, values. Unknown attribute on a known op → refuse. +- Annotations round-trip, not dropped: `metadata_props` (Model, Graph, Node, ValueInfo, Tensor, Function); `doc_string` (Model, Graph, Node, ValueInfo, Attribute, Tensor, Function); `producer_name/version`/; `quantization_annotation`. +- `training_info` is refused on import (opusC N5; `onnx:docs/IR.md:110,515`). No initializer value is ever a law premise: initializers are data; laws are `AdmittedLaw` values (`crates/dr-math-binding-probe/src/relcomp.rs`). + +Typed refusal shape (proposal modelled on `RelError`, `crates/lance-graph-relalg/src/lower.rs`, and `FoldError`, `crates/lance-graph-r2il/src/lib.rs`): `Refusal { node: u32, domain, op_type, opset: i64, reason }`, `reason` ∈ {UnknownDomain, OpsetUnsupported, UnsupportedOp, UnsupportedDtype(elem_type), Broadcast, RankNotOne, DimUnbound(dim_param), UnknownAttribute(name), OverflowDomain, NoUnsignedCompare, ControlFlow, ExternalData, TrainingInfo, ValueIndexedAddress}. Whether strings may enter the contract is OPEN (`crates/lance-graph-relalg/src/ir.rs` forbids strings in the IR). Never coerce, never partial-run. Whole-graph versus per-node refusal is OPEN. + +**Wording rule (opusC N2).** Do not write "ONNX-compatible". The ONNX IR says "An implementation must support all operators in the set or reject the model" (`onnx:docs/IR.md:80`) and lists "operators that all implementations MUST support" (`onnx:docs/IR.md:67`). The claim is: "ONNX-subset reader that refuses everything else" — it imports IR ≤14, ai.onnx opset N, the listed op subset, and rejects any model whose `opset_import` names an op outside it. "Compatible" is unearned without upstream backend tests per claimed op (`onnx:docs/OnnxBackendTest.md`). + +**No float law.** No float law is admitted. Float ONNX ops lower only as written (fixed evaluation order, analogue of `run_as_written`, `crates/lance-graph-relalg/src/lower.rs`) or are refused. Reassociation is admitted for Boolean-Distinct relations only (#1707). The egglog rule set is structural (`crates/dr-math-binding-probe/src/relcomp.rs`); its soundness rests on OR/AND associativity, which IEEE-754 `+`/`*` lack. No ONNX statement fixing a float summation order was found (OPEN). + +**No ONNX-level rewrite pass (opusC C1).** No ONNX graph optimizer (constant folding, fusion, shape-inference passes) and no ONNX interpreter beside mask-risc. The only rewrites are contract set-algebra and egglog-admitted laws. + +**Palette256 (opusC N4).** ONNX ops never consume or produce Palette256 values except as opaque u8 codes passed through. Forbidden conversions: Palette256 → float to feed an ONNX op; a stored Fisher-z or cosine column produced by an ONNX graph; a generic ONNX distance op over u8 codes (`.claude/board/ISSUES.md`). Codebook attestation has no contract type yet (`.claude/board/ISSUES.md`). + +## 5. Importer dependency options — OPEN for the operator; no decision + +Facts: nothing in the repo parses ONNX. `prost = "0.13"` is optional in `crates/cognitive-shader-driver/Cargo.toml`, enabled only by feature `grpc`, under a "NEVER in production binary" comment. `protoc` 3.21.12 is installed in the container (`/usr/bin/protoc`). + +| Option | Cost | Risk | +|---|---|---| +| A. prost(-build) codegen from `onnx.proto` | new build dep, protoc at build time | proto2 handling in prost: OPEN; whether an AdaWorldAPI prost fork exists: OPEN (lance-graph CLAUDE.md fork policy) | +| B. hand-written wire reader for the ~15 fields S1 needs | zero deps, hundreds of LOC | a second partial proto decoder to maintain | +| C. existing ONNX crate (tract-onnx, candle-onnx, onnx-protobuf) | brings its own proto, often a runtime | an executor arrives with the parser (none present today) | +| D. no parser in S1: build the graph in-test from Rust values mirroring the proto subset | none | intake of real files untested in S1 | +| E. Python-side intake, scratch only | none in repo | test-only, cannot ship | + +Correction to the brief (opusA §5): onnxruntime 1.29.0 IS installed in the container's Python (not in the Rust tree). `onnx.reference` cannot run in the clone because `import onnx` needs the C++ extension (`onnx:onnx/__init__.py:82`). Either oracle is a differential test, not a proof. + +## 6. DR64³ / DR256³ + +**Original plan: NOT FOUND.** Negative-search evidence (BRIEF): no `DR64³`, `DR256³`, `64×64×64` or `64x64x64` string anywhere in the repo (`grep -rIl`, 0 files). Branch `ccr-e97e5d58-1bkumg-cartesian12` is CartesianAddress12/Quad8 shader work, not the plan. GitHub PR search "cartesian": 23 PRs, none is a DR64³ plan. The 12-stage PR sequence is not found. `.claude/knowledge/delta-card-addressing-integration-map.md` has an "18-bit hot envelope = 262,144 ... CONCURRENT mailbox working set", a working-set size and not a DR64³ identity. 262,144 = 2¹⁸ coincides arithmetically; the coincidence licenses nothing and no 18-bit DR64³ identity is defined. + +**What DR64 and DR256 are today:** DR64 `Operand { rows: &[u64; 64], validity }` (`crates/dr-math-binding-probe/src/lib.rs`), composition `relcomp::compose` (`relcomp.rs`), `Chain` guards (`relcomp.rs`). DR256 `Row = [u64; 4]` (`crates/dir-rmap-probe/src/focus.rs`), `Composer::compose` (`compose.rs`), guard by `prep::Witness` (`prep.rs`), no `MethodSignature`/`Axis` typing. + +**NEW PROPOSAL (from opusB §2), not recovered history.** "DR64³" is the logical index cube X×Y×Z (64 each) over which a contraction of typed DR64 views ranges. It is never a stored object. +- (R1) Chain contraction `R: X→Y`, `S: Y→Z`, `(R∘S)[i,k] = ∃j R[i,j] ∧ S[j,k]`. This is `relcomp::compose` today (`relcomp.rs`); nothing is new except the name. +- (R2) Triangle `(R∘S) ∧ Q` with `Q: X→Z`. Needs one new check not in `Chain` (adjacency only, `relcomp.rs`): `Q.row == R.row` and `Q.column == S.column`. Whether it belongs in `Chain` or a separate admission type: OPEN. +- Guards applying unchanged: same frame issue and still current (`lib.rs`, `relcomp.rs`), same focus, same scope, domain adjacency, TwoValued + Distinct only (`lib.rs`), only `BooleanCompose` admitted. +- Not allowed: a new identity encoding (no packed `(i,j,k)` id); any CausalEdge64 change (S/P/O bytes are palette indices, `crates/causal-edge/src/edge.rs`); a new executor; a gather-shaped hop (`crates/lance-graph-mask-risc/src/graph_hop.rs`); Bag through the DR64 binder (`lib.rs`); any claim that 64³ is implemented. +- Sizes, arithmetic only, computed not measured: 64³ bits = 262,144 bits = 32 KiB; 256³ bits = 16,777,216 bits = 2 MiB. The cube must not be materialized; no measurement shows it cheaper (OPEN). No throughput figure is given for either. + +**OPEN tension (bit-position scan).** `relcomp::compose` scans set bits for positions (`trailing_zeros`, `crates/dr-math-binding-probe/src/relcomp.rs`) and DR256 `compose` does the same (`crates/dir-rmap-probe/src/compose.rs`), while `crates/dir-rmap-probe/src/qr.rs` states "no loop scans set bits for a position (the D-RU-6 address rule)". Whether position-scanning inside one co-addressed frame is the forbidden gather (ADMISSION B, `.claude/board/ISSUES.md`) is not ruled anywhere found. + +**DR256³ preconditions (opusB §5), none met:** DR64³ R1/R2 pass the S3 arms with the R2IL arm measured; a DR256 binder with DR64 typing (`prep.rs`); a certificate route at 256 (no egglog dep in `dir-rmap-probe`); materialization stays refused (precedent `crates/cognitive-shader-driver/src/immaterial_needle.rs`); `TooLarge` (`qr.rs`) refuses on every axis; CausalEdge64 S/P/O bytes are not DR256³ coordinates; cross-width transfer (256 → 64) has no code, only DR64→DR64 reuse exists (#1740). + +## 7. Stages + +"Proof engine" values: egglog-certified (only `LawShape::BooleanCompose`), differential test (oracle named), none. "Certified" may appear only in the first case (opusC B4). The operator rule names egglog, eggcc, datafrog, ascent and MeTTa over MORK over a PathMap oracle as the engines a proof may come from. Today only egglog produces a proof object in this repo. eggcc has no code. datafrog and Ascent are dev-dependency oracles here and emit no provenance; their tuple-comparison oracle role was withdrawn on 2026-10-21 (`.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md`). A stage that wants them as its proof engine must first show what proof object they produce (OPEN, OP-ONNX-14). + +| Stage | Deliverable | Gate | Proof engine | Prerequisite | Status | +|---|---|---|---|---|---| +| S0 | this plan + board entry | review | none | none | this PR | +| S1 | ONNX intake probe, subset reader with typed `Refusal`; Boolean/compare/reduce fragment lowered onto relalg | S1 falsifier below | differential test (onnxruntime 1.29.0; numpy reference semantics) | importer decision (OP-ONNX-2) | PLANNED, not authorized | +| S2 | admission table and value-maths decision recorded | operator ruling | none | OP-ONNX-1 | PLANNED, not authorized | +| S3 | DR64³ R1/R2 contraction probe, three arms | S3 falsifier below | egglog-certified for reassociation only; all else differential test | S2; OP-ONNX-4, OP-ONNX-5 | PLANNED, not authorized | +| S4 | learned-transition boundary: ONNX `training_info` refused; plasticity typed as method, never premise; Palette256 forbidden conversions enforced | refusal tests with disable runs | none (refusals are tests) | S1 | PLANNED, not authorized | +| S5 | export/codegen evaluation | review | none | S1..S4 | PLANNED, not authorized | + +The 64³ Explore → 256³ Validate → Certified Method → 64³ Reuse progression: the "256³ Validate" step is a differential test and must be named so (opusC B4). It has no proof engine today. + +**S1 falsifier (opusA §5).** Fixture: one table, `n_rows ∈ {0, 1, 63, 64, 65, 1000}`, lane `x: int32` (incl. i32::MIN/MAX), lane `k: uint32`, one bool plane `b`, symbolic dim `N`. +- Positive: G1 `Less(x,c)`; G2 `And(Less(x,c), Not(b))`; G3 `ReduceSum(Cast(G2, INT64))`; G4 `ReduceMin(x)`, `ReduceMax(x)` (N=0 → i32::MAX/MIN via adapter); G5 `Equal(k,v)`. relalg output equals onnxruntime output; mask words equal packed bools. +- Negative (named `Refusal`, never an answer): `Tanh(x)`; `Less` on float; `Less` on uint32; `Less(x,x)` lane-vs-lane; broadcast `[N]` vs `[N,1]`; unknown domain; `ReduceSum` whose i64 result leaves i32. +- Silent twin: every positive graph yields zero refusals; in-range `ReduceSum` does not raise `OverflowDomain`; `metadata_props`/`doc_string` still lower and round-trip unchanged. +- Disable runs (commit first, assert the patch applied): `Less→Le`; drop the dtype check; map empty Min `None→0`; delete the overflow guard; skip `Not`. Each must turn a named test red. + +**S3 falsifier (opusB §4).** Fixture: three bound DR64 views on one `FrameStore` seal, one focus, one scope, axes X→Y→Z(→W); seeded fill as `crates/dr-math-binding-probe/tests/relcomp.rs`. Arms, bit-exact over all 64 rows: (1) `Chain::eval` over every order (`relcomp.rs`); (2) a co-addressed R2IL program (`exists(intersect(R_row_i, S_col_k))`, needs `S` transposed first, a preparation cost reported separately per D-RU-6, `.claude/plans/d-relalg-unified-v1.md`), which does not exist; (3) an independent scalar pair-enumeration oracle (`tests/relcomp.rs`), a differential test; (4) reassociation equality via the egglog certificate only (`relcomp.rs`). Costs reported separately (bind; transpose; steady contraction; result materialization; cold egglog) in ns/µs only. Refusals needing can-fire and can-stay-silent cases: `DifferentFrame` (`relcomp.rs`), `StaleFrame`, `DomainMismatch`, `BagNeedsMultiplicity` (`lib.rs`), focus/scope moved (`relcomp.rs`), `NotThisChain`, and the R2 closing-view axis mismatch (does not exist; must be added and disable-verified). + +## 8. What ONNX reuse eliminates, and what it does not + +- ONNX replaces at most an interchange AST. It does not remove the proof-side term language: egglog needs its own datatype (`crates/dr-math-binding-probe/src/relcomp.rs`) and ONNX has no rewrite or proof semantics (opusC N7). +- The #1741 Julia-map conclusions P-J1..P-J4 stay open: typed egglog rules via the Rust API, keep `ProofStore`, a standalone replay checker (entry `.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md`). X4 (rules as typed values) and X12 (keep the proof DAG) are proof-side work ONNX does not touch. Anchor A2 ("internal proof representation chosen by measurement") is not pre-decided as "ONNX + relalg" and remains open (same entry). +- Certificate reuse is shown only for `source` changes with the same focus, scope and ABI (`crates/dr-math-binding-probe/tests/x8_fresh_frame.rs`); refusals at. + +## 9. Open-points register + +| ID | Question | Owner | Dependency | Evidence | Falsifier | Decision | Status | +|---|---|---|---|---|---|---|---| +| OP-ONNX-1 | Home for value maths (arithmetic, MatMul, Exp/Tanh/Mish): relalg cannot take it without a new IR | operator | none | opusA §2; D-RA-2 `.claude/plans/d-relalg-unified-v1.md`; `crates/lance-graph-relalg/src/lib.rs` | any proposal adding value-producing nodes to `Rel` | none | OPEN | +| OP-ONNX-2 | Importer dependency (options A-E) | operator | OP-ONNX-1 for scope | §5 above | S1 reads real ONNX bytes | none | OPEN | +| OP-ONNX-3 | DR64³/DR256³ original plan missing | operator | none | §6 negative search (BRIEF) | the plan is located | none | OPEN | +| OP-ONNX-4 | Does bit-position scanning in one co-addressed frame violate ADMISSION B / D-RU-6? | operator | none | `relcomp.rs`; `compose.rs`; `qr.rs`; `.claude/board/ISSUES.md` | a ruling | none | OPEN | +| OP-ONNX-5 | Independent proof checker; none exists | plan owner | #1741 P-J4 | `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md` | a replay checker that rejects a tampered proof | none | OPEN | +| OP-ONNX-6 | Cross-focus/scope/ABI rebinding of certificates beyond #1740 | plan owner | S3 | `tests/x8_fresh_frame.rs`; opusC N3 | reuse across stores with different focus/scope/geometry | none | OPEN | +| OP-ONNX-7 | Prover revision not recorded in the certificate (egglog `branch = "main"`). Floating deps are per repo pin policy, so this is a certificate-identity gap, not a dependency defect | plan owner | none | `crates/dr-math-binding-probe/Cargo.toml`; opusC N3 | certificate carries the egglog revision | none | OPEN | +| OP-ONNX-8 | Why onnxruntime 1.29.0 saturates int32 `ReduceSum` (observed in 2 cases) | S1 | S1 | opusA §5 | a third case or the kernel source | none | OPEN | +| OP-ONNX-9 | `.claude/plans/dr-mathematical-compiler-v1.md` calls egglog's self-check "independent" (wording defect) | owner of that plan | none | `relcomp.rs` ("egglog checks every proof it returns") | the wording is corrected | none | OPEN | +| OP-ONNX-10 | `.claude/plans/dr-mathematical-compiler-v1.md` "RelAlg/typed AST expresses admissible mathematics" versus D-RA-2; whether it predates 2026-10-20 | owner of that plan | OP-ONNX-1 | opusC B1 | the plan line is reconciled | none | OPEN | +| OP-ONNX-11 | R2 closing-view typing check: in `Chain` or a separate admission type | S3 | S3 | opusB §2 | disable-verified refusal | none | OPEN | +| OP-ONNX-12 | `observe_focus` omits a scope refusal; intended? | plan owner | none | `crates/dr-math-binding-probe/src/population.rs` | a ruling | none | OPEN | +| OP-ONNX-14 | Which proof object datafrog, Ascent or MeTTa/MORK/PathMap would produce, so they can serve as a stage's proof engine | operator | none | `.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md` | an exported, replayable derivation | none | OPEN | +| OP-ONNX-13 | Whole-graph versus per-node refusal; strings in the contract | operator | S1 | §4; `ir.rs` | a ruling | none | OPEN | + +## 10. Housekeeping + +SAFE NOW (done in this PR, commits `7fa35361` and `83945785`): D-TGA-5D status; `IDEAS.md` amendments X8 and the certified-compiler row; PR_ARC catch-up #1726–#1741; LATEST_STATE after #1741; D-TGA-5 file attribution. + +SEPARATE PR: none identified. + +BLOCKED: D-DRMC rows missing from STATUS_BOARD (owner CC2, ask on EXO-50); the `dr-mathematical-compiler-v1.md` wording fix (plan owner; OP-ONNX-9). + +## 11. Next gate + +The smallest independently reviewable step is the S1 intake probe, pending the importer decision (OP-ONNX-2) and the value-maths scope ruling (OP-ONNX-1). Nothing past S0 is authorized.