integrate(math-foundry): land #1694/#1695 catalogue and heritage stages on main

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/src/catalogue.rs

@@ -0,0 +1,201 @@
+//! Stage D (lab): pre-certified mathematical patterns with fallback.
+//!
+//! Egglog is invoked ONLY when a candidate is cold-certified/promoted.
+//! The lookup path is a BTreeMap + exact semantic/target/binding guard + an
+//! already-lowered R2IL scalar program. Every miss/refusal calls the existing
+//! caller-supplied trusted baseline. This is NOT a production cache, data
+//! attestation, benchmark framework, or background task scheduler.
+
+use std::collections::BTreeMap;
+
+use crate::artifact::{ReplayCapsule, ReplayRefusal};
+use crate::{LowerRefusal, Problem};
+
+/// Full source expression signature. Deliberately preserve premise order,
+/// coefficient, and variable names; no hashes or accidentally merged laws.
+#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
+pub struct SemanticKey {
+    goal: String,
+    target: String,
+    premises: Vec<(String, i64, String)>,
+}
+
+impl From<&Problem> for SemanticKey {
+    fn from(p: &Problem) -> Self {
+        Self {
+            goal: p.goal.to_owned(),
+            target: p.target_var.to_owned(),
+            premises: p.premises.iter()
+                .map(|e| (e.lhs.to_owned(), e.coeff, e.rhs.to_owned()))
+                .collect(),
+        }
+    }
+}
+
+/// Caller-supplied lab witness. A production owner must independently attest
+/// these values from the sealed source and coordinates before any cache use.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub struct BindingWitness {
+    pub source_generation: u64,
+    pub scope: u64,
+    pub coordinate_generation: u64,
+}
+
+/// Plan compatibility, independent of mathematical identity and bindings.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct TargetAbi {
+    pub revision: u32,
+    pub target: String,
+}
+
+/// All times are supplied from external measurements; none are inferred from
+/// AST size or fabricated by the catalogue.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub struct CostEvidence {
+    pub baseline_ns: u64,
+    pub candidate_ns: u64,
+    pub compile_and_certify_ns: u64,
+    pub expected_reuse: u64,
+}
+
+impl CostEvidence {
+    pub fn pays_for_itself(&self) -> bool {
+        self.candidate_ns < self.baseline_ns
+            && self.expected_reuse > 0
+            && u128::from(self.baseline_ns - self.candidate_ns)
+                * u128::from(self.expected_reuse)
+                > u128::from(self.compile_and_certify_ns)
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum PromotionRefusal {
+    Uncertified(ReplayRefusal),
+    NotAmortized,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum FallbackReason {
+    CacheMiss,
+    BindingChanged,
+    TargetChanged,
+    CompiledRefused,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum Route {
+    Certified,
+    Baseline(FallbackReason),
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Execution {
+    pub route: Route,
+    pub result: Result<i64, LowerRefusal>,
+}
+
+struct Entry {
+    capsule: ReplayCapsule,
+    binding: BindingWitness,
+    abi: TargetAbi,
+    _cost: CostEvidence,
+}
+
+/// In-memory lab catalogue; never loads an unverified disk blob.
+#[derive(Default)]
+pub struct Catalogue {
+    entries: BTreeMap<SemanticKey, Entry>,
+}
+
+impl Catalogue {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn len(&self) -> usize {
+        self.entries.len()
+    }
+
+    pub fn is_empty(&self) -> bool {
+        self.entries.is_empty()
+    }
+
+    /// Cold gate. A proof, replay, independent i128 oracle and supplied
+    /// break-even evidence are required before inserting executable steps.
+    /// This retains the existing Stage B exact-integer / E1-only restriction.
+    pub fn promote(
+        &mut self,
+        capsule: ReplayCapsule,
+        binding: BindingWitness,
+        abi: TargetAbi,
+        cost: CostEvidence,
+    ) -> Result<(), PromotionRefusal> {
+        capsule.recheck().map_err(PromotionRefusal::Uncertified)?;
+        for x in [0_i64, 1, -1, 7] {
+            capsule.replay(x).map_err(PromotionRefusal::Uncertified)?;
+        }
+        if !cost.pays_for_itself() {
+            return Err(PromotionRefusal::NotAmortized);
+        }
+        self.entries.insert(
+            SemanticKey::from(capsule.problem()),
+            Entry {
+                capsule,
+                binding,
+                abi,
+                _cost: cost,
+            },
+        );
+        Ok(())
+    }
+
+    /// Hot-compatible lookup and execution: neither egglog nor the i128
+    /// oracle runs here. Source/coordinate/target validation is fail-closed,
+    /// but caller-supplied witnesses are not source attestation.
+    ///
+    /// Any miss or compiled execution refusal invokes baseline unconditionally.
+    pub fn execute_or<F>(
+        &self,
+        problem: &Problem,
+        binding: BindingWitness,
+        abi: &TargetAbi,
+        x: i64,
+        baseline: F,
+    ) -> Execution
+    where
+        F: FnOnce(i64) -> Result<i64, LowerRefusal>,
+    {
+        let entry = match self.entries.get(&SemanticKey::from(problem)) {
+            Some(e) => e,
+            None => {
+                return Execution {
+                    route: Route::Baseline(FallbackReason::CacheMiss),
+                    result: baseline(x),
+                };
+            }
+        };
+        let refusal = if entry.binding != binding {
+            Some(FallbackReason::BindingChanged)
+        } else if &entry.abi != abi {
+            Some(FallbackReason::TargetChanged)
+        } else {
+            None
+        };
+        if let Some(reason) = refusal {
+            return Execution {
+                route: Route::Baseline(reason),
+                result: baseline(x),
+            };
+        }
+        match entry.capsule.execute(x) {
+            Ok(value) => Execution {
+                route: Route::Certified,
+                result: Ok(value),
+            },
+            Err(_) => Execution {
+                route: Route::Baseline(FallbackReason::CompiledRefused),
+                result: baseline(x),
+            },
+        }
+    }
+}