xlog-relcomp-probe: XLOG recursion on DR64, and XLOG × egglog over one relation

.claude/board/entries/2026-10-31-coresearch-d-staunen-arc.md

@@ -0,0 +1,65 @@
+# Co-research: the D-STAUNEN arc (#1885–#1889) against code and outside sources — 2026-10-31
+
+**Status: exploration map. Ratifies nothing.** The operator chooses which probes run.
+
+## Question
+The arc is five docs-only maps (D-STAUNEN-0..4): plasticity as a DT64 capability over Atlas SNN events, HDC signatures, novelty-gated eligibility, XLOG/NSL hypotheses in sparse THOUGHT deltas, and 64-thought metaplasticity with root-disjoint evidence. Which of its gates have their own falsifier run, and what outside knowledge changes which gate to run first?
+
+Premise gate (premise-auditor): PREMISE-SPLIT. A PR that overlaps a gate is candidate evidence, not admission. X6 splits into X6a (lineage and independent support) and X6b (attribution). HDC and SNN map only onto candidate discovery and novelty modulation, never onto evidence.
+
+## Gate ledger (code cartographer; file:line in the scratch crosswalk)
+- **Falsified by its own gate:** X3 only (lance-graph-nsl oracles, #1846).
+- **Partial:** X0, X1, X2 (#1884 bag counts; no forced-overflow test on the checked multiply), X4 (no gradient check), X6 (test-level, #1896), X7, X8.
+- **Candidate evidence:** C1, M2.
+- **Absent:** C0, C2, C6, X5, M0, M1, M3–M8, A0–A7. For A0–A7 the closed search space was `crates/**/*.rs,*.toml` for brian2, stdp, atlasir, three-factor and eligibility traces.
+
+## Fixed during the run
+#1896's `derivation_multiplicity_is_not_independent_evidence` counted **lineage** (every root any derivation touches) and called it independent evidence. With A reporting 1→2→4→5 and B only 1→3→4, the derivations rest on {A} and {A,B}. Absorption leaves {A}: one independent support, where the test asserted two.
+
+The test now computes the minimal-environment label (ATMS / PosBool, arXiv 2202.10766 §2–3) for three cases, and keeps lineage as a separate count. Four disables are red, each at a distinct assertion. Commits `9007724`, `da0feb5`, `c295d25`; the last scopes the label as a cold test-only oracle.
+
+## Verdicts
+| # | idea | verdict | why / probe |
+|---|---|---|---|
+| 1 | Independent support = root-disjoint minimal environments (X6a) | **PROBE** P-X6A-LEDGER | Already in production as `DerivationLedger` (`lance-graph-planner/src/nars/support.rs:308-323`, D-EPI-COT C1/C2). Probe: a plain-text fixture exported by xlog-relcomp-probe, replayed by a planner dev test into the ledger. `pooled` must agree with the probe's label on {A}/{A,B} and on disjoint {A},{B}. On the triangle {A,B},{B,C},{A,C} they **diverge by design**: the label has 3 environments, `pooled` selects 1. The test pins that divergence. The probe crate does not depend on the planner: the probe is a separate workspace because of arrow 60 vs 58, and the planner takes a path ndarray. |
+| 1b | Label stable under cycle unrolling | **PROBE** P-X6A-CYCLE (run first) | `derivations()` lists simple paths only, so recursion is unexercised. Fixture: 1→2, 2→3, 3→2, 3→4; A = {1→2, 2→3, 3→4}, B = {3→2}. The label must equal {{A}} for k = 0..3 unrollings. Twin: a bypass 1→5→4 reported by C must give {{A},{C}}, disjoint. Disable: drop minimality. |
+| 2 | N[X] is infinite under recursion | **PROBE** P-REC-NO-COUNT | Pin that no API returns a multiplicity for a recursive fact. Twin: the acyclic count is admitted. |
+| 3 | One witness is not lineage | **PROBE** P-TRACE-NOT-DISJOINT | On the diamond, `trace` roots == 1 and the `support` label == 2. Twin: a chain. |
+| 4 | Truncated proof sets prove overlap only | **PARK** | One-way rule; matters only once a k-truncated proof set exists. The ledger horizon is k = 1. |
+| 5 | Retraction under recursion (DRed^c) | **PARK** | Stale frame refused plus recompute is enough until incremental retraction is asked for; a counter store would be a new store. |
+| 6 | PROV attribution (X6b) | **ADOPT-NOW (vocabulary)** | Root, version and program hash stay on the test record and fixture header, not a new type. `reading` is an attribute of the result, not provenance. CE64 W never carries it (#1847 :405). |
+| 7 | Root = agent or report? | **OPEN, operator** | `root()` hashes observer and facts, so one observer filing two reports counts twice. P-AGENT-VS-REPORT pins both readings once ruled. |
+| 8 | Three senses of "provenance" | ADOPT-NOW (vocabulary only) | Attribution (PROV) / lineage-support (semiring) / encoding generation (`EdgeProvenance`). Rename nothing. |
+| 9 | Cross-THOUGHT root-disjointness | SKIP (duplicate) | Already D-HL-3 (Queued, falsifier pre-registered; capstone :150). |
+| 10 | Replay must not reinforce | SKIP (duplicate) | 2026-10-22 E2/E3/P-M1 and #1847 E1–E7 already cover it. |
+| 11 | Novelty gating | PARK | Must inherit D-CE64-STAUNEN-0's kill condition: raw surprise lost to round-robin. |
+| 12 | Eligibility traces / delayed credit | PARK | H3 inconclusive under Holm. Traces would make W carry evidence. |
+| 13 | HDC/SNN for discovery only | ADOPT-NOW (ruling) | I-VSA-IDENTITIES; ScentLearner #1844 is the surface. Nengo is non-commercial: never a dependency. |
+| 14 | Mask-union why-provenance holds only for monotone queries | **PROBE** (cheap) | X-gates over NOT/minus refuse; a test pins the refusal. |
+| 15 | Stored N[X]/Why(X) carrier | SKIP (anchor) | 2026-10-21 PARK/SKIP; #1888 forbids a provenance store. |
+| 16 | Signed diffs as multiplicity | PARK (lens) | A DD/DDlog engine would be a new engine. The concrete X2 gap is a forced-overflow test on `native.rs:45`: PROBE, cheap. |
+| 17 | Kythe ref/call | PROBE (P-KYTHE-CALL) | #1894 emits `ref` only. The probe must start red; call facts need a source (Charon not installed). |
+| 18 | egglog proofs | SKIP (resolved) | The PLDI'23 paper calls proofs future work; the fork has `new_with_proofs` and #1896 uses it. |
+| 19 | Atlas Definition/Instance/Run identity | PROBE (document check, needs network) | The fetched Atlas README does not mention it. A0–A2 stay parked until it is found at file:line. Brian2 CeCILL-2.1: external oracle only. |
+| 20 | NSL neighbour packing | SKIP (anchor) | Copies neighbour features per example (zero copy). Oracle use (#1846) stays. |
+
+## Recommended order
+1. P-X6A-CYCLE
+2. P-REC-NO-COUNT and P-TRACE-NOT-DISJOINT (all offline, test-only)
+3. P-X6A-LEDGER, which decides whether X6a is already met by the ledger
+4. The X2 overflow test
+
+A-gates wait for P-ATLAS-IDENTITY. M-gates cite D-HL-3 and the 2026-10-22 probes rather than re-plan them.
+
+## Not searched
+- Atlas source tree: only the README was fetched.
+- Green et al. 2007, de Kleer 1986, Nieuwenhuis–Oliveras and the Soufflé TOPLAS paper are cited secondhand.
+- Miconi 2018's arXiv id is unverified.
+- Scallop's licence file was not read.
+- The arc's ACT-R, PointCare, qualia and Brain-SoC context was not researched, by design.
+- `holograph`, `cognitive-shader-driver/src/serve.rs` and `learning/src/cam_ops.rs` matched eligibility/STDP terms and were not read.
+
+PR #1896 | STATUS: open | OUTCOME: co-research map for the D-STAUNEN arc; lineage-as-evidence defect fixed | OPEN: root = agent or report; which probes to run
+
+MIRROR
+- BLIND SPOT: #1896's provenance test was reviewed for multiplicity versus roots, but never against a case where a second observer depends on the first.

.claude/board/entries/2026-10-31-d-reasoning-codegraph-0-xlog-egglog-shared-relation.md

@@ -0,0 +1,19 @@
+# D-REASONING-CODEGRAPH-0 stage 1: XLOG × egglog over one DR64 relation
+
+**Date 2026-10-31 · Status MEASURED (lab probe) · Crate `crates/xlog-relcomp-probe` (`src/recursive.rs`, `tests/recursive.rs`, `tests/shared_relation.rs`)**
+
+**XLOG recursion on the CPU kernel.** XLOG's compiled transitive-closure SCC is admitted (`admit_closure`) and evaluated semi-naively on the DR64 register with the existing `relcomp::compose`. #1888 noted this was not covered by #1884. It matches BFS and a fixpoint walk of XLOG's own plan, and a 200-case differential. Work is exactly one row OR per derived pair. Non-linear and mutual recursion are refused.
+
+**Shared relation.** One `edge` register under one sealed frame is read by XLOG's closure (directed reachability) and by egglog (equality with `ProofStore` proofs).
+- egglog's equality equals the closure of `E ∪ Eᵀ`.
+- egglog proof facts are bits of the same register, and lie inside XLOG's `support` mask for a directed answer.
+- A removed fact invalidates the XLOG bind (stale frame) and is located in the old egglog proof by address, without re-running egglog.
+
+**Traceroute.** Backward is `support(x, y)` and forward is `affected(u, v)`, both computed from the closure on demand; derivations are not stored. The one conversion is register bits to egglog fact text (114 B for 6 edges).
+
+OPEN:
+- timing;
+- MLIR/DialEgg leg;
+- SQL and Java legs;
+- egglog proofs of a directed relation;
+- XLOG recursion shapes beyond one linear closure.

.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.
 
-526 entries, 2026-08-06 .. 2026-10-31.
+528 entries, 2026-08-06 .. 2026-10-31.
 
 | date | entry id | finding | file |
 |---|---|---|---|
@@ -35,10 +35,12 @@ exactly one of them, never both.
 | 2026-10-31 | `D-SAG-6-2-JOIN-IDENT` |  | [2026-10-31-d-sag-6-2-span-join-identity.md](2026-10-31-d-sag-6-2-span-join-identity.md) |
 | 2026-10-31 | `D-SAG-6-2-LAB` |  | [2026-10-31-d-sag-6-2-lab-projection.md](2026-10-31-d-sag-6-2-lab-projection.md) |
 | 2026-10-31 | `D-SAG-6-1-CHECKLIST` |  | [2026-10-31-d-sag-6-1-checklist.md](2026-10-31-d-sag-6-1-checklist.md) |
+| 2026-10-31 | `D-REASONING-CODEGRAPH-0` |  | [2026-10-31-d-reasoning-codegraph-0-xlog-egglog-shared-relation.md](2026-10-31-d-reasoning-codegraph-0-xlog-egglog-shared-relation.md) |
 | 2026-10-31 | `D-MIST-NATIVE-1b` |  | [2026-10-31-d-mist-native-1b-makor-hydrate.md](2026-10-31-d-mist-native-1b-makor-hydrate.md) |
 | 2026-10-31 | `D-DT64-6-DR` |  | [2026-10-31-d-dt64-6-dr-addressing-module.md](2026-10-31-d-dt64-6-dr-addressing-module.md) |
 | 2026-10-31 | `D-DYNBAG-X` |  | [2026-10-31-cross-frontend-projection-crosswalk.md](2026-10-31-cross-frontend-projection-crosswalk.md) |
 | 2026-10-31 | `coresearch-mandatory-codegraph` |  | [2026-10-31-coresearch-mandatory-codegraph.md](2026-10-31-coresearch-mandatory-codegraph.md) |
+| 2026-10-31 | `D-STAUNEN` |  | [2026-10-31-coresearch-d-staunen-arc.md](2026-10-31-coresearch-d-staunen-arc.md) |
 | 2026-10-30 | `D-XLOG-NATIVE-0` |  | [2026-10-30-d-xlog-native-crosswalk.md](2026-10-30-d-xlog-native-crosswalk.md) |
 | 2026-10-30 | `D-XLOG-DR64-0` | XLOG's CPU frontend lowers onto DR64 relcomp (answer {2}, 2 oracles); its optimizer emits ChainJoin and swapped orders; arrow 60 vs 58 blocks in-tree use; masks lose to scalar on selective data | [2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md](2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md) |
 | 2026-10-30 | `D-TRACT-SHAPE-1` |  | [2026-10-30-d-tract-shape-1-cold-shape-folding.md](2026-10-30-d-tract-shape-1-cold-shape-folding.md) |

crates/xlog-relcomp-probe/Cargo.toml

@@ -34,6 +34,10 @@ xlog-logic = { git = "https://github.com/BrainyBlaze/xlog", rev = "bff6da6633081
 lance-graph-contract = { path = "../lance-graph-contract" }
 # CausalEdge64, for the Epi5 reading of XLOG results (tests/epi5_reading.rs).
 causal-edge = { path = "../causal-edge" }
+# egglog, on the coordinate dr-math-binding-probe already uses, for the
+# shared-relation experiment (tests/shared_relation.rs): equality with proofs
+# over the same DR64 register the closure reads.
+egglog = { git = "https://github.com/AdaWorldAPI/egglog", branch = "main" }
 
 [patch."https://github.com/AdaWorldAPI/lance-graph"]
 lance-graph-contract = { path = "../lance-graph-contract" }

crates/xlog-relcomp-probe/README.md

@@ -342,3 +342,98 @@ The Y axis is DR's `lance_graph_dt64::dr::LocalMap` (64 or 256 wide). `admit_cou
 - adding instead of multiplying: 2 failed;
 - ignoring a bound: 5 + 1 failed;
 - admitting any aggregate: 1 failed.
+
+## Recursion and a second engine on the same relation (`src/recursive.rs`)
+
+**Recursion.** XLOG compiles `path(X, Y) :- edge(X, Y). path(X, Y) :- path(X, Z), edge(Z, Y).`
+into one recursive SCC: a base `Scan edge`, and a `ChainJoin` of `Scan path` with `Scan edge` on
+`path.1 = edge.0`, projecting columns 0 and 3, with an agreeing `fallback`. `admit_closure`
+accepts exactly that shape. It refuses non-linear recursion (`path ∘ path`) and mutual recursion,
+each with its own reason. `closure` binds `edge` under the sealed frame, types `edge ∘ edge` with
+the existing chain typing, and runs semi-naive rounds over the existing `relcomp::compose`. No new
+kernel is added.
+
+`tests/recursive.rs` (9 tests):
+- the result equals BFS over the tuples and a naive fixpoint walk of XLOG's own compiled bodies;
+- a 200-case deterministic differential against BFS passes;
+- cycles terminate;
+- semi-naive work is exactly one row OR per derived pair;
+- a stale frame is refused.
+
+**Derivations on demand.** `support(x, y)` returns the `edge` facts some derivation of
+`path(x, y)` can use: both branches of a diamond, nothing off-route. `affected(u, v)` returns the
+answers a fact can feed. Both are masks read from the closure; nothing about a derivation is stored.
+
+**A second engine.** `tests/shared_relation.rs` puts egglog on the same register. Equality comes
+from `(rule ((edge a b)) ((union a b)))`, and proofs from `prove`.
+- egglog's `a = b` equals the closure of `E ∪ Eᵀ` on every pair of a two-component graph.
+- Every directed `path` is an egglog equality; the converse fails.
+- Every `edge` fact an egglog proof rests on is a bit of the shared register. On the diamond, every
+  such fact also lies in XLOG's `support` mask for the same answer.
+- When a fact is removed and the frame advances, the XLOG bind refuses, and the removed fact is
+  found in the old egglog proof by its address, without re-running egglog.
+
+The one conversion is register bits to egglog fact text. For 6 edges that is 114 bytes, against a
+512-byte register. egglog keeps its own tables and union-find; they are not replaced by masks.
+
+Disable runs: dropping the support filter, the reflexive star in `affected`, the non-linear guard,
+the mutual-recursion guard, or semi-naive deltas each turns its test red.
+
+Not done:
+- timing, for either engine;
+- XLOG recursion beyond one linear closure;
+- egglog proofs of a directed relation (egglog's equality is symmetric by construction).
+
+## Traceroute and provenance (`src/recursive.rs`, `tests/trace.rs`, `tests/provenance.rs`)
+
+**Traceroute.** `trace(edge, valid, x, y)` replays the semi-naive rounds `closure` runs, keeps each
+round's delta, and walks back from the round in which `path(x, y)` first appeared, choosing the
+smallest `z` with `(x, z)` in the previous delta and `edge(z, y)`. It returns the chain of `edge`
+facts, or `None` when the pair does not hold. `closure` is unchanged. `tests/trace.rs` (6 tests)
+checks on the diamond, the cycle and a 200-case random differential that every chain starts at `x`,
+ends at `y`, links up, uses only bits of `edge` inside `support(x, y)`, and has the BFS
+shortest-path length.
+
+**Provenance.** `tests/provenance.rs` (6 tests) carries X6 provenance at test level:
+`Provenance { root, version, program_hash, reading }`.
+- `root` identifies the original source: an observer and the set of facts it reported, sorted and
+  deduplicated, so a reordered or repeated copy of one report is the same root.
+- `version` is the frame's `FrameRevisions`.
+- `program_hash` is FNV-1a over the consumer's program text (XLOG rules, or egglog rules), never over
+  the facts.
+- `reading` is the CE64 declared reading, read through `Epi5Declarations`: `Direct × Open` for a
+  trace of length 1, `IndirectKnown × Open` otherwise. An egglog equality has no declared reading
+  (`None`).
+
+Evidence and derivations are counted separately:
+- Independent support is the set of minimal environments of source roots that entail the answer:
+  the ATMS label, PosBool provenance. Lineage (every root any derivation touches) is a separate,
+  weaker count.
+- On the diamond, `path(1, 5)` has 2 derivations. With one observer they rest on one environment
+  `{A}`. If B reports `1->3->4` but only A reports `4->5`, the derivations rest on `{A}` and
+  `{A, B}`; absorption leaves `{A}`, so B adds no independent support, although lineage touches 2
+  roots. If B also reports `4->5`, `{A}` and `{B}` are disjoint: 2 independent supports. Lineage is
+  2 in both cases.
+- XLOG's trace and an egglog proof over one register are two consumers with two program hashes and
+  one root: 1 independent observation.
+
+Not shown: that a root hash is a durable source identity outside these tests.
+
+Disable runs for the traceroute and provenance (committed first, one patch at a time, each anchor asserted, file restored with `git checkout`):
+
+| Disabled | Red |
+|---|---|
+| `trace` picks the largest intermediate | `diamond_trace_takes_the_smallest_intermediate` |
+| `trace` drops the `edge(z, y)` check | `deterministic_differential` |
+| root depends on serialization order (no sort/dedup) | `reordering_a_report_is_not_a_new_observation` |
+| program hash covers the facts | `provenance_changes_when_and_only_when_its_inputs_change` |
+| root ignores the observer | `reordering_a_report_is_not_a_new_observation` |
+| a base fact reads as composed | `readings_follow_the_trace_of_the_real_closure`, `provenance_changes_…` |
+
+Disable runs for the minimal-environment label (2026-10-31, after the co-research on the D-STAUNEN
+arc found that the first version counted lineage and called it independent support): dropping
+absorption, keeping only the first reporter of a fact, `disjoint` always true and `disjoint` always
+false each turn `derivation_multiplicity_is_not_independent_evidence` red, at four different
+assertions.
+
+One mutant stays green and is equivalent, not a missing test: searching for the last round that holds `(x, y)` instead of the first. Each round's delta excludes everything already derived, so a pair appears in exactly one round.

crates/xlog-relcomp-probe/src/lib.rs

@@ -39,6 +39,7 @@
 use std::collections::BTreeMap;
 
 pub mod native;
+pub mod recursive;
 
 use dr_math_binding_probe::relcomp::{ComposeRefusal, Rows, Work, compose};
 use dr_math_binding_probe::{