Integrate #1694/#1695 into main with isolated math-foundry CI and semantic gates

.github/workflows/egglog-r2il-probe.yml

@@ -0,0 +1,70 @@
+name: egglog R2IL mathematical compiler probe
+# Own [workspace] excluded from root tests; this is a lab gate, not production admission.
+on:
+  pull_request:
+    paths:
+      - 'crates/egglog-r2il-probe/**'
+      - 'crates/lance-graph-contract/**'
+      - 'crates/lance-graph-r2il/**'
+      - 'crates/lance-graph-mask-risc/**'
+      - '.github/workflows/egglog-r2il-probe.yml'
+      - 'rust-toolchain.toml'
+  push:
+    branches: [main]
+    paths:
+      - 'crates/egglog-r2il-probe/**'
+      - 'crates/lance-graph-contract/**'
+      - 'crates/lance-graph-r2il/**'
+      - 'crates/lance-graph-mask-risc/**'
+      - '.github/workflows/egglog-r2il-probe.yml'
+      - 'rust-toolchain.toml'
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+env:
+  CARGO_TERM_COLOR: always
+  CARGO_INCREMENTAL: "0"
+  CARGO_PROFILE_DEV_DEBUG: "0"
+  CARGO_PROFILE_TEST_DEBUG: "0"
+  RUST_BACKTRACE: "1"
+jobs:
+  math-foundry:
+    name: excluded-crate fmt, clippy and tests
+    runs-on: ubuntu-24.04
+    timeout-minutes: 60
+    defaults:
+      run:
+        working-directory: lance-graph
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          path: lance-graph
+          persist-credentials: false
+      - name: Checkout AdaWorldAPI/ndarray (sibling path patch)
+        uses: actions/checkout@v4
+        with:
+          repository: AdaWorldAPI/ndarray
+          path: ndarray
+          persist-credentials: false
+      - name: Rust toolchain
+        run: rustup show
+      - name: Resolve target-cpu=native for this runner
+        id: cpu
+        run: |
+          flags=$(.github/scripts/resolve-native-rustflags.sh)
+          echo "RUSTFLAGS=$flags" >> "$GITHUB_ENV"
+          hash=$(printf %s "$flags" | sha256sum | cut -c1-16)
+          echo "flags=$hash" >> "$GITHUB_OUTPUT"
+      - uses: Swatinem/rust-cache@v2
+        with:
+          key: cpu-${{ steps.cpu.outputs.flags }}
+          workspaces: lance-graph/crates/egglog-r2il-probe
+      - name: fmt
+        run: cargo fmt --manifest-path crates/egglog-r2il-probe/Cargo.toml --check
+      - name: clippy
+        run: cargo clippy --manifest-path crates/egglog-r2il-probe/Cargo.toml --all-targets -- -D warnings
+      - name: tests
+        run: cargo test --release --manifest-path crates/egglog-r2il-probe/Cargo.toml

crates/egglog-r2il-probe/HERITAGE_STUDY.md

@@ -1,13 +1,13 @@
 # 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.
