From 0dca6c521e61be7f7f6e2597171617786fd5d3c8 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 09:19:32 +0000 Subject: [PATCH 1/8] board: pre-register the D-TGA-5 squash gate probe (most-updated lane, contradiction gate, blame) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- ...-23-d-tga-5-squash-gate-preregistration.md | 88 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 2 files changed, 90 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md diff --git a/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md b/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md new file mode 100644 index 000000000..6c69ff837 --- /dev/null +++ b/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md @@ -0,0 +1,88 @@ +# 2026-10-23: D-TGA-5 lab precursor — squash the chain of origin into the most-updated lane, gated on contradiction (pre-registration) + +**Status:** PRE-REGISTERED. Everything above the line was fixed before any +probe code was written. Results go below it. + +**Source:** an operator direction (provenance, not validation): the first +squash gate is "which thought lane was updated most". That lane's chain of +origin is squashed into one lane, gated against contradiction. Lance then +carries the delta, the compiled order and a seal reference, not every +operation. Claim: EXO-50 `session_01VncKoyG6JkpsoqhqTGTv3f/034`. +STATUS_BOARD D-TGA-5 (`squash_into` and blame) is the deliverable this +precedes. + +## Model + +- **A lane** is `(id ∈ 1..=63, chain: Vec)` in origin order. Each + thought is one batch of writes. `ops(lane)` is the total number of writes + in its chain. +- **A lane's final state** `F_l` is its chain folded in order, with later + writes replacing earlier ones at the same cell. A rewrite inside one lane's + own chain is history, not a contradiction. +- **The gate** squashes a set of lanes: + - **Target:** the lane with the most ops; ties go to the lowest id. + - **R1, contradiction:** some `F_l` writes a cell that has a given, with a + different value. Refuse, naming the cell, the given, the offer and the + lane. + - **R2, divergence:** two lanes' final states differ at one cell. Refuse, + naming the cell and every `(value, lane)`. + - Otherwise accept. +- **Output of an accepted squash:** + - `cells`: the union of the final states, without values that agree with a + given; + - `order`: every `(lane, thought id)` in lane-ascending, chain order; + - `blame`: for each cell, a `u64` bitset with bit `l` set for every lane + that wrote the cell anywhere in its chain; + - `seal`: FNV-1a 64 over the ordered history. + +## Predictions (each one a test) + +- **P1, equivalence.** Landing the squashed thought through the D-TGB-0 + oracle (`next_version`) gives the same `Version`, and the same `read` on + every fixture cell, as landing every lane's final state together. +- **P2, divergence is refused.** Two lanes disagree on one cell → + `Err(Divergence)` naming both. The naive `oracle::squash` keeps the later + value on the same input; the test shows that difference. +- **P3, contradiction is refused.** A lane offers 999 for a given → + `Err(Contradiction)`. +- **P4, silence twin, on non-trivial input.** Disjoint lanes are accepted. A + lane that rewrites its own cell several times is accepted. Two lanes that + write the same value to one cell are accepted. +- **P5, target is the most-updated lane.** The fixture puts the most ops on + the highest lane id, so neither "lowest id" nor "first given" can pass. +- **P6, blame survives the squash.** For every cell, `blame` equals the set + of writing lanes computed independently from the raw chains, including a + cell two lanes wrote with the same value (both bits set). +- **P7, delta, not history.** + - Setup: k rounds of one lane rewriting the same N cells, k ∈ {1, 2, 4, + …, 64}. + - `cells` stays N for every k, while the writes the history holds grow as + k·N. + - Stated plainly: `order` grows with the number of thoughts (k), not with + writes per thought. The seal is one value. + +## Disables (each must turn its named test red) + +| | disable | test that must turn red | +|---|---|---| +| D1 | no divergence check | P2 | +| D2 | no contradiction check | P3 | +| D3 | divergence checked across every chain entry instead of across final states | P4 | +| D4 | target = lowest lane id | P5 | +| D5 | blame keeps only the target's bit | P6 | + +## Kill + +P1 fails, which means squash-then-land is not landing the finals. Or the gate +refuses P4's inputs, which means it fires on everything. + +## Out of scope (an IDEAS row, not claimed) + +- Promoting CE64 epistemic bits 59..63 (correlation → causality, MUL + confidence) at squash time. +- An egglog / eggcc certificate that replaces the order list with a proof + reference. +- Any Lance storage, and any timing. Under this file's rules only counts are + reported. + +--- diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index c2d7d6217..bcda1dcf9 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 | `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-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 31552ec204b4398f3c920a4cbf09e70699c56b2a Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 09:20:59 +0000 Subject: [PATCH 2/8] =?UTF-8?q?thought-git-probe:=20squash=20gate=20probe?= =?UTF-8?q?=20(D-TGA-5=20precursor)=20=E2=80=94=20most-updated=20target,?= =?UTF-8?q?=20contradiction=20gate,=20blame?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- crates/thought-git-probe/tests/squash_gate.rs | 376 ++++++++++++++++++ 1 file changed, 376 insertions(+) create mode 100644 crates/thought-git-probe/tests/squash_gate.rs diff --git a/crates/thought-git-probe/tests/squash_gate.rs b/crates/thought-git-probe/tests/squash_gate.rs new file mode 100644 index 000000000..be455bddc --- /dev/null +++ b/crates/thought-git-probe/tests/squash_gate.rs @@ -0,0 +1,376 @@ +//! D-TGA-5 lab precursor: squash every lane's chain of origin into the +//! most-updated lane, gated on contradiction, with blame preserved. +//! +//! Pre-registered in +//! `.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md` +//! before this file was written. Predictions P1..P7 are the tests below; the +//! disables D1..D5 are named on the test each must turn red. +//! +//! The gate lives here, in the test, because it is a lab question: it does +//! not change `oracle.rs`, `slots.rs` or `receipt.rs`. + +use std::collections::{BTreeMap, BTreeSet}; + +use thought_git_probe::fixtures::{Cell, Outcome, Thought, cell, givens, main_version}; +use thought_git_probe::oracle::{Givens, Version, next_version, squash}; + +/// A thought lane: its id (1..=63) and its chain of origin, oldest first. +struct Lane { + id: u8, + chain: Vec, +} + +impl Lane { + fn new(id: u8, chain: Vec) -> Self { + assert!((1..=63).contains(&id), "lane {id} outside 1..=63"); + Self { id, chain } + } + + /// Total writes in the chain. + fn ops(&self) -> usize { + self.chain.iter().map(|t| t.writes.len()).sum() + } + + /// The chain folded in order: later writes replace earlier ones. + fn final_state(&self) -> BTreeMap { + let mut f = BTreeMap::new(); + for t in &self.chain { + for &(c, v) in &t.writes { + f.insert(c, v); + } + } + f + } +} + +#[derive(Debug, PartialEq, Eq)] +enum Refusal { + Contradiction { + cell: Cell, + given: u64, + offered: u64, + lane: u8, + }, + Divergence { + cell: Cell, + offers: Vec<(u64, u8)>, + }, +} + +#[derive(Debug)] +struct Squashed { + target: u8, + cells: BTreeMap, + order: Vec<(u8, u32)>, + blame: BTreeMap, + seal: u64, +} + +impl Squashed { + /// The squash as one committed thought, for the oracle. + fn as_thought(&self, id: u32) -> Thought { + Thought::new( + id, + self.cells.iter().map(|(&c, &v)| (c, v)).collect(), + Outcome::Commit, + ) + } +} + +fn fnv1a(seal: &mut u64, x: u64) { + for b in x.to_le_bytes() { + *seal ^= u64::from(b); + *seal = seal.wrapping_mul(0x0000_0100_0000_01b3); + } +} + +/// The gate. Lanes are taken in ascending id order whatever order they are +/// passed in. +fn squash_gate(g: &Givens, lanes: &[Lane]) -> Result { + let mut lanes: Vec<&Lane> = lanes.iter().collect(); + lanes.sort_by_key(|l| l.id); + + // Target: most ops; on a tie the lowest id (max_by_key keeps the last + // maximum, so compare on (ops, Reverse(id))). + let target = lanes + .iter() + .max_by_key(|l| (l.ops(), std::cmp::Reverse(l.id))) + .map_or(0, |l| l.id); + + // R1, then R2, over final states only. + let mut offers: BTreeMap> = BTreeMap::new(); + for l in &lanes { + for (c, v) in l.final_state() { + if let Some(&given) = g.0.get(&c) { + if given != v { + return Err(Refusal::Contradiction { + cell: c, + given, + offered: v, + lane: l.id, + }); + } + continue; // agreement with a given is not stored + } + offers.entry(c).or_default().insert((v, l.id)); + } + } + let mut cells = BTreeMap::new(); + for (c, set) in offers { + let values: BTreeSet = set.iter().map(|&(v, _)| v).collect(); + if values.len() > 1 { + return Err(Refusal::Divergence { + cell: c, + offers: set.into_iter().collect(), + }); + } + cells.insert(c, *values.iter().next().expect("one value")); + } + + let mut order = Vec::new(); + let mut blame: BTreeMap = BTreeMap::new(); + let mut seal = 0xcbf2_9ce4_8422_2325_u64; + for l in &lanes { + for t in &l.chain { + order.push((l.id, t.id)); + fnv1a(&mut seal, u64::from(l.id)); + fnv1a(&mut seal, u64::from(t.id)); + for &(c, v) in &t.writes { + *blame.entry(c).or_default() |= 1u64 << l.id; + fnv1a(&mut seal, u64::from(c.row)); + fnv1a(&mut seal, u64::from(c.lane)); + fnv1a(&mut seal, v); + } + } + } + + Ok(Squashed { + target, + cells, + order, + blame, + seal, + }) +} + +fn commit(id: u32, writes: Vec<(Cell, u64)>) -> Thought { + Thought::new(id, writes, Outcome::Commit) +} + +/// Three lanes, no anomaly: lane 7 rewrites its own cell twice, lanes 3 and 7 +/// agree on (6, 2), lane 12 has the most ops and agrees with a given. +fn clean_lanes() -> Vec { + vec![ + Lane::new( + 3, + vec![commit(1, vec![(cell(4, 1), 41)]), commit(2, vec![(cell(6, 2), 62)])], + ), + Lane::new( + 7, + vec![ + commit(3, vec![(cell(5, 1), 50)]), + commit(4, vec![(cell(5, 1), 51)]), + commit(5, vec![(cell(5, 1), 52), (cell(6, 2), 62)]), + ], + ), + Lane::new( + 12, + vec![ + commit(6, vec![(cell(8, 1), 81), (cell(8, 2), 82), (cell(0, 0), 100)]), + commit(7, vec![(cell(9, 1), 91), (cell(9, 2), 92), (cell(10, 1), 101)]), + ], + ), + ] +} + +/// The cells every fixture here touches, for the read comparison. +fn probe_cells() -> Vec { + (0..12) + .flat_map(|r| (0..4).map(move |l| cell(r, l))) + .collect() +} + +/// P1. Kill condition if it fails: squash-then-land is not land-the-finals. +#[test] +fn p1_landing_the_squash_equals_landing_every_final_state() { + let g = givens(); + let lanes = clean_lanes(); + let s = squash_gate(&g, &lanes).expect("clean lanes squash"); + + let finals: Vec = lanes + .iter() + .map(|l| commit(1000 + u32::from(l.id), l.final_state().into_iter().collect())) + .collect(); + let via_finals = next_version(&g, &main_version(), &finals); + let via_squash = next_version(&g, &main_version(), &[s.as_thought(999)]); + + assert_eq!(via_squash, via_finals, "squash differs from landing the finals"); + for c in probe_cells() { + assert_eq!(via_squash.read(&g, c), via_finals.read(&g, c), "read at {c:?}"); + } + // Anti-vacuity: the comparison covers a rewritten cell and a shared cell. + assert_eq!(via_squash.read(&g, cell(5, 1)), Some(52)); + assert_eq!(via_squash.read(&g, cell(6, 2)), Some(62)); +} + +/// P2. Disable D1 (no divergence check) turns this red. +#[test] +fn p2_two_lanes_that_disagree_are_refused() { + let g = givens(); + let lanes = vec![ + Lane::new(4, vec![commit(1, vec![(cell(5, 2), 7)])]), + Lane::new(9, vec![commit(2, vec![(cell(5, 2), 8)])]), + ]; + assert_eq!( + squash_gate(&g, &lanes).err(), + Some(Refusal::Divergence { + cell: cell(5, 2), + offers: vec![(7, 4), (8, 9)], + }) + ); + // The naive squash keeps the later value on the same input: the gate is + // what stops a silent overwrite. + let naive = squash(1, &[lanes[0].chain[0].clone(), lanes[1].chain[0].clone()]); + assert_eq!(naive.writes, vec![(cell(5, 2), 8)]); +} + +/// P3. Disable D2 (no contradiction check) turns this red. +#[test] +fn p3_a_lane_that_overwrites_a_given_is_refused() { + let g = givens(); + let lanes = vec![ + Lane::new(2, vec![commit(1, vec![(cell(4, 2), 42)])]), + Lane::new(5, vec![commit(2, vec![(cell(1, 0), 999)])]), + ]; + assert_eq!( + squash_gate(&g, &lanes).err(), + Some(Refusal::Contradiction { + cell: cell(1, 0), + given: 101, + offered: 999, + lane: 5, + }) + ); +} + +/// P4, the silence twin. Disable D3 (divergence over every chain entry) +/// turns this red: lane 7's own rewrites of (5, 1) would read as a +/// disagreement. +#[test] +fn p4_rewrites_in_one_lane_and_agreement_across_lanes_are_accepted() { + let g = givens(); + let lanes = clean_lanes(); + // Non-trivial: the input really has an in-lane rewrite and a shared cell. + let rewrites: BTreeSet = lanes[1] + .chain + .iter() + .flat_map(|t| t.writes.iter()) + .filter(|(c, _)| *c == cell(5, 1)) + .map(|&(_, v)| v) + .collect(); + assert_eq!(rewrites.len(), 3, "fixture lost its in-lane rewrite"); + assert!(squash_gate(&g, &lanes).is_ok()); +} + +/// P5. Disable D4 (target = lowest lane id) turns this red. +#[test] +fn p5_the_target_is_the_most_updated_lane() { + let lanes = clean_lanes(); + let ops: Vec<(u8, usize)> = lanes.iter().map(|l| (l.id, l.ops())).collect(); + assert_eq!(ops, vec![(3, 2), (7, 4), (12, 6)]); + let s = squash_gate(&givens(), &lanes).expect("clean lanes squash"); + assert_eq!(s.target, 12); + + // A tie goes to the lowest id, deterministically. + let tie = vec![ + Lane::new(20, vec![commit(1, vec![(cell(4, 1), 1)])]), + Lane::new(11, vec![commit(2, vec![(cell(4, 2), 2)])]), + ]; + assert_eq!(squash_gate(&givens(), &tie).expect("tie squash").target, 11); +} + +/// P6. Disable D5 (blame keeps only the target's bit) turns this red. +#[test] +fn p6_blame_names_every_lane_that_wrote_a_cell() { + let lanes = clean_lanes(); + let s = squash_gate(&givens(), &lanes).expect("clean lanes squash"); + + // Independent reference from the raw chains. + let mut expected: BTreeMap = BTreeMap::new(); + for l in &lanes { + for t in &l.chain { + for &(c, _) in &t.writes { + *expected.entry(c).or_default() |= 1u64 << l.id; + } + } + } + assert_eq!(s.blame, expected); + assert_eq!( + s.blame[&cell(6, 2)], + (1 << 3) | (1 << 7), + "a cell two lanes agreed on keeps both lanes" + ); + assert_eq!(s.blame[&cell(0, 0)], 1 << 12, "agreement with a given is still blamed"); +} + +/// P7. The stored delta does not grow with the history. +#[test] +fn p7_the_delta_stays_n_cells_while_the_history_grows() { + const N: u32 = 8; + let mut rows = Vec::new(); + for k in [1u32, 2, 4, 8, 16, 32, 64] { + let chain: Vec = (0..k) + .map(|round| { + commit( + round, + (0..N) + .map(|i| (cell(4 + i, 1), u64::from(round * 100 + i))) + .collect(), + ) + }) + .collect(); + let lane = Lane::new(1, chain); + let history = lane.ops(); + let s = squash_gate(&givens(), &[lane]).expect("one lane squash"); + rows.push((k, history, s.cells.len(), s.order.len())); + assert_eq!(s.cells.len(), N as usize, "delta at k = {k}"); + assert_eq!(history, (k * N) as usize, "history at k = {k}"); + assert_eq!(s.order.len(), k as usize, "order is one entry per thought"); + // The delta holds the LAST round's values. + assert_eq!(s.cells[&cell(4, 1)], u64::from((k - 1) * 100)); + } + println!("k, history writes, delta cells, order entries: {rows:?}"); +} + +/// The seal changes when the history changes, and only then. +#[test] +fn the_seal_depends_on_the_ordered_history() { + let g = givens(); + let a = squash_gate(&g, &clean_lanes()).expect("squash").seal; + let b = squash_gate(&g, &clean_lanes()).expect("squash").seal; + assert_eq!(a, b, "same history, same seal"); + + let mut changed = clean_lanes(); + changed[1].chain.swap(0, 1); // same writes, other order + let c = squash_gate(&g, &changed).expect("squash").seal; + assert_ne!(a, c, "reordering the chain must change the seal"); +} + +/// The squash agrees with the oracle's own divergence record: where the +/// gate refuses, landing the finals records a `Divergence` on the same cell. +#[test] +fn a_refused_squash_is_a_divergence_the_oracle_also_records() { + let g = givens(); + let lanes = vec![ + Lane::new(4, vec![commit(1, vec![(cell(5, 2), 7)])]), + Lane::new(9, vec![commit(2, vec![(cell(5, 2), 8)])]), + ]; + let finals: Vec = lanes + .iter() + .map(|l| commit(u32::from(l.id), l.final_state().into_iter().collect())) + .collect(); + let v: Version = next_version(&g, &main_version(), &finals); + assert_eq!(v.divergences.len(), 1); + assert_eq!(v.divergences[0].cell, cell(5, 2)); + assert!(squash_gate(&g, &lanes).is_err()); +} From ce60db62cf1aa0fe461b0e4fcf6e9415dbfb3643 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 09:24:21 +0000 Subject: [PATCH 3/8] board + probe: D-TGA-5 squash gate measured (7/7, 5 disables red); IDEAS row 'a certificate replaces the deltas' MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit squash_gate.rs: fmt only. Entry results: landing the squash equals landing the finals; blame over lanes survives; delta stays N while history grows k·N. STATUS_BOARD D-TGA-5 -> In PR (lab precursor). IDEAS: certificate replaces deltas, with 01G22yT6's determinism falsifier as next probe. FRUITS / entries / supersession indexes regenerated. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .claude/board/FRUITS.md | 3 +- .claude/board/IDEAS.md | 55 ++++++++++++++++++ .claude/board/STATUS_BOARD.md | 2 +- ...-23-d-tga-5-squash-gate-preregistration.md | 57 ++++++++++++++++++- crates/thought-git-probe/tests/squash_gate.rs | 39 ++++++++++--- 5 files changed, 145 insertions(+), 11 deletions(-) diff --git a/.claude/board/FRUITS.md b/.claude/board/FRUITS.md index 0cdbcdd4c..5f9e56fbf 100644 --- a/.claude/board/FRUITS.md +++ b/.claude/board/FRUITS.md @@ -4,7 +4,7 @@ Generated by `.claude/tools/fruits_index.py --write`. Do not hand-edit: add or change a `**Fruit:**` line on the ledger row and regenerate. CI fails when this file is stale. -Open: 24. Closed: 0. +Open: 25. Closed: 0. ## discovery torque @@ -16,6 +16,7 @@ Open: 24. Closed: 0. | tier | row | status | ledger | |---|---|---|---| +| High-signal | 2026-10-23 — A certificate replaces the deltas: lane 0 keeps the delta, a receipt or seal, and in time a proof reference — never the operations | Open. | `IDEAS.md` | | High-signal | 2026-10-23 — One replay that checks proof, receipt and commit witness together | Open. | `IDEAS.md` | | High-signal | 2026-10-23 — OGAR #357's first kill test (TLAC-P01) is now buildable from real guards | Open. | `IDEAS.md` | | High-signal | 2026-10-23 — The five unrun D-DRMC probes: X6, X7, X8, X16, X18 | Open | `IDEAS.md` | diff --git a/.claude/board/IDEAS.md b/.claude/board/IDEAS.md index c6069f648..23b5782e6 100644 --- a/.claude/board/IDEAS.md +++ b/.claude/board/IDEAS.md @@ -87,6 +87,61 @@ Agents filter by `@`-mention or domain to see what's theirs. (Prepend new ideas here with today's date. Format:) +## 2026-10-23 — A certificate replaces the deltas: lane 0 keeps the delta, a receipt or seal, and in time a proof reference — never the operations + +`[P1 @thought-struct-scribe @truth-architect domain:thought-git D-TGA-5 D-TGB-4 D-TGB-7 D-DRMC D-CGW-4]` + +Operator direction (provenance): lane 0 is main, 1..63 are thoughts, and each +lane may run on the order of 10^6 operations. Written with session 01G22yT6's +mapping (EXO-50, 2026-10-23). + +**Storage arithmetic, not a measurement.** 64 lanes × 10^6 operations is +6.4·10^7 deltas per cycle: 1–2 GB at 16–32 bytes each, or 33 GB at 512-byte +rows. A few cycles a minute reaches terabytes within hours. A receipt per +landed thought is about 64 × ~100 bytes per cycle. So deltas stay in RAM and +die at squash; only the squashed delta, receipts and seals reach disk. + +**What exists.** +- **D-TGB-4** (#1674, EXO-58 done) replaces history with a receipt. It + proves only the replay half, not admissibility. +- **egglog** checks a proof for every admissible solution. +- **DR64** refuses every recipe with `NoCertifiedCompiler`. That is the + certified-compiler-boundary row below, and its scope is the operator's call. +- **The joint replay** (proof + receipt + lane read) is the 2026-10-23 IDEAS + row below. +- **The causal verdict** is computed (`pearl.rs:259`) but promotes nothing + (ISS-D-CGW-4-PROMOTION-GATE). + +**The rungs.** +1. **The gate:** squash every chain of origin into the most-updated lane, + refusing on contradiction or divergence, with blame kept over lanes. + MEASURED in `entries/2026-10-23-d-tga-5-squash-gate-preregistration.md`: + landing the squash equals landing the finals, and the delta stays N + cells while the history grows k·N. Update count is activity, not + insight, so the target choice is only a tie-free rule. Correctness comes + from the gate. +2. **The determinism falsifier** (01G22yT6). The receipt replaces the + history only if every lane is deterministic given its seeds. Inject one + nondeterministic read (an outside read, thread timing) into the D-TGB-4 + replay test. The replay must refuse, not reproduce different writes + silently. +3. **Promotion at squash time.** CE64 bits 59..63 advance (correlation → + causality, MUL-calibrated rather than overconfident) only when the + squash is contradiction-free and blame shows independent lanes + (EXO-138's stamp condition). +4. **Compiled thought.** An egglog / eggcc certificate replaces the order + list. Lane 0 then stores the delta plus a seal that points at the + certificate, and a certified thought is reusable by reference. + +**Next probe:** rung 2, which is cheapest and guards the whole storage +argument. **Kill:** a lane that is deterministic given its seeds cannot be +defined for the planned writers (outside reads are essential). In that case +receipts cannot replace deltas, and the arithmetic above stands against the +design. + +**Fruit:** High-signal +**Status:** Open. + ## 2026-10-23 — One replay that checks proof, receipt and commit witness together `[P1 @thought-struct-scribe @truth-architect domain:thought-git D-TGB-7 D-RFT-5 D-DRMC]` diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 321efd45b..067bebd21 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -385,7 +385,7 @@ 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 | Queued | blame returns original sources after slot reuse | +| **D-TGA-5** | squash_into (partial squash) and blame | In PR (lab precursor: `crates/thought-git-probe/tests/squash_gate.rs`, `entries/2026-10-23-d-tga-5-squash-gate-preregistration.md`; most-updated target, contradiction/divergence gate, blame over lanes, 5 disables red) | blame returns original sources after slot reuse (slot reuse not yet covered) | | **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-tga-5-squash-gate-preregistration.md b/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md index 6c69ff837..6f2432aad 100644 --- a/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md +++ b/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md @@ -1,7 +1,7 @@ # 2026-10-23: D-TGA-5 lab precursor — squash the chain of origin into the most-updated lane, gated on contradiction (pre-registration) -**Status:** PRE-REGISTERED. Everything above the line was fixed before any -probe code was written. Results go below it. +**Status:** MEASURED, all seven predictions hold. Everything above the line was +fixed before any probe code was written. The results are below it. **Source:** an operator direction (provenance, not validation): the first squash gate is "which thought lane was updated most". That lane's chain of @@ -86,3 +86,56 @@ refuses P4's inputs, which means it fires on everything. reported. --- + +## Results (`cd crates/thought-git-probe && cargo test --test squash_gate`) + +9 tests pass: P1–P7, plus a seal test and a check against the oracle's own +divergence record. All 15 + 10 + 7 + 9 tests in the crate pass. clippy +`-D warnings` and fmt are clean. + +| prediction | result | +|---|---| +| P1 | the squash lands to the same `Version` as the final states, on every one of the 48 fixture cells | +| P2 | `Divergence { cell (5,2), offers [(7, lane 4), (8, lane 9)] }`; on the same input `oracle::squash` keeps 8 silently | +| P3 | `Contradiction { cell (1,0), given 101, offered 999, lane 5 }` | +| P4 | accepted; the input has 3 rewrites of one cell in one lane plus one cell two lanes agree on | +| P5 | ops per lane `(3,2) (7,4) (12,6)`, target 12; a tie goes to the lower id (11 over 20) | +| P6 | blame equals the independent reference; the shared cell carries bits 3 and 7 | +| P7 | see the table below | + +P7, with N = 8: + +| k | history writes | delta cells | order entries | +|---|---|---|---| +| 1 | 8 | 8 | 1 | +| 2 | 16 | 8 | 2 | +| 4 | 32 | 8 | 4 | +| 8 | 64 | 8 | 8 | +| 16 | 128 | 8 | 16 | +| 32 | 256 | 8 | 32 | +| 64 | 512 | 8 | 64 | + +Every anchor was asserted before each disable, and the file was restored +after each one. Every disable turned its test red: + +| disable | tests that went red | +|---|---| +| D1 | P2, plus the oracle cross-check | +| D2 | P3 | +| D3 | P4, plus P1, P5, P6, P7 and the seal test (all of them rewrite in a lane) | +| D4 | P5 | +| D5 | P6 | + +**Bearing on EXO-138.** Blame survives the squash as one `u64` over lanes, +the same shape as P-E2's stamp. The lane read can therefore serve as the +stamp at squash time, provided this bitset is kept when the squash lands. + +**Bearing on EXO-132 (lumpability).** Squash is a quotient: a chain of +operations collapses to one delta. P1 tests that quotient for one reader, +landing on the next version, and it holds. It does not test a reader of an +intermediate state (a mid-chain read), and by design the squash cannot +answer one. The full condition, raised by 01G22yT6: every later read, +including the 59..63 promotion, gets the same answer from the squash as +from the chain. That is a hypothesis, not tested here. + +Closeout: `STATUS: measured | OUTCOME: the most-updated lane absorbs the chain of origin under a contradiction/divergence gate; landing the squash equals landing the finals; blame survives; the stored delta stays N while the history grows k·N | OPEN: slot reuse (D-TGA-5's own falsifier); squash against a non-empty prior version; the order list still grows with thought count; CE64 59..63 promotion and certificates (IDEAS)` diff --git a/crates/thought-git-probe/tests/squash_gate.rs b/crates/thought-git-probe/tests/squash_gate.rs index be455bddc..0fe501a4c 100644 --- a/crates/thought-git-probe/tests/squash_gate.rs +++ b/crates/thought-git-probe/tests/squash_gate.rs @@ -163,7 +163,10 @@ fn clean_lanes() -> Vec { vec![ Lane::new( 3, - vec![commit(1, vec![(cell(4, 1), 41)]), commit(2, vec![(cell(6, 2), 62)])], + vec![ + commit(1, vec![(cell(4, 1), 41)]), + commit(2, vec![(cell(6, 2), 62)]), + ], ), Lane::new( 7, @@ -176,8 +179,14 @@ fn clean_lanes() -> Vec { Lane::new( 12, vec![ - commit(6, vec![(cell(8, 1), 81), (cell(8, 2), 82), (cell(0, 0), 100)]), - commit(7, vec![(cell(9, 1), 91), (cell(9, 2), 92), (cell(10, 1), 101)]), + commit( + 6, + vec![(cell(8, 1), 81), (cell(8, 2), 82), (cell(0, 0), 100)], + ), + commit( + 7, + vec![(cell(9, 1), 91), (cell(9, 2), 92), (cell(10, 1), 101)], + ), ], ), ] @@ -199,14 +208,26 @@ fn p1_landing_the_squash_equals_landing_every_final_state() { let finals: Vec = lanes .iter() - .map(|l| commit(1000 + u32::from(l.id), l.final_state().into_iter().collect())) + .map(|l| { + commit( + 1000 + u32::from(l.id), + l.final_state().into_iter().collect(), + ) + }) .collect(); let via_finals = next_version(&g, &main_version(), &finals); let via_squash = next_version(&g, &main_version(), &[s.as_thought(999)]); - assert_eq!(via_squash, via_finals, "squash differs from landing the finals"); + assert_eq!( + via_squash, via_finals, + "squash differs from landing the finals" + ); for c in probe_cells() { - assert_eq!(via_squash.read(&g, c), via_finals.read(&g, c), "read at {c:?}"); + assert_eq!( + via_squash.read(&g, c), + via_finals.read(&g, c), + "read at {c:?}" + ); } // Anti-vacuity: the comparison covers a rewritten cell and a shared cell. assert_eq!(via_squash.read(&g, cell(5, 1)), Some(52)); @@ -310,7 +331,11 @@ fn p6_blame_names_every_lane_that_wrote_a_cell() { (1 << 3) | (1 << 7), "a cell two lanes agreed on keeps both lanes" ); - assert_eq!(s.blame[&cell(0, 0)], 1 << 12, "agreement with a given is still blamed"); + assert_eq!( + s.blame[&cell(0, 0)], + 1 << 12, + "agreement with a given is still blamed" + ); } /// P7. The stored delta does not grow with the history. From 8ec6018ba68c48fbef5050345a11164a0b06b602 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 09:26:05 +0000 Subject: [PATCH 4/8] board: D-TGA-5 entry names its lumpability scope (deterministic congruence, not stochastic) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .../entries/2026-10-23-d-tga-5-squash-gate-preregistration.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md b/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md index 6f2432aad..03222ef52 100644 --- a/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md +++ b/.claude/board/entries/2026-10-23-d-tga-5-squash-gate-preregistration.md @@ -137,5 +137,9 @@ intermediate state (a mid-chain read), and by design the squash cannot answer one. The full condition, raised by 01G22yT6: every later read, including the 59..63 promotion, gets the same answer from the squash as from the chain. That is a hypothesis, not tested here. +This probe is deterministic, so P1 tests deterministic congruence (the +squashed state is independent of the chain that produced it). It does not +test strong stochastic lumpability. That distinction comes from GPT /08 on +EXO-50, which 019fbZ92 adopted in /011 item 4. Closeout: `STATUS: measured | OUTCOME: the most-updated lane absorbs the chain of origin under a contradiction/divergence gate; landing the squash equals landing the finals; blame survives; the stored delta stays N while the history grows k·N | OPEN: slot reuse (D-TGA-5's own falsifier); squash against a non-empty prior version; the order list still grows with thought count; CE64 59..63 promotion and certificates (IDEAS)` From e709bd3142d52c23c4229d29eda58b86ff8994f9 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 09:30:16 +0000 Subject: [PATCH 5/8] =?UTF-8?q?board:=20ground=20the=20certificate=20idea?= =?UTF-8?q?=20in=20Bittracher=20&=20Sch=C3=BCtte=202021=20(aggregation=20o?= =?UTF-8?q?f=20undersampled=20Markov=20chains)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lumpable + deflatable => rank R, P = Pi P_hat Lambda; aggregates from J sampled columns with J depending only on R and p; P_hat recovered with L1 error <= 4 eps, independent of N. Mapped to thought-git as [H] with four named falsifiers (non-homogeneity, non-uniform lane draws, deflatability, SVD only cold). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .claude/board/IDEAS.md | 54 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/.claude/board/IDEAS.md b/.claude/board/IDEAS.md index e7631da65..1bcf5b2c0 100644 --- a/.claude/board/IDEAS.md +++ b/.claude/board/IDEAS.md @@ -133,6 +133,60 @@ die at squash; only the squashed delta, receipts and seals reach disk. list. Lane 0 then stores the delta plus a seal that points at the certificate, and a certified thought is reusable by reference. +**Outside grounding: the accumulation as a large Markov chain** (operator, +2026-10-23). Source: Bittracher & Schütte, "A probabilistic algorithm for +aggregating vastly undersampled large Markov chains", *Physica D* 416 +(2021) 132799, +https://publications.imp.fu-berlin.de/2614/1/1-s2.0-S016727891930764X-main.pdf. +The grades are per claim. + +- **[G] within the paper's assumptions (Def. 2.1, Lemma 2.3).** + - *Lumpable*: the probability of moving into an aggregate depends only on + the starting state's aggregate. + - *Deflatable*: within an aggregate, the end state is drawn independently + of where the chain came from. + - A chain that is both is *aggregatable*. Its N×N matrix then has exactly + R distinct columns, so it has rank R, and it equals + `P = Π · P̂ · Λ`. +- **[G] (Alg. 3.1, Eq. 18).** + - Sample J columns, take an SVD and read the aggregates off the sign + pattern of the leading R left singular vectors (spectral clustering, + PCCA+ or SEBA). + - J depends only on R and the confidence p, never on N. With equal-sized + aggregates, recomputed here: R = 8 needs J = 51 for p = 0.99, R = 10 + needs J = 66, and R = 16 needs J = 115. +- **[G] (Prop. 3.9, Thm. 2.10).** + - The reduced matrix is recovered from the sampled columns alone: + `P̂ = Λ · P_K · Λᵀ_K · K⁻¹`. + - For an ε-almost aggregatable P, the L1 error is ≤ 4ε, also independent + of N. +- **[H] mapping to thought-git.** + - The 64 × 10^6 operations are the trajectory of one large chain over + cell states. Each lane's run is an expensive sample from its starting + state. + - A knowledge-preserving squash is an aggregation. Lane 0 would store the + partition Ω, the R×R matrix P̂ and the in-aggregate distributions π: the + certificate is P̂, not the operations. + - With the 63 thought lanes as J = 63 column samples, recomputed with + Eq. 18: R ≤ 10 aggregates are recovered with p ≥ 0.987, R = 12 with + 0.951, and R = 16 with only 0.758. + - The 4ε bound gives the squash gate a quantitative tolerance where it now + has a yes/no refusal. +- **[H] where the mapping can break.** Each item is a falsifier, not an + assumption. + 1. The paper's chain is time-homogeneous. Thought lanes are not, and the + aggregated process is in general non-homogeneous (paper §2). + 2. Lanes are chosen thoughts, not uniform independent column draws, so + Eq. 18's p does not hold for them as written. + 3. Deflatability is a strong extra condition, and nothing yet says + thought transitions satisfy it. + 4. SVD / PCCA+ is a floating-point clustering step. It belongs only on the + cold, out-of-fold path (CLAUDE.md, the no-ms scoped exception), never + per query. +- **Ties.** This is the stochastic form of EXO-132's lumpability, the + distinction GPT /08 asked for: almost-lumpability in L1, not deterministic + congruence. + **Next probe:** rung 2, which is cheapest and guards the whole storage argument. **Kill:** a lane that is deterministic given its seeds cannot be defined for the planned writers (outside reads are essential). In that case From 1f99aaaa529476f779ec4bce4e53114889c72196 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 09:43:18 +0000 Subject: [PATCH 6/8] thought-git-probe: squash folds only committed writes (P8) Lane::final_state, ops and blame folded every write whatever the thought's Outcome, while next_version lands only Commit. Every fixture used Commit, so no test saw it. P8 lands a lane with Prune / Veto / Plan writes one thought per version and compares every read against the squash: it was red before this change (Prune write (5,1)=51 squashed), green after. Pruned and vetoed thoughts stay in order and the seal as history. Found by the falsifier co-architect of the 2026-10-23 coresearch on thought-git as a Markov chain. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- crates/thought-git-probe/tests/squash_gate.rs | 56 +++++++++++++++++-- 1 file changed, 51 insertions(+), 5 deletions(-) diff --git a/crates/thought-git-probe/tests/squash_gate.rs b/crates/thought-git-probe/tests/squash_gate.rs index 0fe501a4c..3e385bd4d 100644 --- a/crates/thought-git-probe/tests/squash_gate.rs +++ b/crates/thought-git-probe/tests/squash_gate.rs @@ -26,15 +26,21 @@ impl Lane { Self { id, chain } } - /// Total writes in the chain. + /// The thoughts whose writes land: only `Outcome::Commit`, as in + /// `next_version`. Plan, Prune and Veto stay in the history only. + fn landed(&self) -> impl Iterator { + self.chain.iter().filter(|t| t.outcome == Outcome::Commit) + } + + /// Total landed writes in the chain. fn ops(&self) -> usize { - self.chain.iter().map(|t| t.writes.len()).sum() + self.landed().map(|t| t.writes.len()).sum() } - /// The chain folded in order: later writes replace earlier ones. + /// The landed chain folded in order: later writes replace earlier ones. fn final_state(&self) -> BTreeMap { let mut f = BTreeMap::new(); - for t in &self.chain { + for t in self.landed() { for &(c, v) in &t.writes { f.insert(c, v); } @@ -136,7 +142,9 @@ fn squash_gate(g: &Givens, lanes: &[Lane]) -> Result { fnv1a(&mut seal, u64::from(l.id)); fnv1a(&mut seal, u64::from(t.id)); for &(c, v) in &t.writes { - *blame.entry(c).or_default() |= 1u64 << l.id; + if t.outcome == Outcome::Commit { + *blame.entry(c).or_default() |= 1u64 << l.id; + } fnv1a(&mut seal, u64::from(c.row)); fnv1a(&mut seal, u64::from(c.lane)); fnv1a(&mut seal, v); @@ -399,3 +407,41 @@ fn a_refused_squash_is_a_divergence_the_oracle_also_records() { assert_eq!(v.divergences[0].cell, cell(5, 2)); assert!(squash_gate(&g, &lanes).is_err()); } + +/// P8. Only committed writes are squashed, as only committed writes land. +/// The chain is landed one thought per version with `next_version`, which +/// drops Plan, Prune and Veto; the squash must read the same everywhere. +/// The pruned and vetoed thoughts stay in `order` and the seal: they are +/// history, not state. Disable D6 (fold every write in `final_state`) turns +/// this red. +#[test] +fn p8_a_pruned_or_vetoed_write_is_not_squashed() { + let g = givens(); + let lanes = vec![Lane::new( + 3, + vec![ + commit(1, vec![(cell(4, 1), 41)]), + Thought::new(2, vec![(cell(5, 1), 51)], Outcome::Prune), + Thought::new(3, vec![(cell(4, 1), 99)], Outcome::Veto), + Thought::new(4, vec![(cell(6, 1), 61)], Outcome::Plan), + commit(5, vec![(cell(7, 2), 72)]), + ], + )]; + let s = squash_gate(&g, &lanes).expect("one lane squashes"); + + let mut chain = main_version(); + for t in &lanes[0].chain { + chain = next_version(&g, &chain, std::slice::from_ref(t)); + } + let via_squash = next_version(&g, &main_version(), &[s.as_thought(999)]); + for c in probe_cells() { + assert_eq!(via_squash.read(&g, c), chain.read(&g, c), "read at {c:?}"); + } + // Anti-vacuity: the dropped writes really were offered, and the kept ones land. + assert_eq!(via_squash.read(&g, cell(4, 1)), Some(41)); + assert_eq!(via_squash.read(&g, cell(5, 1)), None); + assert_eq!(via_squash.read(&g, cell(6, 1)), None); + assert_eq!(via_squash.read(&g, cell(7, 2)), Some(72)); + // History keeps every thought, landed or not. + assert_eq!(s.order.len(), 5); +} From 2c15792252cedca30dd0d487c65f8fccb2ad375a Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 09:44:45 +0000 Subject: [PATCH 7/8] board: coresearch map, thought-git accumulation as a large Markov chain Five scouts, crosswalk of 16 ideas, three co-architects. The papers' main results need a restart oracle, homogeneity and independent lanes; none hold (transducer, transient DAG, lanes measured dependent). What survives: min/max L/U bounds, partition-refinement congruence, the certificate/model split. One defect found and fixed in the squash gate (P8). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- ...026-10-23-coresearch-thought-git-markov.md | 78 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 2 files changed, 80 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..4ad4809f0 --- /dev/null +++ b/.claude/board/entries/2026-10-23-coresearch-thought-git-markov.md @@ -0,0 +1,78 @@ +# Coresearch 2026-10-23: thought-git accumulation as a large Markov chain + +**Status:** exploration map. Nothing is adopted; the operator chooses. +**Question (operator):** "Consider that giant thought-git accumulation as a large Markov chain." +Sources: Bittracher & Schütte, *Physica D* 416 (2021) 132799, read in full; +Askarian, Xu & Faragó, *Algorithms* 9(3):50 (2016), arXiv 1809.06564, read in full. + +## Frame (what the scouts established) + +- **F1.** A version is a deterministic function of the givens, the prior + version and the landing thought set (`oracle.rs:46-108`, verified in code). + Thought-git is therefore a transducer, or a Markov decision process; it is a + Markov chain only once the policy that chooses thoughts is fixed. +- **F2.** No ruling grants the Markov property to lane accumulation. + E-SUBSTRATE-1 covers bundles and E-MARKOV-TEMPORAL-STREAM-1 covers stream + order. Last-writer replace is neither, and the seal is an order-dependent + fold (`seal-vs-temporal-ordering-information.md`). +- **F3.** Lanes are measured not independent: they share the manuscript, the + tokenizer and the model (`ISSUES.md:3852`). +- **F4.** No code in `crates/` estimates transition probabilities, tests + lumpability or bounds an aggregation error. The search space was a closed + `git grep`; ndarray/hpc was not searched. +- **F5.** Two earlier rejections apply here. + - #1703: a replay capsule is not proof authority, and population evidence + only nominates. + - TORQUE T-2026-10-23-1 (killed): a learned PaletteLut aggregation did not + compose. + +## Where the papers stop applying + +- **B&S Algorithm 3.1.** It needs a restart from any state to draw a column. + A trajectory log cannot do that. Trajectory-only estimation needs about + p·r samples (Zhu et al., arXiv 1907.00113, Thm 3, section-read), so "J + independent of N" does not transfer [S]. It also requires homogeneity + (fails per F1) and independent samples (fail per F3). +- **AXF Theorem 2.** It needs an irreducible, aperiodic chain. Accumulation + over versions is a transient DAG with no recurrence, so the theorem does + not apply. +- **What survives** without the Markov property and without independence: + - min/max L/U bounds over counts (AXF Def. 3); + - deterministic congruence found by partition refinement; + - the type split: certificate (replay + seal) versus model. + +## Exploration map + +| idea | verdict | why / probe | +|---|---|---| +| Squash folds only committed writes | **ADOPT-NOW, done** | Found by the falsifier: `Lane::final_state` folded Prune/Veto/Plan writes. Fixed in #1736 with P8 (red before the fix, green after; disable D6 turns only P8 red). | +| D: squash equals chain for every later read | PROBE (S) | Fixtures: (b) contradiction then rewrite; (c) intermediate divergence then agreement; (d) the same value 3× vs 1×. Predicted: the intermediate contradiction and divergence records, and the multiplicity, are lost. Decide whether that loss is acceptable before building a certificate on the squash. Silent twin: `clean_lanes`. | +| D-59..63: the squash preserves the epistemic promotion | PROBE (S), blocked | The promotion reader must be pinned first. Blame is a lane bitmask, not a count, so a multiplicity-reading promotion breaks. | +| I3: counted ε-spread L/U gate | PROBE (M) | Bridge: R2 is ε = 0 with a point mass per lane. Count lanes per (cell, value class) from the blame bitmask; refuse when U−L > ε by integer cross-multiplication. With ε = 0 it must reproduce R2 (the p2/p4 tests). It is a BOUND only when the counts are exhaustive; otherwise it is an empirical interval, a gate annotation and never proof authority. | +| I7: coarsest congruence by partition refinement | PROBE (S–M) | Integer, cold. It supplies I3's blocks. Kill if the reduction is below 2× on real traces. | +| F1: is the process Markov at all, over a chosen state space | PROBE (M), needs real traces | First the revisit rate: below 1% means untestable on that state space, so coarsen. Then an order-1 vs order-2 contingency test against a Jirak band; kill if more than 10% of states differ. A synthetic policy decides the answer in advance, so it does not count. | +| F3: lane independence after conditioning on shared inputs | PROBE (M), needs real traces | Conditional mutual information against a time-shuffled null. Precondition for any cross-lane convergence gate. | +| I12/I13: lossless op-log encoding, tags plus cleanup | PROBE (S) | Use Lance's own column encodings and version tags; no parallel store. This answers the terabyte concern without any Markov assumption. | +| I2 P = Π P̂ Λ; I5 defect; I6 interval propagation; I10 Chapman-Kolmogorov; I11 VAMP; I16 MarkovTripletState | PARK | Each needs F1 to pass (homogeneity) or the dormant VAMPE+Jirak track. All are cold-path and report-only. | +| I1 J-column SVD; I4 AXF convergence; I14 Nova IVC | SKIP | I1: no restart oracle and dependent lanes. I4: transient DAG. I14: licence unknown, far outside the ns law. | +| I8 causal state; I9 certificate vs model | ALREADY-HAVE | `final_state()` is the causal state of a deterministic lane; replay plus seal is the certificate. | + +## Head selection (operator follow-up) + +Recency is not the criterion. The gate-grade parts are subsumption (R1/R2) +and the exact L/U spread. The others are not: + +- cross-lane convergence (R̂) presumes independent lanes, which F3 refutes; +- stability (ρ) and predictive sufficiency are cold-path and report-only. + +## Not searched + +- ndarray/hpc (clam_compress, cam_pq); +- GOLDSTAUB, identity-temporal-evidence-primer, holographic-temporal-access-projection; +- the IDEAS joint-replay row; +- Buchholz and Franceschinis-Muntz bounding-aggregation papers (not located); +- bisimulation metrics (abstract only). + +## Closeout + +`coresearch | STATUS: open | OUTCOME: one defect fixed in #1736 (P8); map with 7 probes | OPEN: real lane traces needed for F1/F3/I3/I7; promotion reader unpinned` diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index bcda1dcf9..067eb8cbe 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 | `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 | `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 6ad966d1ed6d4a1a4de1b7968fe5c6c5dc0f29c4 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 10:05:34 +0000 Subject: [PATCH 8/8] board: withdraw the probabilistic framing of thought-git (category error) The substrate is deterministic; a probabilistic model is a counterfactual that the egglog/eggcc compiler must certify. The Markov/aggregation papers describe at most the search, never the certificate. Head = the thought whose compiled proof is admitted; the children's folds are its compilation material. Blocker named: no DR64 certified compiler (NoCertifiedCompiler). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .claude/board/IDEAS.md | 6 +++ ...026-10-23-coresearch-thought-git-markov.md | 38 ++++++++++++++++++- 2 files changed, 43 insertions(+), 1 deletion(-) diff --git a/.claude/board/IDEAS.md b/.claude/board/IDEAS.md index 1bcf5b2c0..9640dc320 100644 --- a/.claude/board/IDEAS.md +++ b/.claude/board/IDEAS.md @@ -186,6 +186,12 @@ The grades are per claim. - **Ties.** This is the stochastic form of EXO-132's lumpability, the distinction GPT /08 asked for: almost-lumpability in L1, not deterministic congruence. +- ⊘ **Superseded 2026-10-23 (same day).** DECISION (operator): the substrate + is not probabilistic; a probabilistic model is a counterfactual that the + egglog/eggcc compiler must certify. The certificate is a checked proof, not + P̂, and the 64 × 10^6 folds are compilation material, not samples. The block + above is kept as the record of a withdrawn framing; see + `entries/2026-10-23-coresearch-thought-git-markov.md` § Correction. **Next probe:** rung 2, which is cheapest and guards the whole storage argument. **Kill:** a lane that is deterministic given its seeds cannot be 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 4ad4809f0..fe7e4303a 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 @@ -73,6 +73,42 @@ and the exact L/U spread. The others are not: - Buchholz and Franceschinis-Muntz bounding-aggregation papers (not located); - bisimulation metrics (abstract only). +## ⊘ Correction 2026-10-23: the probabilistic premise was a category error + +DECISION (operator, 2026-10-23): the substrate is not probabilistic. SPO-FC +being probabilistic today is legacy. Every probabilistic model counts as a +**counterfactual** and must be certified by the egglog / eggcc reasoning +compiler before anything rests on it. The 64 lanes × ~10^6 folds run per +second are the **material** a thought is compiled from, until it is a proof +that later operations can call by reference. They are not a population to be +aggregated statistically. +SCOPE: this map and the IDEAS row "A certificate replaces the deltas" (its +Markov block). BASIS: the operator's statement; consistent with F1 (versions +are deterministic), #1703 (population evidence only nominates) and +`dr-math-binding-probe` (`admit_recipe` ends in `NoCertifiedCompiler`). +REVISIT WHEN: never on statistical grounds. + +What this changes in the map: +- The Bittracher/Schütte and Askarian papers describe at most the **search + over counterfactuals**, never the admission and never the certificate. + All their rows (I1–I6, I10, I11) drop to PARK as counterfactual-layer + descriptions. The certificate/model split (I9) holds and is sharpened: the + certificate is a checked egglog proof, not a replay witness and not P̂. +- The premise gate failed. Phase 0 split certificate from aggregation but + never asked whether the substrate is stochastic at all. F1 (versions are + deterministic) already said it is not; the brief should have stopped there. +- Head selection: the head is the thought whose compiled proof is admitted. + The children's folds are the search trace. After admission they are + discarded, except the seal and the refuted branches the proof cites. +- What actually blocks this: no certificate exists for DR64 (`dr-math-binding-probe`, + `NoCertifiedCompiler`). The open items there are a typed relational statement + language, egglog laws with checked proofs, and a lowering check. The candidate + first law is associativity of Boolean relation composition. `crates/egglog-r2il-probe` + holds the cold compile path; `.arxiv/2026-10_eggcc_effect_safe_extraction_statewalk_r2il_map.md` + holds the effect-safe extraction lesson. +- Still valid: the P8 fix (only committed writes squash) and probe D + (squash = chain for every later read). Both are deterministic. + ## Closeout -`coresearch | STATUS: open | OUTCOME: one defect fixed in #1736 (P8); map with 7 probes | OPEN: real lane traces needed for F1/F3/I3/I7; promotion reader unpinned` +`coresearch | STATUS: open | OUTCOME: one defect fixed in #1736 (P8); probabilistic premise withdrawn (category error) | OPEN: DR64 certified compiler (typed statement language + checked egglog laws + lowering check); probe D; promotion reader unpinned`