board: /coresearch map — thought-git accumulation as a large Markov chain

.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-cc2.md` (CC2's map; session 01Vnc's parallel map on the same question is `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<f32>` 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.