diff --git a/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md b/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md
new file mode 100644
index 000000000..dd5e982c3
--- /dev/null
+++ b/crates/dr-math-binding-probe/POPULATION_EVIDENCE.md
@@ -0,0 +1,15 @@
+# D-DRMC-2 — Population evidence is not proof of universal mathematics
+
+This stage adds a deliberately small independent **audit/reference** implementation for one 64×64 focus, plus scalar-per-pair differential fixtures. It has zero data storage and does not run in a hot application path.
+
+`Gamma` (constraints, two-valued) and `R` (proposed relationship) are bound through Stage 1: same row/column coordinate domains, the same issue of the same store-sealed frame (still current), and the same focus. A three-valued `R` carries its own validity bits; there is no separately bound validity plane. `UNKNOWN` is not FALSE, and a counterexample is reported before any unknown pair: one observed FALSE refutes the claim whatever the unknown pairs hold. The fixed 4096-pair focus is not the global population, and a DR bit does not encode multiplicity, confidence, observational provenance, or independent data quality.
+
+`universal_on_focus` checks, in order, `eligible > 0`, `false == 0`, `unknown == 0` over *these supplied bits*. This is a **finite-focus result**, not a generalized theorem, a causal discovery, or source attestation. Caller-supplied bits and revision numbers can be fabricated. In particular, no production method may call this a `CertifiedLaw` until an independently sealed source snapshot, completeness proof, interpretation of the constraints, and independent oracle have been checked.
+
+Next falsifiers for an actual discovery pipeline:
+1. Compare against authoritative source observation IDs and a scalar/SQL/datafrog oracle; measure distinct/bag derivations separately.
+2. Add a source seal and valid coverage receipt, distinguish a selected focus from exhaustive whole-population enumeration, and revalidate any learned threshold/rule against a held-out population.
+3. For candidate algebraic rewrites, check the statement under formal mathematical assumptions through an independent proof checker. egglog e-graph extraction alone cannot prove it holds in nature.
+4. Preserve negative controls: empty sample, unknown observations, one contradicting member, stale revision, changed authorization, out-of-focus true member, cyclic/self-supporting derivations.
+
+Runtime masks/folds remain Quack/R2IL/mask-risc or the established direct resident SIMD fast path. The `observe_focus` loop is test/reference checking only and not an alternative production evaluator.
diff --git a/crates/dr-math-binding-probe/src/lib.rs b/crates/dr-math-binding-probe/src/lib.rs
index 196afc4eb..81feb138d 100644
--- a/crates/dr-math-binding-probe/src/lib.rs
+++ b/crates/dr-math-binding-probe/src/lib.rs
@@ -271,3 +271,6 @@ pub fn bind_dr64<'a>(
         validity: operand.validity,
     })
 }
