diff --git a/crates/egglog-r2il-probe/src/catalogue.rs b/crates/egglog-r2il-probe/src/catalogue.rs
new file mode 100644
index 000000000..4e644f319
--- /dev/null
+++ b/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),
+            },
+        }
+    }
+}
diff --git a/crates/egglog-r2il-probe/src/lib.rs b/crates/egglog-r2il-probe/src/lib.rs
index a9d022cb8..d84a530fd 100644
--- a/crates/egglog-r2il-probe/src/lib.rs
+++ b/crates/egglog-r2il-probe/src/lib.rs
@@ -22,6 +22,7 @@
 //!    sharing no code with steps 2-4.
 
 pub mod artifact;
+pub mod catalogue;
 pub mod encode;
 pub mod laws;
 pub mod lower;
diff --git a/crates/egglog-r2il-probe/tests/catalogue.rs b/crates/egglog-r2il-probe/tests/catalogue.rs
new file mode 100644
index 000000000..839076d1b
--- /dev/null
+++ b/crates/egglog-r2il-probe/tests/catalogue.rs
@@ -0,0 +1,93 @@
+//! Stage D: certified cache hit, explicit witness fallbacks, no hot egglog.
+use egglog_r2il_probe::artifact::ReplayCapsule;
+use egglog_r2il_probe::catalogue::{
+    BindingWitness, Catalogue, CostEvidence, FallbackReason, PromotionRefusal, Route, TargetAbi,
+};
+use egglog_r2il_probe::{LowerRefusal, e1_problem};
+
+fn bind() -> BindingWitness {
+    BindingWitness { source_generation: 1, scope: 42, coordinate_generation: 9 }
+}
+
+fn abi() -> TargetAbi {
+    TargetAbi { revision: 1, target: "r2il-checked-i64".into() }
+}
+
+fn measured() -> CostEvidence {
+    // Synthetic evidence for testing the policy, NOT measured performance.
+    CostEvidence {
+        baseline_ns: 300,
+        candidate_ns: 100,
+        compile_and_certify_ns: 1_000,
+        expected_reuse: 10,
+    }
+}
+
+fn trusted(x: i64) -> Result<i64, LowerRefusal> {
+    x.checked_mul(2)
+        .and_then(|v| v.checked_mul(2))
+        .and_then(|v| v.checked_mul(2))
+        .ok_or(LowerRefusal::Overflow)
+}
+
+#[test]
+fn certified_hit_uses_saved_r2il_and_zero_baseline_calls() {
+    let mut cache = Catalogue::new();
+    let p = e1_problem();
+    let compiled = ReplayCapsule::certify(&p, 8).expect("cold E1");
+    cache.promote(compiled, bind(), abi(), measured()).unwrap();
+    assert_eq!(cache.len(), 1);
+    let hit = cache.execute_or(&p, bind(), &abi(), 7, |_| panic!("baseline on hit"));
+    assert_eq!(hit.route, Route::Certified);
+    assert_eq!(hit.result, Ok(56));
+}
+
+#[test]
+fn no_certificate_is_installed_without_economic_gate() {
+    let mut cache = Catalogue::new();
+    let mut losing = measured();
+    losing.candidate_ns = 500;
+    let c = ReplayCapsule::certify(&e1_problem(), 8).expect("cold E1");
+    assert_eq!(
+        cache.promote(c, bind(), abi(), losing),
+        Err(PromotionRefusal::NotAmortized)
+    );
+    assert!(cache.is_empty());
+}
+
+#[test]
+fn changed_coordinates_target_and_semantics_call_baseline() {
+    let mut cache = Catalogue::new();
+    let p = e1_problem();
+    cache.promote(
+        ReplayCapsule::certify(&p, 8).unwrap(), bind(), abi(), measured()
+    ).unwrap();
+
+    let mut stale = bind();
+    stale.source_generation += 1;
+    let out = cache.execute_or(&p, stale, &abi(), 7, trusted);
+    assert_eq!(out.route, Route::Baseline(FallbackReason::BindingChanged));
+    assert_eq!(out.result, Ok(56));
+
+    let other = TargetAbi { revision: 2, target: "r2il-checked-i64".into() };
+    let out = cache.execute_or(&p, bind(), &other, 7, trusted);
+    assert_eq!(out.route, Route::Baseline(FallbackReason::TargetChanged));
+
+    let mut altered = p.clone();
+    altered.premises[0].coeff = 3;
+    let out = cache.execute_or(&altered, bind(), &abi(), 7, |_| Ok(-123));
+    assert_eq!(out.route, Route::Baseline(FallbackReason::CacheMiss));
+    assert_eq!(out.result, Ok(-123));
+}
+
+#[test]
+fn overflow_must_fallback_without_manufacturing_an_answer() {
+    let mut cache = Catalogue::new();
+    let p = e1_problem();
+    cache.promote(
+        ReplayCapsule::certify(&p, 8).unwrap(), bind(), abi(), measured()
+    ).unwrap();
+    let out = cache.execute_or(&p, bind(), &abi(), i64::MAX, trusted);
+    assert_eq!(out.route, Route::Baseline(FallbackReason::CompiledRefused));
+    assert_eq!(out.result, Err(LowerRefusal::Overflow));
+}