superseded: #1696 is the Math Foundry main integration PR

crates/egglog-r2il-probe/HERITAGE_STUDY.md

@@ -0,0 +1,50 @@
+# Stage E: mathematical heritage / 27-atom falsifier (lab only)
+
+**Dependency chain:** merged [#1690](https://github.com/AdaWorldAPI/lance-graph/pull/1690) (E1 compiler) → draft Stage C proof capsule (#1693) → draft Stage D catalogue (#1694) → this draft.
+
+## What this implements
+
+The Rust `heritage` module distinguishes:
+1. **Source lead**: an author/work/edition candidate. NOT a reviewed facsimile, historical influence proof or mathematical certification.
+2. **Normalized mathematical statement**: a modern reconstruction with its assumptions, not necessarily the author's original proof.
+3. **Checked computational artifact**: currently only the synthetic E1 exact-integer substitution, compiled by egglog and replayed through R2IL with independent i128 oracle.
+
+The Leibniz 1684 product-rule and Euler-identity entries are **uncertified source candidates**. Neither is executable, because the current E1 language has only `Num/Var/Def/Mul` and does not express differentiation, complex exponentials or the necessary side conditions. A test refuses both, by design.
+
+## 27-atom hypothesis, not a discovery
+
+Candidate vocabulary: six term constructors, eight algebra operators, seven relational operators, six derivation constructs. These are *research-level semantic categories*, not R2IL opcodes or claims that 27 operations suffice for all mathematical domains. No atom is considered "covered" unless an independently certified compiled procedure exercises it. Today the synthetic E1 program witnesses just `Const, Var, Multiply`.
+
+Measure on a future licensed corpus:
+- Historical coverage: reviewed editions and unambiguous citations
+- Formalization coverage: statements expressed with domain/assumption witnesses
+- Proof coverage: mechanically checked lemmas, including independent proof-checker identity
+- Lowering coverage: lawful mappings to extant R2IL opcodes/folds
+- Minimum description length: vocabulary bytes + compiled corpus bytes; nonsharing control
+- Replay cost, proof bytes, binding costs, cache hit rates and provenance retention
+
+**A shorter encoding is not evidence of semantic preservation.** The optimizer must refuse a proposed common template that changes SQL NULL/UNKNOWN, Set/Bag, numeric overflow, effects, source identity or historical attribution.
+
+## Thought-Git learning × audit integration (future gate)
+
+Do not duplicate Thought-Git's store or insert proof events into the nanosecond hot loop. Its existing D-TGB-4 receipts and landed commit witnesses are distinct from egglog proof DAGs. The future link is a reference-only citation from a versioned derivation or historical study row to:
+- certified law identity and assumptions
+- compiled procedure identity and checker version
+- source edition/provenance and any uncertainty
+- runtime binding witness (separately invalidatable)
+- promotion/demotion decision, counterexamples and cost samples
+
+A replay recipe should be sufficient to recompute the outcome if the source snapshot/operands, codebook and checker are available. A hash alone is not a replay. An unsigned witness fold is not a cryptographic proof. Rubicon authorization and real LanceCycleWriter integration are out of scope.
+
+## Next falsifiable stages (not shipped here)
+
+1. Formalize the Leibniz product rule against an independent differentiation theorem checker. Preserve exact domain conditions, such as differentiability of both functions.
+2. Add an explicit mapping from the formal derivative term graph into the low-code hypothesis, measuring needed *new* atoms instead of forcing a 27-atom success.
+3. Compare Leibniz- and Newton-era equivalent formulas only after historical source reviews; equivalence does **not** establish intellectual influence.
+4. E2: 256 templates × 4,096 focus contexts = 1,048,576 applications. Compare cold certified catalogue vs existing relalg/CSE baseline, share/no-share controls and **total** execution cost. No demonstrated throughput claim yet.
+5. Add read-only Thought-Git proof/reference records and replay tests after EXO-98 owner coordination.
+
+## Verification
+
+`cd crates/egglog-r2il-probe && cargo test` (requires sibling OGAR and ndarray checkout).
+No runnable historical theorem is claimed. The three source/sample fixtures remain entirely outside production.

crates/egglog-r2il-probe/REVIEW_1690_1695.md

@@ -0,0 +1,88 @@
+# Review of #1690–#1695: preserve merged-stack provenance and complete the mathematical compiler seams
+
+**Review date:** 2026-10-22. **Scope:** current `main` compared to the exact GitHub PR metadata and the #1695 head branch; selected source-level inspection of `egglog-r2il-probe`, `perturbation-sim::outage_oracle`, Stage A/B board entries and `thought-git-probe::receipt`. This is **not** a successful local Cargo run (Rust toolchain unavailable in reviewer environment). Separate observed repository facts from research recommendations.
+
+## Critical integration finding and recovery
+
+GitHub marks [#1693](https://github.com/AdaWorldAPI/lance-graph/pull/1693), [#1694](https://github.com/AdaWorldAPI/lance-graph/pull/1694) and [#1695](https://github.com/AdaWorldAPI/lance-graph/pull/1695) as merged. But their targets differ:
+
+- #1693: `lab/math-foundry-1-proof-replay-20261022` -> **main**.
+- #1694: `lab/math-foundry-2-certified-catalogue-20261022` -> **#1693 feature branch**.
+- #1695: `lab/math-foundry-3-heritage-study-20261022` -> **#1694 feature branch**.
+
+As inspected, **main had `artifact.rs` and `tests/replay.rs`, but lacked `catalogue.rs`, `heritage.rs`, both associated integration tests, `HERITAGE_STUDY.md` and corresponding `pub mod` declarations**. Merely reading merged PR status substantially overstates deployed integration.
+
+**Recovery change in this PR:** copy the five missing files byte-identically from the #1695 head and expose both modules in `lib.rs`. This branch deliberately leaves their logic unchanged. It does **not** claim to have executed the recovered tests or promoted them to production. Before merging, compare file blob SHAs against original #1695 and run **the excluded probe's own tests**, not just root CI.
+
+**Regression requirement for stacked PRs:** Require that *all expected file paths appear under the intended final integration branch* before marking a staged program delivered. Mark stacked child PR merge-to-feature as `integrated_into_parent`, not as `shipped_on_main`. Revalidate after parent merge. The ordinary repository build/test jobs do not establish coverage for the separate `[workspace]` `egglog-r2il-probe`.
+
+## Review by PR and missing connections
+
+| PR | Directly established | Open, not established |
+|---|---|---|
+| #1690 | MORK `query_multi` oracle behind plain Lance value boundary; egglog E1 exact substitution, bounded scheduling, checked egglog proof, R2IL scalar `INT_MULT`, independent i128 value comparison. | E2–E5, production source bindings, general optimizer, memory/sharing study and cold compile economics; MORK callback/derivation count is not SQL BAG semantics without explicit de-dup policy. |
+| #1691 | Standalone K3 site-service scalar oracle with distinct grid, backup and telecom signals; source-generation and stable focus guard. | No measured site↔bus mapping, independent grid/telecom telemetry, graph-risk-to-site-power inference, egglog/R2IL extraction or observed-outage validation. `grid_status` in legacy A10H data is a synthetic label derivative, not a fresh observation. |
+| #1692 | Three source-attributed Tatlock `.arxiv` research notes, **documentation only**. | Relational e-matching, Ruler/Enumo, babble anti-unification, Small Proofs, Chassis or Lakeroad are not integrated just because they are studied. |
+| #1693 | In-memory replay capsule, deterministic re-egglog `recheck`, proof/extraction/step-list consistency, no egglog on saved `execute`. | No durable certificate, independent proof checker, trusted artifact import, pinned egglog/compiler version or cryptographic identity. Proof text stability across compiler revisions is not guaranteed. |
+| #1694 | *Recovering via this PR*: in-memory semantic-keyed catalogue, caller-supplied binding/ABI witness, economic gate and baseline callback. | A four-input i128 sample check and caller-supplied nanosecond estimates are not universal theorem verification or measured break-even. No source-backed witness attestation; key omits explicitly named algorithm/law-set/version/source identity beyond the caller fields. |
+| #1695 | *Recovering via this PR*: synthetic E1 execution, uncertified Leibniz/Euler leads, 27 **candidate** atoms, descriptive meta-study. | 24/27 atoms are not compiled; historical source/authorship and theorem proof are independent evidentiary questions. No real Thought-Git reference, source edition pin, durable provenance, derivative/complex term grammar or replay from disk. |
+
+## P0: mathematical premise soundness before expanding beyond E1
+
+**Observed:** `Problem { premises: Vec<Eq> }` is public. `encode::setup` indiscriminately `union`s every equation, while `oracle::solve` builds a forward `BTreeMap` and silently skips subsequent definitions of the same `lhs`. Neither `ReplayCapsule::certify` nor `Catalogue::promote` currently validates duplicate/conflicting definitions, attempts to define the freely supplied target, or cycles in a generalized input graph.
+
+**Concrete counterexample to test (NOT claimed executed):**
+```text
+goal=z; target=c; premises=[ z=2*c, z=3*c ]; supplied c=7
+```
+These premises conflict for nonzero c. egglog considers both asserted equalities true; the i128 oracle may retain the first equation and ignore the second. A matching sample therefore need not establish that the full equation set is jointly valid for every runtime input. This is **not a flaw in egglog**: it is a missing caller contract for treating equations as universally valid definitions.
+
+**Minimal next code change, separate owned PR:** validate that `target_var` is a free parameter, each `lhs` has a unique definition, reachable definitions are acyclic and every dependency needed by the goal resolves to the target or refuses. Reject conflicts **before `union` or promotion**. Add adversarial tests for conflicting duplicate heads, two contradictory paths, `c=2c`, cycles, disconnected premises and benign duplicate equations. Independently check every equation against generated input assignments, including negative and boundary values, rather than trusting the first path. Only then consider reusable arbitrary equation DAGs. Keep #1693's valid E1 behavior unchanged.
+
+## P1: distinguish mathematical, compiled, binding and execution identities
+
+The following are different and must not be collapsed into one `SemanticKey` or one vague `certified` flag:
+
+1. **Math identity**: normalized statement + assumptions + typed domain (Exact / Checked / Wrapping / IEEE, Boolean set / SQL K3+validity / Bag+Distinct) + admitted law IDs and rule versions. A historical attribution is *not* a mathematical assumption.
+2. **Compiler identity**: extracted term, R2IL step list, lowering and target/ABI versions, cost objective, egglog engine/checker version, and optional proof DAG/checker receipt. A rendered proof string alone is not a durable independent proof.
+3. **Binding identity**: dataset and source snapshot(s), focus, source↔local codebook mapping, typed coordinate domain and attested generations. `BindingWitness { source_generation, scope, coordinate_generation }` is currently caller-supplied lab metadata. Two unrelated sources with the same numeric generation values still must not alias.
+4. **Execution identity**: actual inputs, BEFORE/AFTER or independent output oracle, error/refusal codes, physical reads and separate durable commit acknowledgment. `ReplayCapsule::execute` is **not** a write or a source-attested replay.
+5. **Historical identity**: edition/source locator, transcription normalization and uncertainty; can be reviewed independently from mathematical formalization or proof.
+
+Proposed reference-only join shape for EXO-98 / D-TGB-4 (no writer integration here):
+```text
+TheoremRef(math_id, source_edition?, assumptions, domain)
+  -> LawProofRef(proof_id, checker_version, typed_law_ids)
+  -> CompiledPatternRef(r2il_steps_digest, target_abi, compiler_revision)
+  -> BindingRef(dataset, snapshot, focus, coordinate_codebook, generations)
+  -> ReplayRef(inputs, result, comparison, error, proof_receipt)
+  -> CommitRef(optional, real coalesced cycle + durable store witness)
+```
+**Never** mistake an equality proof, a call-success result, an unsigned Fold receipt, or `CandidateDirty` for a durable acknowledged commit. Thought-Git's current `Receipt`, `BaseRef`, `ProgramId`, metadata seal and `CommitWitness` already express **different** lifecycle concepts. Link by immutable IDs/references and admission fences rather than putting egglog into Thought-Git's hot cycle.
+
+## P1: honest fallback and measured economics
+
+`Catalogue::promote` checks a caller-provided `CostEvidence` where `(baseline_ns-candidate_ns)*expected_reuse > compile_and_certify_ns`. This is a good *lab policy formula* but not self-attesting cost evidence. A false positive can be generated by invented inputs; even honest averages need variance and workload shape.
+
+**Measure independently**: cold egglog+proof, cold independent oracle/checker, catalogue lookup, binding/attestation, first execution, steady R2IL path, baseline path, runtime refusal/fallback, output materialization and retained proof bytes. Include instruction-cache and e-graph costs for high-width extraction. A cache hit with identical goal and coefficients but wrong source snapshot is a red failure, irrespective of the saved nanoseconds.
+
+**Required E2 sample**: 256 distinct rules × 4,096 pinned contexts (1,048,576 requested uses), plus deliberately *nonsharing* control. Compare direct relalg normalization/CSE and existing R2IL procedures first; optionally add relational e-matching, babble abstraction reuse and effect-safe extraction **only if those baselines show a real gap**. Quantify amortized net savings and refused/witness-invalidated work. Cold compile cannot be hidden by `CLAUDE.md`'s reporting-budget language.
+
+## P1/P2: complete the research connections without replacing the runtime
+
+- **#1690 ↔ #1692:** Ruler/Enumo propose typed rewrite candidates; relational e-matching searches for them; babble suggests template factoring; eggcc requires effect-aware extraction; Small Proofs motivates shared proof DAG; Chassis applies only in explicitly approximate real-number domains. All are **cold** / optional. None authorizes a foreign positional gather or new hot runner.
+- **#1691 ↔ #1690:** a pure K3 site equation could become a *new* bounded compilation fixture **after** source version, tower focus and independent power/telecom evidence are resolved; it cannot be evaluated as checked integer E1 or infer causality from historical synthetic labels.
+- **#1693 ↔ Thought-Git:** replayable proof equations are not replayable physical thought histories. Use distinct IDs for math proof, compiler recipe, source binding and actual sealed thought receipt; preserve D-TGB-4 ABA, provenance roots, multi-thought coalescing and two-write crash window.
+- **#1695 ↔ mathematical heritage:** freeze a licensed primary-source edition and transcribed statement; separately formalize Leibniz with derivative assumptions/quantifiers and Euler with complex exponential definitions; mechanical proof and modern compiled recipe are distinct again. E1 currently witnesses `Const, Var, Multiply` only.
+- **relalg/R2IL/Quack boundary:** `lance-graph-contract` is the admitted set-law owner (D-RA-2=A); relalg plans/lower; R2IL is the SIMD polyfill; Quack selects the physical procedure; `mask-risc::execute_into` is the hot executor. E1 is scalar-only, so it does not demonstrate 256-bit mask fusion or a population `SUM`. ADMISSION=B prohibits cross-table foreign-value-directed positional gathers during preparation.
+
+## Minimum practical gates before calling the full stage delivered
+
+1. **Restore to main:** verify this recovery PR contains all six recovery changes and the original #1695 test suites; run `cargo test --manifest-path crates/egglog-r2il-probe/Cargo.toml`, `cargo fmt --manifest-path crates/egglog-r2il-probe/Cargo.toml -- --check`, and isolated clippy with sibling OGAR/ndarray available. Root CI success does **not** substitute.
+2. **Premise validation:** contradictory duplicate/cycle cases fail; independent oracle checks *all* premises and full goal, not the first forward path.
+3. **Artifact portability:** serialization → fresh-process import → pinned checker and R2IL replay; reject tampered proof, compiler revision, law ID, input and binding.
+4. **Cache soundness:** stale dataset/scope/coordinate, same ordinal/different entity, Bag/Distinct and valid FALSE/NULL/K3 witnesses all fail closed or use trusted fallback.
+5. **Cost validity:** E2 measured with sharing/nonsharing controls and accounted cold+warm costs.
+6. **Historical honesty:** 27 atoms remain hypotheses and historical claims cannot be upgraded without reviewed source and independent formal theorem proof.
+
+**Owner boundaries:** this review/recovery does not modify `.claude/board/STATUS_BOARD.md` or EXO-50/EXO-98 owner fields; coordinating sessions should update those after the restored files are demonstrably present and tested on `main`. The Stage A gap-matrix claim that no LG crate depends on egglog is stale after Stage B, although its subsequent Stage B entry already documents the correction. Stage A should be retained as a historical snapshot, with a cross-link rather than silently rewritten as current state.