From 8b005f7ea5a717043d7df035f28f97e01c6ed04e Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 08:48:40 +0200 Subject: [PATCH 1/4] feat(math-foundry): separate historical source leads from certified math --- crates/egglog-r2il-probe/src/heritage.rs | 214 +++++++++++++++++++++++ 1 file changed, 214 insertions(+) create mode 100644 crates/egglog-r2il-probe/src/heritage.rs diff --git a/crates/egglog-r2il-probe/src/heritage.rs b/crates/egglog-r2il-probe/src/heritage.rs new file mode 100644 index 000000000..81bed9308 --- /dev/null +++ b/crates/egglog-r2il-probe/src/heritage.rs @@ -0,0 +1,214 @@ +//! Stage E (lab): mathematics heritage as explicitly labelled source claims, +//! not as automatically certified executable proofs. +//! +//! The first runnable entry is the SYNTHETIC #1690 E1 substitution theorem. +//! Historical examples are catalogue leads only. Leibniz's product rule and +//! Euler's identity require new higher-level term grammars, domain guards and +//! independent theorem checkers before they may become proof capsules. +//! +//! The 27 atoms are a falsifiable vocabulary hypothesis, NOT an admitted +//! universal mathematical basis and NOT 27 R2IL opcodes. + +use std::collections::BTreeSet; + +use crate::Step; +use crate::artifact::{ReplayCapsule, ReplayRefusal}; +use crate::e1_problem; + +/// Proposal for a cross-domain low-code vocabulary, NOT the R2IL ISA. +/// Grouped 6 terms + 8 algebra + 7 relation + 6 derivation = 27 candidates. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] +pub enum Atom27 { + Const, + Var, + Lambda, + Apply, + Let, + Tuple, + Add, + Neg, + Multiply, + Divide, + Power, + Equal, + Order, + If, + Select, + Project, + Join, + Union, + Distinct, + Group, + Aggregate, + Substitute, + Rewrite, + Differentiate, + Integrate, + Iterate, + Prove, +} + +pub const PROPOSED_ATOMS: [Atom27; 27] = [ + Atom27::Const, + Atom27::Var, + Atom27::Lambda, + Atom27::Apply, + Atom27::Let, + Atom27::Tuple, + Atom27::Add, + Atom27::Neg, + Atom27::Multiply, + Atom27::Divide, + Atom27::Power, + Atom27::Equal, + Atom27::Order, + Atom27::If, + Atom27::Select, + Atom27::Project, + Atom27::Join, + Atom27::Union, + Atom27::Distinct, + Atom27::Group, + Atom27::Aggregate, + Atom27::Substitute, + Atom27::Rewrite, + Atom27::Differentiate, + Atom27::Integrate, + Atom27::Iterate, + Atom27::Prove, +]; + +/// Unverified historical bibliographic lead, not a proof and not the +/// attribution of the modern formal reconstruction to its historical author. +#[derive(Debug, Clone)] +pub struct SourceLead { + pub author: &'static str, + pub work: &'static str, + pub date_note: &'static str, + pub candidate_catalogue_uri: &'static str, +} + +/// Historical source and mathematical implementation certification are +/// orthogonal: proof replay can certify the math without establishing +/// historical authorship, and vice versa. +#[derive(Debug, Clone)] +pub struct HeritageEntry { + pub id: &'static str, + pub normalized_statement: &'static str, + pub source: Option, + capsule: Option, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum HeritageRefusal { + NoCheckedMathematicalProof, + Replay(ReplayRefusal), +} + +impl HeritageEntry { + pub fn synthetic_e1() -> Result { + let capsule = ReplayCapsule::certify(&e1_problem(), 8)?; + Ok(Self { + id: "synthetic-e1-1690", + normalized_statement: "a=2b, b=2c, z=2a |- z=8c (exact integer premises)", + source: None, + capsule: Some(capsule), + }) + } + + /// Historical lead only; the existing E1 grammar has no differentiation, + /// function application or quantification over differentiable functions. + pub fn leibniz_product_rule() -> Self { + Self { + id: "leibniz-product-rule-candidate", + normalized_statement: "D(f*g)=D(f)*g+f*D(g), for differentiable f,g", + source: Some(SourceLead { + author: "Gottfried Wilhelm Leibniz", + work: "Nova Methodus pro Maximis et Minimis", + date_note: "1684; attribution and textual correspondence require primary-source review", + candidate_catalogue_uri: "https://digitalcollections.hkust.edu.hk/Detail/objects/b540295", + }), + capsule: None, + } + } + + /// An additional corpus lead. No proof or original-edition claim. + pub fn euler_identity() -> Self { + Self { + id: "euler-identity-candidate", + normalized_statement: "exp(i*pi)+1=0 (complex exponential)", + source: Some(SourceLead { + author: "Leonhard Euler", + work: "Historical attribution and notation to be verified", + date_note: "18th-century work; no primary-source edition checked by this probe", + candidate_catalogue_uri: "", + }), + capsule: None, + } + } + + pub fn is_mathematically_certified(&self) -> bool { + self.capsule.is_some() + } + + /// Replay is permitted only with an actual checked E1 capsule. A text + /// claim and bibliographic lead can never implicitly become executable. + pub fn replay(&self, value: i64) -> Result { + self.capsule + .as_ref() + .ok_or(HeritageRefusal::NoCheckedMathematicalProof)? + .replay(value) + .map_err(HeritageRefusal::Replay) + } + + fn program(&self) -> Option<&[Step]> { + self.capsule.as_ref().map(|c| c.program()) + } +} + +/// Research fixture, intentionally mixing an executable *synthetic* theorem +/// with historically attributed *uncompiled* mathematical statements. +pub fn sample_corpus() -> Result, ReplayRefusal> { + Ok(vec![ + HeritageEntry::synthetic_e1()?, + HeritageEntry::leibniz_product_rule(), + HeritageEntry::euler_identity(), + ]) +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct MetaStudy { + pub total_entries: usize, + pub historical_leads: usize, + pub mathematically_certified: usize, + pub distinct_compiled_programs: usize, + /// Only atoms witnessed by an actually compiled R2IL program. + pub observed_atoms: Vec, +} + +/// Deterministic descriptive analysis. No equivalence between historical +/// methods, no complexity claim, and no unlicensed mathematical law inference. +pub fn analyse(corpus: &[HeritageEntry]) -> MetaStudy { + let mut programs = BTreeSet::new(); + let mut atoms = BTreeSet::new(); + for entry in corpus { + if let Some(steps) = entry.program() { + programs.insert(steps.iter().map(Step::mnemonic).collect::>()); + for step in steps { + match step { + Step::PushConst(_) => { atoms.insert(Atom27::Const); } + Step::PushVar(_) => { atoms.insert(Atom27::Var); } + Step::IntMult => { atoms.insert(Atom27::Multiply); } + } + } + } + } + MetaStudy { + total_entries: corpus.len(), + historical_leads: corpus.iter().filter(|x| x.source.is_some()).count(), + mathematically_certified: corpus.iter() + .filter(|x| x.is_mathematically_certified()).count(), + distinct_compiled_programs: programs.len(), + observed_atoms: atoms.into_iter().collect(), + } +} From 246fff8db8dded832223ba6edb1c32b5cbc68711 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 08:48:43 +0200 Subject: [PATCH 2/4] test(math-foundry): refuse uncertified historical proofs and count 27 atom hypotheses --- crates/egglog-r2il-probe/tests/heritage.rs | 44 ++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 crates/egglog-r2il-probe/tests/heritage.rs diff --git a/crates/egglog-r2il-probe/tests/heritage.rs b/crates/egglog-r2il-probe/tests/heritage.rs new file mode 100644 index 000000000..93e67b217 --- /dev/null +++ b/crates/egglog-r2il-probe/tests/heritage.rs @@ -0,0 +1,44 @@ +//! Heritage study cannot confuse attribution with a checked proof. +use std::collections::BTreeSet; +use egglog_r2il_probe::heritage::{ + Atom27, HeritageEntry, HeritageRefusal, PROPOSED_ATOMS, analyse, sample_corpus, +}; + +#[test] +fn exactly_27_candidate_atoms_without_a_universality_claim() { + let unique: BTreeSet = PROPOSED_ATOMS.into_iter().collect(); + assert_eq!(PROPOSED_ATOMS.len(), 27); + assert_eq!(unique.len(), 27); +} + +#[test] +fn historical_catalogue_leads_do_not_execute_as_proofs() { + for entry in [ + HeritageEntry::leibniz_product_rule(), + HeritageEntry::euler_identity(), + ] { + assert!(entry.source.is_some()); + assert!(!entry.is_mathematically_certified()); + assert_eq!( + entry.replay(7), + Err(HeritageRefusal::NoCheckedMathematicalProof) + ); + } +} + +#[test] +fn synthetic_e1_is_replayable_but_not_misattributed_to_leibniz() { + let corpus = sample_corpus().expect("E1 proof certified"); + assert_eq!(corpus[0].id, "synthetic-e1-1690"); + assert!(corpus[0].source.is_none()); + assert_eq!(corpus[0].replay(7), Ok(56)); + let report = analyse(&corpus); + assert_eq!(report.total_entries, 3); + assert_eq!(report.historical_leads, 2); + assert_eq!(report.mathematically_certified, 1); + assert_eq!(report.distinct_compiled_programs, 1); + assert_eq!( + report.observed_atoms, + vec![Atom27::Const, Atom27::Var, Atom27::Multiply] + ); +} From 203f5c4baf8bcfc25ccd3fda22f7b7b226f560b7 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 08:48:45 +0200 Subject: [PATCH 3/4] docs(math-foundry): define heritage provenance and Thought-Git audit gates --- crates/egglog-r2il-probe/HERITAGE_STUDY.md | 50 ++++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 crates/egglog-r2il-probe/HERITAGE_STUDY.md diff --git a/crates/egglog-r2il-probe/HERITAGE_STUDY.md b/crates/egglog-r2il-probe/HERITAGE_STUDY.md new file mode 100644 index 000000000..f6e58651d --- /dev/null +++ b/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. From 68043f20d28a09e364efe488a4fbd808e37a71b3 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 08:48:48 +0200 Subject: [PATCH 4/4] feat(math-foundry): expose heritage PoC research module --- crates/egglog-r2il-probe/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/crates/egglog-r2il-probe/src/lib.rs b/crates/egglog-r2il-probe/src/lib.rs index d84a530fd..62c30aa9b 100644 --- a/crates/egglog-r2il-probe/src/lib.rs +++ b/crates/egglog-r2il-probe/src/lib.rs @@ -23,6 +23,7 @@ pub mod artifact; pub mod catalogue; +pub mod heritage; pub mod encode; pub mod laws; pub mod lower;