Merge pull request #1702 from AdaWorldAPI/lab/dr-math-2-population-evidence-20261022

probe(dr-math): finite-population evidence and counterexample refusal [2/5]

Author: AdaWorldAPI

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.

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;

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)
+}