+
+/// Independent 64x64 finite-population reference audit; NEVER a production evaluator.
+pub mod population;
diff --git a/crates/dr-math-binding-probe/src/population.rs b/crates/dr-math-binding-probe/src/population.rs
new file mode 100644
index 000000000..f3cfb0240
--- /dev/null
+++ b/crates/dr-math-binding-probe/src/population.rs
@@ -0,0 +1,110 @@
+//! D-DRMC-2: deliberately small, independent FINITE POPULATION audit oracle.
+//!
+//! NOT a physical runtime executor, graph engine, statistical test, proof of
+//! causality, or independent authentication of supplied source data. Reads
+//! one 64x64 QR focus to find concrete counterexamples before a law is admitted.
+//! Hot production folds remain existing Quack/R2IL/mask-risc/native SIMD.
+use crate::{BoundDr64, FrameStore, Truth};
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct PopulationReport {
+    /// Pairs selected by Gamma within this concrete 64x64 focus.
+    pub eligible: u32,
+    /// Eligible positions with an observed TRUE/valid relationship.
+    pub true_pairs: u32,
+    /// Eligible positions observed FALSE (counterexamples).
+    pub false_pairs: u32,
+    /// Eligible positions without a known TRUE/FALSE observation.
+    pub unknown_pairs: u32,
+}
+
+impl PopulationReport {
+    pub const fn checked(self) -> u32 {
+        self.true_pairs + self.false_pairs
+    }
+    /// Finite-focus only: no statement about unobserved people or any theorem
+    /// over every possible population.
+    pub fn universal_on_focus(self) -> Result<Self, ClaimRefusal> {
+        // Refuted beats unknown (certain-answer semantics): one observed
+        // counterexample refutes the claim whatever the unknown pairs hold,
+        // so it is reported first and never hidden behind `Unknown`.
+        if self.eligible == 0 {
+            return Err(ClaimRefusal::Vacuous);
+        }
+        if self.false_pairs != 0 {
+            return Err(ClaimRefusal::Counterexamples(self.false_pairs));
+        }
+        if self.unknown_pairs != 0 {
+            return Err(ClaimRefusal::Unknown(self.unknown_pairs));
+        }
+        Ok(self)
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum ClaimRefusal {
+    DifferentAxes,
+    /// The selection is three-valued; Gamma selects or it does not.
+    SelectionNotTwoValued,
+    /// Gamma and R were not bound to the same issue of the same frame.
+    DifferentFrame,
+    /// The frame they share is no longer the store's current seal.
+    StaleFrame,
+    /// Gamma and R read different windows of the frame.
+    DifferentFocus,
+    Vacuous,
+    Unknown(u32),
+    Counterexamples(u32),
+}
+
+/// Reference checker over the selection Gamma and the relation R:
+/// 1. Gamma: which DR pairs satisfy the candidate constraints (two-valued);
+/// 2. R: which DR pairs satisfy the proposed relational law, with R's own
+///    validity bits when R's method is three-valued. UNKNOWN is never FALSE.
+///
+/// It compares the bound axes, that both operands share one current frame
+/// issue and one focus. It does not verify that the source exists or that its
+/// relation facts are true.
+pub fn observe_focus(
+    store: &FrameStore,
+    gamma: &BoundDr64<'_>,
+    relation: &BoundDr64<'_>,
+) -> Result<PopulationReport, ClaimRefusal> {
+    if (gamma.method.row, gamma.method.column) != (relation.method.row, relation.method.column) {
+        return Err(ClaimRefusal::DifferentAxes);
+    }
+    if gamma.method.truth != Truth::TwoValued {
+        return Err(ClaimRefusal::SelectionNotTwoValued);
+    }
+    if !gamma.frame.same_issue(&relation.frame) {
+        return Err(ClaimRefusal::DifferentFrame);
+    }
+    if store.check(&gamma.frame).is_err() {
+        return Err(ClaimRefusal::StaleFrame);
+    }
+    if gamma.focus != relation.focus {
+        return Err(ClaimRefusal::DifferentFocus);
+    }
+    let mut report = PopulationReport {
+        eligible: 0,
+        true_pairs: 0,
+        false_pairs: 0,
+        unknown_pairs: 0,
+    };
+    for i in 0..64 {
+        let focus = gamma.rows[i];
+        let known = relation.validity.map_or(u64::MAX, |v| v[i]);
+        let positive = focus & relation.rows[i] & known;
+        let negative = focus & !relation.rows[i] & known;
+        let unknown = focus & !known;
+        report.eligible += focus.count_ones();
+        report.true_pairs += positive.count_ones();
+        report.false_pairs += negative.count_ones();
+        report.unknown_pairs += unknown.count_ones();
+    }
+    debug_assert_eq!(
+        report.eligible,
+        report.true_pairs + report.false_pairs + report.unknown_pairs
+    );
+    Ok(report)
+}
diff --git a/crates/dr-math-binding-probe/tests/population.rs b/crates/dr-math-binding-probe/tests/population.rs
new file mode 100644
index 000000000..424e6754b
--- /dev/null
+++ b/crates/dr-math-binding-probe/tests/population.rs
@@ -0,0 +1,287 @@
+use dr_math_binding_probe::{
+    Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand,
+    Scope, Truth, bind_dr64,
+    population::{ClaimRefusal, PopulationReport, observe_focus},
+};
+
+const FOCUS: Focus = Focus { revision: 3 };
+const SCOPE: Scope = Scope { id: 4 };
+
+fn store() -> FrameStore {
+    FrameStore::new(FrameRevisions {
+        source: 8,
+        relation_map: 1,
+        coordinates: 2,
+    })
+}
+fn sig(method: u16, column: AxisKind) -> MethodSignature {
+    MethodSignature::presence(
+        7,
+        method,
+        Axis {
+            class: 7,
+            kind: AxisKind::Identity,
+        },
+        Axis {
+            class: 7,
+            kind: column,
+        },
+    )
+}
+fn three_valued(mut s: MethodSignature) -> MethodSignature {
+    s.truth = Truth::ThreeValued;
+    s
+}
+fn bind_at<'a>(
+    store: &FrameStore,
+    focus: Focus,
+    s: MethodSignature,
+    rows: &'a [u64; 64],
+    validity: Option<&'a [u64; 64]>,
+) -> BoundDr64<'a> {
+    let at = Guards {
+        frame: store.seal(),
+        focus,
+        scope: SCOPE,
+    };
+    bind_dr64(store, s, s, &at, (focus, SCOPE), Operand { rows, validity }).unwrap()
+}
+fn bind<'a>(store: &FrameStore, s: MethodSignature, rows: &'a [u64; 64]) -> BoundDr64<'a> {
+    bind_at(store, FOCUS, s, rows, None)
+}
+fn gamma_bits() -> [u64; 64] {
+    let mut rows = [0u64; 64];
+    rows[1] = (1 << 2) | (1 << 3);
+    rows[5] = 1 << 6;
+    rows
+}
+/// R holds every Gamma pair AND pairs outside Gamma (bits 4 and 9), so a
+/// checker that reads Gamma in place of R, or counts R outside the focus,
+/// gives a different answer.
+fn relation_bits() -> [u64; 64] {
+    let mut rows = [0u64; 64];
+    rows[1] = (1 << 2) | (1 << 3) | (1 << 4);
+    rows[5] = (1 << 6) | (1 << 9);
+    rows
+}
+
+#[test]
+fn exact_complete_focus_passes_without_causal_claim() {
+    let st = store();
+    let (selected, relation) = (gamma_bits(), relation_bits());
+    // Anti-vacuity: Gamma and R are different bits, and R reaches outside Gamma.
+    assert_ne!(selected, relation);
+    assert!((0..64).any(|i| relation[i] & !selected[i] != 0));
+    let g = bind(&st, sig(1, AxisKind::Property), &selected);
+    let r = bind(&st, sig(2, AxisKind::Property), &relation);
+    let summary = observe_focus(&st, &g, &r).unwrap();
+    assert_eq!(
+        summary,
+        PopulationReport {
+            eligible: 3,
+            true_pairs: 3,
+            false_pairs: 0,
+            unknown_pairs: 0
+        }
+    );
+    assert_eq!(summary.universal_on_focus().unwrap().checked(), 3);
+}
+
+#[test]
+fn one_concrete_counterexample_refuses_claim() {
+    let st = store();
+    let selected = gamma_bits();
+    let mut relation = relation_bits();
+    relation[5] &= !(1 << 6);
+    let g = bind(&st, sig(1, AxisKind::Property), &selected);
+    let r = bind(&st, sig(2, AxisKind::Property), &relation);
+    assert_eq!(
+        observe_focus(&st, &g, &r).unwrap().universal_on_focus(),
+        Err(ClaimRefusal::Counterexamples(1))
+    );
+}
+
+#[test]
+fn unknown_is_not_false_or_proof() {
+    let st = store();
+    let (selected, relation) = (gamma_bits(), relation_bits());
+    let mut known = [u64::MAX; 64];
+    known[1] &= !(1 << 3);
+    let g = bind(&st, sig(1, AxisKind::Property), &selected);
+    let r = bind_at(
+        &st,
+        FOCUS,
+        three_valued(sig(2, AxisKind::Property)),
+        &relation,
+        Some(&known),
+    );
+    let observed = observe_focus(&st, &g, &r).unwrap();
+    assert_eq!(
+        (
+            observed.true_pairs,
+            observed.false_pairs,
+            observed.unknown_pairs
+        ),
+        (2, 0, 1)
+    );
+    assert_eq!(observed.universal_on_focus(), Err(ClaimRefusal::Unknown(1)));
+}
+
+/// Certain-answer semantics: a refuted claim is refuted whatever the unknown
+/// pairs hold, so `Counterexamples` must win over `Unknown`. Gamma 0b111, R
+/// 0b001, validity 0b011: one true, one false, one unknown.
+#[test]
+fn refuted_beats_unknown() {
+    let st = store();
+    let report = |relation: u64, validity: u64| {
+        let (mut g, mut r, mut v) = ([0u64; 64], [0u64; 64], [0u64; 64]);
+        g[0] = 0b111;
+        r[0] = relation;
+        v[0] = validity;
+        let gb = bind(&st, sig(1, AxisKind::Property), &g);
+        let rb = bind_at(
+            &st,
+            FOCUS,
+            three_valued(sig(2, AxisKind::Property)),
+            &r,
+            Some(&v),
+        );
+        observe_focus(&st, &gb, &rb).unwrap()
+    };
+    let both = report(0b001, 0b011);
+    assert_eq!(
+        (both.true_pairs, both.false_pairs, both.unknown_pairs),
+        (1, 1, 1)
+    );
+    assert_eq!(
+        both.universal_on_focus(),
+        Err(ClaimRefusal::Counterexamples(1))
+    );
+    // Twins: unknown only, false only.
+    assert_eq!(
+        report(0b011, 0b011).universal_on_focus(),
+        Err(ClaimRefusal::Unknown(1))
+    );
+    assert_eq!(
+        report(0b011, 0b111).universal_on_focus(),
+        Err(ClaimRefusal::Counterexamples(1))
+    );
+}
+
+#[test]
+fn empty_population_is_a_vacuity_not_a_law() {
+    let st = store();
+    let empty = [0u64; 64];
+    let relation = relation_bits();
+    let g = bind(&st, sig(1, AxisKind::Property), &empty);
+    let r = bind(&st, sig(2, AxisKind::Property), &relation);
+    assert_eq!(
+        observe_focus(&st, &g, &r).unwrap().universal_on_focus(),
+        Err(ClaimRefusal::Vacuous)
+    );
+}
+
+#[test]
+fn axes_frame_and_focus_are_checked_before_reading_bits() {
+    let mut st = store();
+    let (selected, relation) = (gamma_bits(), relation_bits());
+    let g = bind(&st, sig(1, AxisKind::Property), &selected);
+    let wrong_axis = bind(&st, sig(2, AxisKind::Identity), &relation);
+    assert_eq!(
+        observe_focus(&st, &g, &wrong_axis),
+        Err(ClaimRefusal::DifferentAxes)
+    );
+    let known = [u64::MAX; 64];
+    let k3_gamma = bind_at(
+        &st,
+        FOCUS,
+        three_valued(sig(1, AxisKind::Property)),
+        &selected,
+        Some(&known),
+    );
+    let r = bind(&st, sig(2, AxisKind::Property), &relation);
+    assert_eq!(
+        observe_focus(&st, &k3_gamma, &r),
+        Err(ClaimRefusal::SelectionNotTwoValued)
+    );
+    let other_focus = bind_at(
+        &st,
+        Focus { revision: 9 },
+        sig(2, AxisKind::Property),
+        &relation,
+        None,
+    );
+    assert_eq!(
+        observe_focus(&st, &g, &other_focus),
+        Err(ClaimRefusal::DifferentFocus)
+    );
+    let other = store();
+    let foreign = bind(&other, sig(2, AxisKind::Property), &relation);
+    assert_eq!(
+        observe_focus(&st, &g, &foreign),
+        Err(ClaimRefusal::DifferentFrame)
+    );
+    st.advance(FrameRevisions {
+        source: 9,
+        relation_map: 1,
+        coordinates: 2,
+    });
+    assert_eq!(observe_focus(&st, &g, &r), Err(ClaimRefusal::StaleFrame));
+}
+
+#[test]
+fn packed_bit_math_matches_independent_scalar_pair_enumeration() {
+    let st = store();
+    let selected = gamma_bits();
+    let mut relation = relation_bits();
+    relation[1] &= !(1 << 2);
+    let mut known = [u64::MAX; 64];
+    known[5] &= !(1 << 6);
+    let g = bind(&st, sig(1, AxisKind::Property), &selected);
+    let r = bind_at(
+        &st,
+        FOCUS,
+        three_valued(sig(2, AxisKind::Property)),
+        &relation,
+        Some(&known),
+    );
+    let report = observe_focus(&st, &g, &r).unwrap();
+    let mut scalar = [0u32; 4]; // eligible, true, false, unknown
+    for (i, row) in selected.iter().enumerate() {
+        for j in 0..64 {
+            if row & (1u64 << j) == 0 {
+                continue;
+            }
+            scalar[0] += 1;
+            if known[i] & (1u64 << j) == 0 {
+                scalar[3] += 1
+            } else if relation[i] & (1u64 << j) != 0 {
+                scalar[1] += 1
+            } else {
+                scalar[2] += 1
+            }
+        }
+    }
+    assert_eq!(
+        report,
+        PopulationReport {
+            eligible: scalar[0],
+            true_pairs: scalar[1],
+            false_pairs: scalar[2],
+            unknown_pairs: scalar[3]
+        }
+    );
+    assert_eq!(
+        (
+            report.eligible,
+            report.true_pairs,
+            report.false_pairs,
+            report.unknown_pairs
+        ),
+        (3, 1, 1, 1)
+    );
+    assert_eq!(
+        report.universal_on_focus(),
+        Err(ClaimRefusal::Counterexamples(1))
+    );
+}