From 3f1658dabf6af686ffc010f9d42c6250ab7dda60 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 09:40:31 +0000 Subject: [PATCH 1/3] =?UTF-8?q?board:=20/coresearch=20exploration=20map=20?= =?UTF-8?q?=E2=80=94=20thought-git=20accumulation=20as=20a=20large=20Marko?= =?UTF-8?q?v=20chain?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Premise gate split the question: thought-git ops are deterministic, no P exists, squash is path composition (a lag), promotion is evidence. Stochastic layer exists only where aggregation induces it (exo129 snap kernel). Map: 20 ideas with ADOPT-NOW/PROBE/PARK/SKIP, seven pre-registered probes (PR-1..7) incl. a head-selection probe, and a requested storno of the #1736 IDEAS "certificate is P-hat" / "4-eps tolerance" bullets. Sources: Bittracher & Schuette 2021, Askarian-Xu-Farago 2016 (both CC BY, read in full). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- ...026-10-23-coresearch-thought-git-markov.md | 164 ++++++++++++++++++ .claude/board/entries/README.md | 3 +- 2 files changed, 166 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-23-coresearch-thought-git-markov.md diff --git a/.claude/board/entries/2026-10-23-coresearch-thought-git-markov.md b/.claude/board/entries/2026-10-23-coresearch-thought-git-markov.md new file mode 100644 index 000000000..48d3e6cc8 --- /dev/null +++ b/.claude/board/entries/2026-10-23-coresearch-thought-git-markov.md @@ -0,0 +1,164 @@ +# 2026-10-23 — /coresearch: thought-git accumulation as a large Markov chain + +**Status:** EXPLORATION MAP. Nothing in it is adopted; the operator chooses which ideas go forward. + +**Input:** the operator, citing two papers: +- **B&S:** Bittracher & Schütte, *A probabilistic algorithm for aggregating vastly undersampled large Markov chains*, Physica D 416 (2021) 132799, CC BY. Read in full. +- **AXF:** Askarian, Xu & Faragó, *Utilizing Network Structure to Accelerate Markov Chain Monte Carlo Algorithms*, Algorithms 9(3):50 (2016), doi 10.3390/a9030050, CC BY. Supplied mid-run and read in full. The PDF came from the mdpi-res.com CDN because www.mdpi.com returns 403 here; sha256 `e219f6ea…12b0`. + +**Follow-up question folded in:** besides CE64 59..63 certification, witness support and resolved contradiction, which heuristic decides that a thought becomes the head and its children are squashed? And what is MCMC? + +## Question, after the premise gate + +The premise auditor returned **PREMISE-SPLIT**. The thought-git ops are deterministic: +- `receipt.rs` `run` is pure, and the jitter is a hash of the recorded seed. +- The version state is a growing cell map (`oracle.rs` `next_version`). +- The lanes are coupled through one 63-slot pool (`slots.rs`). +- No transition matrix P exists over any named state. + +A squash composes write-sets along a path, which is a coarser lag, not a quotient of states. Promotion on 59..63 is a question of evidence, not of correlation. The question was therefore re-asked as four: + +- **Q1:** is there a stochastic process at all, and over what finite state? +- **Q2:** squash safety = commutation with sequential landing. +- **Q3:** promotion; aggregation can at most be a necessary pre-check. +- **Q4:** not storing 64×10⁶ deltas = equivalence classes of receipts. + +## Answer + +The Markov machinery does not apply to the thought-git cells. + +- Ops are functions, not draws. A 0/1 kernel has ergodic coefficient ρ = 1, so the AXF and B&S bounds are vacuous on it. +- The stochastic layer that does exist is **induced by aggregation**. Deterministic ops observed through a lossy palette `snap` give a kernel K(t|s,b). Its row entropy is positive exactly where purity is below 1. This is the exo129 chain (#1731), and it is where lumpability (EXO-132) lives. +- A second stochastic layer could come from seeds or driver choices. It exists only if someone defines it, with a named sampling law. + +What survives for thought-git is algebraic: +- Commutation sweeps (Q2). +- Exact congruence by partition refinement instead of sampled purity (Q1-ii / EXO-132). +- Receipt classes keyed without `thought`, guarded by root identity (Q4). +- A head rule built from refinement, subsumption and root blocking (follow-up). + +Promotion on 59..63 stays where it is: `pearl::revise` on a new independent root (Q3). + +**No tolerance ε ever goes on the D-TGA-5 gate.** A tolerance would admit stacks the exact refusal rejects. + +**MCMC, for the record.** You build a chain whose stationary law is a specified target π, run it until it has mixed, and read π(A) off sample frequencies. +- AXF adds that for one quantity π(A) only the partition {A, Ā} has to be ε-lumpable. The error is then ≲ ε/(p₀+q₀), independent of N. +- The bound survives a time-varying chain whose aggregated step matrices stay inside an interval [L, U] (Hartfiel's Markov set-chains). +- Thought-git has no specified target distribution. Monte Carlo over seeds is sampling, not MCMC. + +## Crosswalk and verdicts + +R = the relation of the outside idea to the existing surface. FW = the firewall critic's verdict. + +| id | idea | R | FW | map | +|---|---|---|---|---| +| X1 | "64×10⁶ ops = one chain over cell states; the certificate is P̂" (#1736 IDEAS block) | CONFLICTS-ANCHOR | CATEGORY-ERROR ×3 | **SKIP**, and correct the block (below) | +| X2 | squash = composition along a path (lag), not lumping | ALREADY-HAVE | FITS | ADOPT-NOW as vocabulary | +| X3 | commutation sweep over random interleavings | PARTIAL | FITS (rename) | **PROBE PR-2** | +| X4 | coarsest congruence by partition refinement (Paige–Tarjan / Valmari–Franceschinis O(m log n)) as the exact form of purity | PARTIAL | FITS (cold, blocks as masks) | **PROBE PR-3** | +| X5 | question-specific ε-lumpability {A, Ā} with the AXF bound | NEW | FITS (pre-register A) | **PROBE PR-4**, exo129 layer only | +| X6 | [L,U] interval matrices for inhomogeneous chains (Hartfiel) | NEW | CATEGORY-ERROR on thought-git | PROBE as the PR-4 inhomogeneous arm on exo129; never on receipts | +| X7 | Hartfiel product bound as a squash tolerance | NEW-cond. | VIOLATES D-TGA-5 | **SKIP** | +| X8 | ergodic coefficient / start-independence of a lane | NEW | partial CATEGORY-ERROR (kernel, not lane) | PARK | +| X9 | receipt class table, key without `thought` (action cache) | PARTIAL | FITS (never addressed through W) | **PROBE PR-5** | +| X10 | path-dependent state never merged by output identity | ALREADY-HAVE | FITS | probe first, inside PR-5 / PR-7 | +| X11 | B&S column sampling + SVD sign structure | PARK-shaped | CATEGORY-ERROR | PARK until PR-6 un-parks it | +| X12 | lanes coupled through the pool ≈ NCD ⇒ not deflatable | NEW | FITS as a kill prediction | **PROBE PR-6** | +| X13 | KL aggregation loss | NEW-cond. | CATEGORY-ERROR | PARK | +| X14 | causal abstraction: the coarse map must commute with interventions (Beckers–Halpern; causal coarsening) | ALREADY-HAVE (anchor) | FITS as a necessary pre-check | PARK; never writes 59..63 | +| X15 | weak lumpability for the fixed initial law "fork from sealed main" | NEW | trivial with one base | folded into PR-3 | +| X16 | k-lumpability of a lag-k squash | NEW | not citable (abstract only) | PARK | +| X17 | head = the lane with most ops, or the lane's stationary mass under the driver | NEW | count ≠ QSD; stationary mass is endogenous and gives no evidence | most-ops only as a tie-break; **SKIP** stationary mass | +| X18 | head rule (a) ε on the question, (b) start-independence, (c) lossless subsumption, (d) a new root blocks the squash, (e) newer becomes head only if it refines | NEW | (b) CATEGORY-ERROR; (c) strongest; (d)/(e) FIT | **PROBE PR-7** with the order (d) block → (c)/(e) decide → (a) scope | +| X19 | drop history only when causally stable (op-based CRDT) | PARTIAL rhyme | FITS (eviction ≠ stability) | PROBE as bridge B7, low priority | +| X20 | log compaction / snapshot = fold of the prefix, valid iff apply is pure | ALREADY-HAVE | FITS | nothing to add | + +**Bridge vs firewall conflict, resolved.** The bridge architect kept (b) start-independence as head-rule step 4. The firewall critic called it a kernel property misapplied to a lane. The stricter verdict wins: (b) is dropped from the head rule. The ρ histogram per program (bridge B6) stays measurable as a description, never as a gate. + +## Head-selection answer to the follow-up (candidates; none measured) + +Applied after D-TGA-5 R1/R2 pass, as an ordered chain that can only refuse or narrow, never promote: + +1. **(d) Root block.** A child whose `roots` contain a root the head lacks is evidence, not redundancy. Refuse the squash with a new kind, `IndependentRoot`. +2. **(e)/(c) Refinement and subsumption.** The head's final state covers every cell the child agreed on, with no contradiction, and the child's receipt classes replay inside the head's base. This is the real head order; "newer" wins only when it refines. +3. **(a) Question scope.** Children that differ only outside the pre-registered question cells Q may merge with respect to Q. +4. **Tie-break.** Most ops, then lowest id. This is the current D-TGA-5 rule, demoted from semantics to tie-break. + +CE64 59..63 is read, never written. Choosing a head is not certification. + +## Pre-registered probes (top three first) + +All probes are new test files, with no production edits, run with `cargo test --release`, debug 0 and incremental off. Hot loops are reported in ns/op. Cold SVD or refinement is reported in µs and labelled "not a gate". Results are counts, folds and u64 hashes, never row sets. + +**PR-7 — head selection.** +- Ground truth is authored before any run. Families, each with 64 seeded variants: + - F1: the newer lane B refines the churning lane A. GT = B. + - F2: the lanes differ only outside Q. GT = merge w.r.t. Q. + - F3: the newer lane has the most ops and contradicts on Q. GT = refuse. + - F4: equal op counts and B refines. GT = B. +- Rules compared: (m) most ops, (e) ε on Q, (r) refines-older, (s) stationary mass (reported only). +- PASS: + - (r) ≥ 0.95 on F1, F3 and F4. + - (e) ≥ 0.95 on F2. + - (m) ≤ 0.5 on F1. KILL this prediction if (m) ≥ 0.95 on every family. +- Disable: drop the ⊇ check from (r). +- Silent twin: on #1736 `clean_lanes`, (r) returns "merge, no head", and the read equals P1. + +**PR-2 — commutation sweep.** +- Seeds 0..1023, L ∈ {2, 4, 8}, chains of 1..16 commits on 48 cells. +- Half of the fixtures are anomaly-free by construction; half carry one injected divergence or contradiction. +- 32 interleavings each. +- PASS: zero accepted mismatches, and zero refusals on the anomaly-free half. +- Reported only: the false-refusal rate. +- Disable: remove R2, after which accepted mismatches must be > 0. + +**PR-1 — locate the stochastic layer (the X1 kill).** +- 4096 receipts, each replayed 8 times. +- KILL X1 if D = 0, where D is the number of receipts with more than one distinct output fold. +- Locate arm: on the exo129 worlds, (row entropy H > 0) must equal (purity < 1). KILL the locate claim on any mismatch. +- Disable: put the replay index into the seed; D must then be 4096. + +**Further probes:** +- **PR-3:** partition refinement. R* = snap-block count ⇔ purity 1.0, and purity < 0.99 ⇒ R* > snap-blocks. Disable: a single refinement pass. +- **PR-4:** AXF bound on a seeded half-palette observable A over 6 hops, plus the inhomogeneous [L,U] arm. Disable: ε = 0. Silent twin: A as a union of PR-3 blocks gives ε = 0. +- **PR-5:** receipt classes without `thought`. + - PASS: zero classes with two distinct folds, and a dedupe ratio ≥ 10. + - Disable: drop `base` from the key. + - Silent twin: with `thought` in the key the ratio is exactly 1. + - Roots differing within a class are reported as merge-blocked. +- **PR-6:** NCD prediction. + - δ is the in-aggregate column spread on the driver chain and on exo129. + - PASS X12: δ > 0.2 and no spectral gap > 5. + - KILL X12, which un-parks X11: δ < 0.05 and gap > 10. + - Disable: give each lane its own slots. + +## Correction owed to the #1736 IDEAS block + +The "Outside grounding: the accumulation as a large Markov chain" block on #1736 (`IDEAS.md`, session 01Vnc) maps the 64×10⁶ ops onto one stochastic chain over cell states. It names P̂ as the certificate, and it offers the 4ε bound as a squash-gate tolerance. + +All three claims fail against the code: +- the ops are deterministic, so there is no P; +- the receipt is lossless and P̂ is lossy; +- a tolerance weakens the exact refusal. + +The 63-lanes-as-iid-columns arithmetic also breaks I-NOISE-FLOOR-JIRAK. The block's own four falsifiers stand. This entry asks for an append-only storno of the "certificate is P̂" and "4ε tolerance" bullets, written by the block's owner or after #1736 merges. It does not edit #1736. + +## Not searched + +- Datomic/XTDB history retention. +- Primary text of Kemeny–Snell, Buchholz 1994, Dayar–Stewart 1997, Larsen–Skou and Givan et al. (all secondhand). +- PyEMMA/MSMBuilder licences. PRISM and Storm licences are from memory. +- The ComposeTable source and the `ps2_*` tests: the P-S2 purity ≈ 0.47 is cited from the EXO-129 entry, not re-read. +- The MCGS paper (fetch failed). +- A primary source for lumpability of inhomogeneous chains beyond AXF's set-chain bound. + +## Sources (read grade) + +- **B&S, AXF:** READ-IN-FULL (main thread). +- **Beckers–Halpern arXiv 1812.03789 §3.1–3.2; Zhang–Wang arXiv 1802.02920 §1, Thm 2:** SECTION-READ. +- **Abstract only:** Geiger et al. arXiv 1304.6603; Zhu et al. arXiv 1907.00113; Duan–Ke–Wang arXiv 1811.02619; Storm arXiv 2002.07080; Baquero et al. arXiv 1710.04469; Derisavi–Hermanns–Sanders 2003 and Valmari–Franceschinis 2010 (abstracts); Geiger–Temmel arXiv 1212.4375. +- **Section read via summarizer:** the deeptime/PyEMMA CK-test tutorial (deeptime LGPL-3.0, checked). Kafka log compaction docs: SECTION-READ. +- **Secondhand:** Kemeny–Snell 1960; Rubino–Sericola 1989; Buchholz 1994; Dayar–Stewart 1997; Larsen–Skou 1989; Givan–Dean–Greig 2003; Chalupka et al. 1412.2309; Bazel hermeticity; git objects; event sourcing; MCTS transpositions. +- **Internal, VERIFIED-IN-CODE (scout 1):** receipt.rs:339-418; oracle.rs:67-122; slots.rs:174-234; squash_gate.rs:89-235 (pr1736); exo129_learned_lut_probe.rs:142-190; pearl.rs:282, 405-424; perturbation-sim eigen.rs:93. + +Council: premise auditor; scouts: code cartographer, internal prior art, literature, systems, concepts and ontology; co-architects: bridge, firewall and fit, falsifier. Session 01G22yT6. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index c2d7d6217..b7c5dcaa9 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,13 +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. -444 entries, 2026-08-06 .. 2026-10-23. +445 entries, 2026-08-06 .. 2026-10-23. | date | entry id | finding | file | |---|---|---|---| | 2026-10-23 | `ps2-compose-chain-preregistration` | | [2026-10-23-ps2-compose-chain-preregistration.md](2026-10-23-ps2-compose-chain-preregistration.md) | | 2026-10-23 | `ledger-revision-1635-1726` | | [2026-10-23-ledger-revision-1635-1726.md](2026-10-23-ledger-revision-1635-1726.md) | | 2026-10-23 | `exo129-learned-lut-preregistration` | | [2026-10-23-exo129-learned-lut-preregistration.md](2026-10-23-exo129-learned-lut-preregistration.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-22 | `probes-pd4-pe2-pd3` | | [2026-10-22-probes-pd4-pe2-pd3.md](2026-10-22-probes-pd4-pe2-pd3.md) | | 2026-10-22 | `pal256-salience-mp3-probe` | | [2026-10-22-pal256-salience-mp3-probe.md](2026-10-22-pal256-salience-mp3-probe.md) | | 2026-10-22 | `pal256-nars-bayes-evidence-contract` | | [2026-10-22-pal256-nars-bayes-evidence-contract.md](2026-10-22-pal256-nars-bayes-evidence-contract.md) | From 2d6071431607b14e2d5f323a6fd01a29722f8fde Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 10:11:42 +0000 Subject: [PATCH 2/3] board: append-only corrigendum to the thought-git Markov map (operator: substrate is not probabilistic) Records the operator DECISION that probabilistic models are counterfactuals certified by the cold egglog/eggcc compiler; withdraws the stochastic-layer, vote/stationary-mass and P-hat framings and the CR#11/ICR#31 naming error; PR-7 superseded by the CC2 proof-discovery plan. Nothing above the corrigendum is deleted. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- ...026-10-23-coresearch-thought-git-markov.md | 44 +++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/.claude/board/entries/2026-10-23-coresearch-thought-git-markov.md b/.claude/board/entries/2026-10-23-coresearch-thought-git-markov.md index 48d3e6cc8..7594281ea 100644 --- a/.claude/board/entries/2026-10-23-coresearch-thought-git-markov.md +++ b/.claude/board/entries/2026-10-23-coresearch-thought-git-markov.md @@ -162,3 +162,47 @@ The 63-lanes-as-iid-columns arithmetic also breaks I-NOISE-FLOOR-JIRAK. The bloc - **Internal, VERIFIED-IN-CODE (scout 1):** receipt.rs:339-418; oracle.rs:67-122; slots.rs:174-234; squash_gate.rs:89-235 (pr1736); exo129_learned_lut_probe.rs:142-190; pearl.rs:282, 405-424; perturbation-sim eigen.rs:93. Council: premise auditor; scouts: code cartographer, internal prior art, literature, systems, concepts and ontology; co-architects: bridge, firewall and fit, falsifier. Session 01G22yT6. + +## Corrigendum (2026-10-23, operator correction; append-only, nothing above is deleted) + +**DECISION** (operator, 2026-10-23, relayed in EXO-50 GPT:gpt-ada-01/…-11 and in chat): the SPO/CE64/Thought-Git +substrate is not probabilistic. Probabilistic "spoFC" semantics are legacy. +Every probabilistic model is a **counterfactual** (Rung 3), and it must be certified by the cold +egglog / eggcc-inspired reasoning compiler before it counts. +- **SCOPE:** Thought-Git knowledge, truth and squash semantics, and head selection. +- **BASIS:** the premise audit above (ops are deterministic, no P), plus the operator's architecture: multi-lane exploration + compiles into checked, reusable recipes. +- **REVISIT WHEN:** never on cost grounds. + +What this withdraws from the map above: +- **The stochastic layer as a home for the Markov tools.** The "Answer" section called the exo129 snap + kernel a legitimate stochastic layer. It is an artifact of lossy quantization: it is a legacy reading, not + a substrate property. Markov / MCMC / lumpability (X3–X8, X11–X13, and PR-4, PR-6) remain at most + specialized counterfactual research tools, and only where someone explicitly defines a stochastic process. + They are not Thought-Git's organizing mathematics. +- **Head by vote, stationary mass or P̂.** X17's stationary mass was already SKIP. Also withdrawn are: + - the chat-side proposal of a source-deduplicated majority vote; + - "certificate is P̂" (X1). + Agreement among lanes, at any count and with any root diversity, never confers proof authority. It + never moves 59..63. +- **Head rule.** The head of a thought family is preferably a NEW proof-carrying synthesis. It must have + lawfully admitted rules that preserve the children's required semantics, dependencies and replay + evidence, and it must pass the exact D-TGA-5 gate (no ε, no majority relaxation of R1/R2). + - If there is no proof, a candidate stays an unadmitted counterfactual. It is never squashed into a + claimed truth. + - A proof certifies a conditional law under stated axioms. Empirical, source and causal claims still + need independent attestation. + - Proof certificate, CE64 59..63 state and Thought-Git replay/commit witness are three separate objects. +- **Tactic naming error.** Chat-side text called #11 "ICR". #11 is CR (Contradiction Resolution) and + #31 is ICR (Iterative Counterfactual Reasoning). MPC #27 / HKF #34 are candidate generators, not + certified mergers. + +What survives unchanged: +- squash = path composition, checked by commutation (X2, PR-2); +- receipt classes keyed without `thought`, guarded by roots (PR-5); +- PR-1 as a short confirmation that lanes are not a stochastic chain; +- the requested storno of the #1736 IDEAS "certificate is P̂" and "4ε tolerance" bullets. + +PR-7 is superseded: the head-selection probe moves to the CC2 proof-discovery plan +(`entries/2026-10-23-cc2-proof-compiling-gap-map.md`, when it lands). Its F5 synthesis fixture and its +F6 correlated-copies fixture keep their shape, with ground truth from an independent oracle, never a vote. From 7d30a15f6e7e206cc80a0ea8217b2ccfb27b7481 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 10:15:22 +0000 Subject: [PATCH 3/3] board: CC2 gap map + staged falsifiers for proof-compiling Thought-Git Source-grounded matrix of the math-compiler lab work (#1690/#1693/#1696/#1698/#1707): nothing SHIPPED; independent proof check, counterexample-driven refutation, full-domain lowering validation, second-fresh-binding reuse and Thought-Git linkage ABSENT. 34 tactics audited as a proposal vocabulary (no kernel emits a derivation; 15 unique signatures). Minimal typed ABI reusing existing names; stages S1-S6 with positive/negative/silent/disable tests. Plan only; no implementation. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .../2026-10-23-cc2-proof-compiling-gap-map.md | 148 ++++++++++++++++++ .claude/board/entries/README.md | 3 +- 2 files changed, 150 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-23-cc2-proof-compiling-gap-map.md diff --git a/.claude/board/entries/2026-10-23-cc2-proof-compiling-gap-map.md b/.claude/board/entries/2026-10-23-cc2-proof-compiling-gap-map.md new file mode 100644 index 000000000..caac71c74 --- /dev/null +++ b/.claude/board/entries/2026-10-23-cc2-proof-compiling-gap-map.md @@ -0,0 +1,148 @@ +# 2026-10-23 — CC2: proof-compiling Thought-Git, current state and staged falsifiers + +**Status:** GAP MAP + PRE-REGISTRATION PLAN. Nothing is implemented by this entry. Each stage below needs its +file ownership agreed in EXO-50 before any write. + +**Owner:** CC2 (session 01G22yT6). Directed by the operator correction relayed in EXO-50 +`GPT:gpt-ada-01/20261023-proof-compiling-thoughts-11`. Read with the corrigendum in +`entries/2026-10-23-coresearch-thought-git-markov.md`. + +## Research question + +Can billions of transient exploratory folds produce a small number of independently checked, reusable +mathematical reasoning primitives? Success would mean that later problems execute those primitives directly +instead of rediscovering them. + +The success metric is checked laws that are actually reused, per unit of exploration folds plus cold compile µs. +The consensus probability and the number of agreeing lanes are not success metrics. + +## Current state (read at origin/main 3f1658dab; every cell backed by a file read) + +Both compiler crates are lab crates with their own `[workspace]`, excluded from the root workspace, with no +dependents and with separate CI: +- `crates/egglog-r2il-probe`: #1690 E1, #1693 ReplayCapsule, #1696 catalogue + heritage, #1698 fixes; +- `crates/dr-math-binding-probe`: #1700 to #1707. + +STATUS_BOARD has no D-DRMC rows. `.claude/plans/dr-mathematical-compiler-v1.md` calls itself a PROPOSAL. +**Nothing in this matrix is SHIPPED.** + +| capability | state | evidence | +|---|---|---| +| saturation finds the rewrite | PROBED | egglog-r2il-probe tests/e1.rs:27-41; dr-math-binding-probe tests/relcomp.rs:292-299 (all 14 orders of a 5-chain) | +| a proof script is produced | PROBED | lib.rs:277-289 (`prove-variants`); relcomp.rs:294-315 | +| the proof is checked by an INDEPENDENT checker | **ABSENT** | egglog `check_proof` is `pub(crate)` (egglog src/proofs/proof_checker.rs:574) and checks its own DAG. `ReplayCapsule::recheck` re-runs egglog and compares bytes (artifact.rs:106-128). The fork's forged-proof tests live only inside egglog. | +| a false rule is refuted by a counterexample and never catalogued | **ABSENT as discovery** | Refusals are a static domain table (laws.rs:372-381), egglog failing to prove, contradictory premises (artifact.rs:66), and heritage atoms that do not replay (tests/heritage.rs:249-261). No proposed rewrite is ever falsified by a generated input. | +| lowering validated against source semantics | PROBED, differential only | an i128 oracle at 7 inputs (e1.rs:45-57) and 4 points at promote (catalogue.rs:433-435); a structural round-trip with no R2IL target (relcomp.rs:380-386); `target_abi` stored but never checked | +| guarded certificate / catalogue entry | PROBED | catalogue `BindingWitness`, `TargetAbi`, `CheckedRange` overflow (catalogue.rs:310-363). `RecipeCertificate` has no public constructor and Bag/Set guard via `LawShape` (recipe.rs:83-99). `admit_recipe` always ends `NoCertifiedCompiler` (recipe.rs:178-184). | +| a cached hit runs without egglog | PROBED for no baseline call; egglog calls not counted | tests/catalogue.rs:41-50; the no-egglog part holds only by reading catalogue.rs:493 | +| reuse on a SECOND FRESH binding | **ABSENT** | any binding change falls back to the baseline (tests/catalogue.rs:78-82). The store is one slot per key, so a second promotion overwrites the first (REVIEW_GATES E-MULTIBIND). Certificate reuse on a second frame is OPEN (drmc-5). | +| cold and hot costs | PARTIAL | E1 encode 2-4 µs; lower + execute 5-15 µs per call (a `FoldDialect` is built per call, lower.rs:642-647); egglog cold 21 084-28 793 µs. Relcomp eval 4.4-10.8 µs; its cold proof is written as "≈12.5 ms" (README:30), which breaks the µs-only rule for cold costs. Catalogue costs are synthetic. | +| candidate rewrites generated by lanes | **ABSENT** | laws are hand-written (laws.rs:398-407; relcomp.rs:264-266); the 27 heritage atoms are a hypothesis | +| linkage to Thought-Git lanes / receipts | **ABSENT** | listed as a "future gate" in HERITAGE_STUDY:28-37 and REVIEW_1690_1695:73-79 | +| 34 tactics as proposal vocabulary | PLANNED / UNPROVEN | see below | + +**The 34 tactics** (`crates/lance-graph-ogar/src/recipe_kernels.rs`, `ThoughtCtx` at :47-64). +- The kernels act on f32 scores, an anonymous `Vec` of candidates, and `(u32, f32, f32)` beliefs. None + emits a term, premise, rule or provenance, so none produces a derivation today. +- "23/34 distinguishable" (#995) counts signature classes. Only 15 ids have a unique signature. 14 kernels + move confidence. #19, #24 and #34 are Demonstrations that ignore the context. +- MPC #27 is a lossy mean: a candidate generator, not a merger. HKF #34 is a demonstration. +- #11 is CR and #31 is ICR. ICR is not a Pearl counterfactual (`ISS-PEARL-VOCABULARY-WITHOUT-PEARL-MECHANICS`). +- `select_tactic` reaches only 8 of the 34 and shadows ICR. Orchestration-to-recipe (O2) is still absent, so + a proof loop must name its tactics explicitly. + +## Minimal typed ABI (types only; existing names reused) + +Reused types: +- `FnIndex`/`Recipe` (recipe_vocab.rs:108-121, recipes.rs:66); +- `Problem`/`Eq`/`Tm`/`RuleId`/`Arith` (egglog-r2il-probe lib.rs:46-64, term.rs:18, laws.rs:17-84); +- `ReplayCapsule`/`ReplayRefusal` (artifact.rs:17-42); +- `SemanticKey`/`BindingWitness`/`TargetAbi` (catalogue.rs:17-166); +- `BaseRef`/`Fold`/`Receipt.roots`/`MetaKey` (thought-git-probe receipt.rs). + +New, minimal: +- `AxiomSet { domain, rules }`; `PremiseSet { premises: Problem, axioms }`; +- `Evidence { base, sources: Fold, roots: u64 }`; +- `TacticProposal { recipe: FnIndex, thought: u32, premises, evidence }`; +- `Candidate::{Equation, Rewrite}`; +- `Counterexample { binding, compiled, oracle }`; +- `DerivationVerdict::{Proved(ProofRef), Disproved(Counterexample), Inconclusive(ReplayRefusal)}`; +- `ProofRef { key: SemanticKey, receipt: MetaKey }`; +- `CompiledRecipeKey { semantic, axioms, abi, scope }`. This is the same guard tuple `Catalogue::execute_or` + already checks (catalogue.rs:257-265). + +Three separate objects that must stay separate: +- the proof certificate (`ProofRef` → capsule); +- the CE64 59..63 state, which no proof, vote or synthesis raises by itself; +- the Thought-Git receipt / commit witness. + +## Smallest vertical loop and its staged falsifiers + +Every stage needs a pre-registered entry and four tests: +- positive; +- negative; +- silent twin (a non-trivial input on which it must NOT fire); +- disable (the guard removed, test must go red; anchor asserted before patching). + +Hot costs are in ns, cold costs in µs, never ms. One additive PR per stage. Lab crates only. + +**Tactic set:** +- proposer: RCR #4 (effect → antecedent), or HTD #2; +- adversaries: CR #11 (contradictory premises) and ASC #7 (negation / counterexample search); +- verifier: SPP #30 (two independent paths must agree); +- optional budget pruner: TCP #5. + +Each is called by id, never through `select_tactic`. + +- **S1 — adversarial counterexample gate. The KILL test asked for: a false rule never enters the catalogue.** + - Setup: several lanes each emit `TacticProposal`s with candidate rewrites over E1 terms. A bounded + exhaustive i128 oracle sweep runs BEFORE egglog. + - PASS: every false candidate yields `Disproved(Counterexample)` and never reaches saturation or the catalogue. + Every true candidate passes on to egglog. + - Disable: skip the oracle, and a false rewrite enters. + - Silent twin: an all-true proposal set yields zero refusals. +- **S2 — independent proof check (E-PROOF).** + - egglog exports its proof as a portable DAG: premises, rule instances, edges. A checker outside egglog + replays each step against `AxiomSet`. + - PASS: the genuine proof checks. Each of five mutations is rejected: a premise, a law, an edge, the axiom + set, the ABI. + - Disable: a checker that skips the rule match must go red. + - Needs an `egglog` fork export. That fork is this session's repo (tasks #72-74), so it is coordinated in + EXO-50. +- **S3 — lowering validated over the full bounded domain.** + - E1 R2IL lowering is checked exhaustively over a stated domain (e.g. all i16 inputs, or a symbolic proof). + `target_abi` is enforced. + - PASS: zero mismatches, and changing the ABI or an overflow case refuses. + - Disable: drop the overflow guard, and a wrapping input must mismatch. +- **S4 — reuse on a second fresh binding with zero egglog calls.** + - The catalogue goes from one slot per key to a key set with a binding witness per frame. An egglog + invocation counter is added. + - PASS: binding B2 (new frame, new data) executes the cached recipe with counter = 0 and is equal to the + oracle. A stale scope, a changed ABI, wrong axioms, or bag-vs-set all refuse. + - Disable: an ignored binding check lets a stale scope through. +- **S5 — Thought-Git link (joint with CC1).** + - A proved recipe is referenced from a lane receipt by `ProofRef`. CC1's squash keeps the receipt and + `ProofRef` and drops the exploratory folds. + - F5 (a synthesised head covers complementary children) and F6 (correlated copies get no proof authority; + validity is decided by the S1/S2 oracle and checker) are CC1's, in #1736. + - Joint check: squash refuses if any child holds an unproved claim that the head would drop. +- **S6 — the honest budget.** Measured separately: + - hot fold throughput (ns/fold); + - cold proof discovery + compile (µs); + - certificate and proof bytes vs raw exploratory trace bytes; + - cache-hit latency (ns); + - reuse count across fresh bindings. + + The 64 × 10⁶ × 30 s figure is a target. Unless S6 measures it, it is reported as unattained, and proof + search is never promised to finish within the budget. + +## Owner-side defects found (reported, not fixed here) + +- "≈12.5 ms" and "21–29 ms" cold-cost wording: README:30 of dr-math-binding-probe and the stage-b-e1 entry. + It should be µs under the scoped cold-cost exception. +- egglog is pinned `branch = "main"` in both lab crates (REVIEW_GATES E-PROOF), which is not a version pin. +- `RecipeCertificate.target_abi` is stored but never checked by `certify_reassociation`. + +Sources: two read-only audits run for this entry (compiler evidence; 34-tactic ABI). Every file:line above was +read by the auditing agent, and the main thread spot-checked the merge provenance. Simulated collision groups +for #995: scratchpad `sim/sim2.py`, which reproduces 23 classes / 15 colliding pairs. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index b7c5dcaa9..c92e2d79c 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. -445 entries, 2026-08-06 .. 2026-10-23. +446 entries, 2026-08-06 .. 2026-10-23. | date | entry id | finding | file | |---|---|---|---| @@ -33,6 +33,7 @@ exactly one of them, never both. | 2026-10-23 | `ledger-revision-1635-1726` | | [2026-10-23-ledger-revision-1635-1726.md](2026-10-23-ledger-revision-1635-1726.md) | | 2026-10-23 | `exo129-learned-lut-preregistration` | | [2026-10-23-exo129-learned-lut-preregistration.md](2026-10-23-exo129-learned-lut-preregistration.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 | `cc2-proof-compiling-gap-map` | | [2026-10-23-cc2-proof-compiling-gap-map.md](2026-10-23-cc2-proof-compiling-gap-map.md) | | 2026-10-22 | `probes-pd4-pe2-pd3` | | [2026-10-22-probes-pd4-pe2-pd3.md](2026-10-22-probes-pd4-pe2-pd3.md) | | 2026-10-22 | `pal256-salience-mp3-probe` | | [2026-10-22-pal256-salience-mp3-probe.md](2026-10-22-pal256-salience-mp3-probe.md) | | 2026-10-22 | `pal256-nars-bayes-evidence-contract` | | [2026-10-22-pal256-nars-bayes-evidence-contract.md](2026-10-22-pal256-nars-bayes-evidence-contract.md) |