+**Dependency chain (2026-10-22):** [#1690](https://github.com/AdaWorldAPI/lance-graph/pull/1690) (E1 compiler) and [#1693](https://github.com/AdaWorldAPI/lance-graph/pull/1693) (Stage C capsule) merged into `main`; [#1694](https://github.com/AdaWorldAPI/lance-graph/pull/1694) (Stage D catalogue) merged into the Stage C feature branch, and [#1695](https://github.com/AdaWorldAPI/lance-graph/pull/1695) (this Stage E) into the Stage D feature branch, not into `main`. Draft integration [#1698](https://github.com/AdaWorldAPI/lance-graph/pull/1698) carries the combined lab stack and dedicated excluded-workspace tests; it is not production-admitted.
 
 ## 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.
+3. **Checked computational artifact**: currently only the synthetic E1 exact-integer substitution, compiled by egglog and replayed through R2IL scalar `FoldDialect` with independent i128 oracle. E1 uses empty planes and scalar `INT_MULT`; it does NOT yet exercise a mask-RISC `execute_into` population fold. An exact symbolic proof is not a proof of checked-i64 intermediate-overflow equivalence for arbitrary inputs (see `REVIEW_GATES.md`).
 
 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.
 
@@ -48,3 +48,5 @@ A replay recipe should be sufficient to recompute the outcome if the source snap
 
 `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.
+
+**Integration check (2026-10-22):** #1698's new isolated Cargo job was triggered and stopped at `cargo fmt --check`; Clippy and tests were consequently skipped on that first run. Formatting and a complete targeted green CI run are open, independent of the semantic gates. The main-workspace checks are not substitutes.

crates/egglog-r2il-probe/REVIEW_GATES.md

@@ -0,0 +1,80 @@
+# Mathematical foundry integration review, 2026-10-22
+
+**Status: REVIEW GATES, not certification or production admission.** This document connects #1689–#1695 and records the falsifiers required to integrate the Stage D/E research branch into `main`. It is a review artifact, not an implementation claim. The branch also adds a dedicated Cargo CI workflow, because `crates/egglog-r2il-probe` is a workspace-excluded lab.
+
+## Merge topology
+
+- #1689 and #1692: source harvest, not executable admission.
+- #1690: merged into main; MORK query_multi SET oracle and independent answer/cost split, plus egglog exact E1 Stage B. The MORK oracle is not a BAG execution engine; callback counts and deduplicated head tuples have different types.
+- #1691: merged into main; separate three-valued Bangladesh site-service scalar oracle with independent grid, backup and telecom inputs. No grid risk becomes a measured tower-down observation.
+- #1693: merged into main; E1 cold `ReplayCapsule`.
+- #1694: merged into `lab/math-foundry-1-proof-replay-20261022`, not main.
+- #1695: merged into `lab/math-foundry-2-certified-catalogue-20261022`, not main.
+- This integration review is based on the latter branch after merge commit `67d060134e570c5cc99caa782af8fd6fcbeec5c3`; the catalogue and heritage remain lab-only.
+
+## Gate P0: mathematical proof is not checked runtime substitutability
+
+`artifact::ReplayCapsule::certify` proves `Arith::Exact` symbolic identities; `lower::run_steps` executes `INT_MULT` with *checked i64* semantics. For general inputs, a correct exact-integer final value is insufficient to establish that baseline and optimized programs have the same intermediate overflow/refusal behavior.
+
+**Falsifier E-OVERFLOW-CANCEL:** For an eager checked baseline `a = i64::MAX * c; z = 0 * a`, input `c=2` refuses with overflow; a direct exact reduction of `z` to zero must NOT be accepted as equivalent on this input without an explicit valid-range/effect certificate. Test both `Ok(value)` and `Err(Overflow)` arms against a separately implemented, specified baseline. Do not assume egglog currently selects this reduction: verify extraction and keep a failure witness regardless of its tie-break.
+
+**Admission:** either a cheaply checkable input-range witness covering every original intermediate step and the compiled steps, or an effect/error-preserving checked extraction. A certificate must include arithmetic domain and baseline evaluation semantics. A four-point i128 sample cannot discharge a quantified proof obligation. Remain in lab until falsified or resolved.
+
+## Gate P0: contradictory or ambiguous premises
+
+`Problem.premises` are fed to egglog as unrestricted `union` assertions while `oracle::solve` ignores a premise once its `lhs` is known. Duplicate contradictory equations, cycles and conflicting paths may therefore have no consistent assignment for arbitrary runtime inputs, yet a purely equational proof need not identify that domain restriction.
+
+**Falsifier E-PREMISE:** `a=2*c; a=3*c` with `c=1` must not become a universally applicable compiled function. Require a coherent constraint/domain witness, or conservatively refuse ambiguous/cyclic/nonfunctional systems. Test duplicate `lhs`, cycles, disconnected premises and order permutation independently of egglog's extraction.
+
+## Gate P1: cache is currently one entry per SemanticKey
+
+`catalogue::Catalogue.entries` is `BTreeMap<SemanticKey, Entry>`; ABI and binding witness are stored inside `Entry`, not the map key. A second promotion for the same expression but a different target/binding **replaces** the earlier entry. The guard causes a conservative fallback, but the implementation does not yet demonstrate simultaneous multi-binding reuse.
+
+**Falsifier E-MULTIBIND:** Promote the same expression for (target A, source generation 1) and (target B, generation 2), then request both. Either both remain separately retrievable, or the spec must label overwrite+fallback as a deliberate single-slot cache. For 256 × 4096 contexts, prefer an immutable `RecipeKey = (canonical term, typed laws, arithmetic domain, checker/toolchain version, target ABI)` and an independent **validated** `BindingKey = (dataset/version, scope, coordinate generation, source roots)`. A witness is supplied by the caller today; no source attestation is performed.
+
+## Gate P1: independent proof verification and durable identity
+
+`ReplayCapsule::recheck` regenerates egglog proof text with egglog and compares rendering bytes. That is conservative regeneration, **not** an independent proof checker, a portable proof format or an integrity-authenticated durable certificate.
+
+**Falsifier E-PROOF:** mutate one premise, law/domain, proof edge, cost/target, lowered step, source root, checker identity or ABI; every material mutation must be rejected by an independently implemented verifier (or exact signed/hash-bound certificate format). A changed pretty-printer must not silently redefine proof validity. Pin the egglog, OGAR, R2IL and law-catalogue identities; branch=`main` git dependencies are not version pins.
+
+Prefer a canonical typed proof DAG and explicit checker version; keep rendered text as a human-readable annex. Capsule digest, certification verdict and Thought-Git execution/commit receipts are three different objects.
+
+## Gate P1: economic and execution certification
+
+`CostEvidence` is provided by the caller and `pays_for_itself` checks a strict arithmetic inequality. This is an in-memory lab policy, not an independent performance measurement or statistical admission.
+
+**Falsifier E-COST:** measure cold harvest/rewrite/proof-check/lowering plus lookup, binding, execution and fallback at fixed inputs; include a no-sharing competitor, an existing R2IL/relalg baseline, miss/stale/overflow arms, confidence ranges and source/version scope. Benchmark 256 templates × 4096 frames with at least two bindings for one template; measure total time and memory, not only the hot hit. Never relabel a synthetic test `CostEvidence` as empirical data.
+
+## Gate P1: excluded-crate checks
+
+The root workspace's green Build/Rust tests do not exercise this excluded crate. `.github/workflows/egglog-r2il-probe.yml` is the new targeted workflow and must finish green on this integration PR (fmt, clippy, release tests). The local Cargo toolchain and sibling ndarray checkout were unavailable to this review; all checks remain unverified until CI reports.
+
+## Gate P2: historical mathematics, provenance and typed effects
+
+`heritage::HeritageEntry` keeps source leads and mathematical capsules separate. Keep Leibniz and Euler **uncertified**. A modern formal reconstruction is not a checked historical attribution. Treat the 27 atoms as candidate semantic categories, not 27 machine opcodes or a universal grammar. Its current observed coverage is only `Const/Var/Multiply`.
+
+The next study must version original source edition/folio, normalized statement, assumptions, theorem/checker, extraction/proof, target/ABI, actual input binding, output/overflow, and cold versus hot costs. D-TGB-4 should store **references** to these artifacts, not megabytes of proof text in each thought, and must keep proof checking, replay evidence and actual `LanceCycleWriter` commit acknowledgement distinct.
+
+For #1691, reuse the typed **three-state physical oracle** only after independently versioned site/telecom/backup observations. Preserve `Unknown` and contradiction, per-tower GUID/window, and pure-versus-effect ordering. Do not map the synthetic legacy `grid_status` to independent observed grid power. Do not admit external `Gather` or physical side effects via algebraic equivalence.
+
+## Admission decision
+
+**Do not auto-merge.** This review enables a real integration diff and a missing CI gate; it does **not** certify the semantic counterexamples above as fixed. Maintain `egglog -> proof/rewrite` strictly cold and `R2IL -> FoldDialect -> mask-risc execute_into` as the permitted execution chain. Promote only after P0 invariants are either proven by witnesses/tests or explicitly restricted to the synthetic E1 admitted input domain.
+
+## Status after rebase onto main (2026-10-22, #1696 merged)
+
+Both P0 gates are now closed **for the linear E1 language**, each with a test that fails when its guard is removed. The P1 gates are unchanged.
+
+- **E-PREMISE: closed.**
+  - Reproduced first: `[z=2c, z=3c]` at c=7 certified 14, and 21 with the premises swapped; the oracle agreed both times.
+  - `oracle::coefficients` now checks every premise:
+    - a second definition must agree;
+    - a cycle such as `c = 2c` is inconsistent;
+    - a premise the target cannot reach is refused.
+  - `ReplayCapsule::certify` refuses such systems with `InvalidPremises` before egglog runs.
+- **E-OVERFLOW-CANCEL: closed by an input-range witness.**
+  - Reproduced first: `a = -1*c; z = -1*a` returned `Ok(i64::MIN)` on a hit where the eager checked baseline overflows (the codex P2), and `a = MAX*c; z = 0*a` returned 0 at c=2.
+  - `Catalogue::promote` records `CheckedRange`: the inputs on which every premise's intermediate `k * x` fits i64.
+  - `execute_or` falls back outside it (`OutsideCheckedRange`).
+  - The witness covers only the eager baseline that evaluates every premise, and only premises linear in the target. A non-linear language needs a new witness.

crates/egglog-r2il-probe/src/artifact.rs

@@ -60,14 +60,17 @@ fn check_compilation(c: &Compiled) -> Result<(), ReplayRefusal> {
 impl ReplayCapsule {
     /// Run the cold compiler and require a checked, closed exact result.
     pub fn certify(problem: &Problem, fuel: usize) -> Result<Self, ReplayRefusal> {
+        // The premises must define the goal as ONE function of the target.
+        // egglog unions contradictory premises without complaint, and its
+        // extraction then picks a definition by cost or order.
+        oracle::coefficients(problem).map_err(|_| ReplayRefusal::InvalidPremises)?;
         let c = compile(problem, Arith::Exact, fuel);
         check_compilation(&c)?;
         let program = lower_steps(&c).map_err(ReplayRefusal::Execution)?;
         let proof = c.proof.ok_or(ReplayRefusal::NoProof)?;
         // This asks egglog to prove the specific selected equality again,
         // rather than treating nonempty rendered proof text as certification.
-        try_prove(problem, Arith::Exact, fuel, &c.extracted)
-            .map_err(ReplayRefusal::Compiler)?;
+        try_prove(problem, Arith::Exact, fuel, &c.extracted).map_err(ReplayRefusal::Compiler)?;
         Ok(Self {
             problem: problem.clone(),
             arith: Arith::Exact,
@@ -139,8 +142,8 @@ impl ReplayCapsule {
     pub fn replay(&self, target_value: i64) -> Result<i64, ReplayRefusal> {
         self.recheck()?;
         let v = self.execute(target_value)?;
-        let expected = oracle::solve(&self.problem, target_value)
-            .ok_or(ReplayRefusal::InvalidPremises)?;
+        let expected =
+            oracle::solve(&self.problem, target_value).ok_or(ReplayRefusal::InvalidPremises)?;
         if i128::from(v) != expected {
             return Err(ReplayRefusal::ResultMismatch {
                 compiled: v,
@@ -156,6 +159,48 @@ mod tests {
     use super::*;
     use crate::e1_problem;
 
+    /// FAILS IF: contradictory premises are certified (in either order).
+    #[test]
+    fn contradictory_premises_are_not_certified() {
+        use crate::Eq;
+        for premises in [
+            vec![
+                Eq {
+                    lhs: "z",
+                    coeff: 2,
+                    rhs: "c",
+                },
+                Eq {
+                    lhs: "z",
+                    coeff: 3,
+                    rhs: "c",
+                },
+            ],
+            vec![
+                Eq {
+                    lhs: "z",
+                    coeff: 3,
+                    rhs: "c",
+                },
+                Eq {
+                    lhs: "z",
+                    coeff: 2,
+                    rhs: "c",
+                },
+            ],
+        ] {
+            let p = Problem {
+                premises,
+                goal: "z",
+                target_var: "c",
+            };
+            assert_eq!(
+                ReplayCapsule::certify(&p, 8).map(|_| ()),
+                Err(ReplayRefusal::InvalidPremises)
+            );
+        }
+    }
+
     #[test]
     fn corrupt_proof_and_program_refuse_on_replay() {
         let good = ReplayCapsule::certify(&e1_problem(), 8).expect("E1");