diff --git a/.claude/plans/dr-mathematical-compiler-v1.md b/.claude/plans/dr-mathematical-compiler-v1.md
index 95f983422..3679f2c39 100644
--- a/.claude/plans/dr-mathematical-compiler-v1.md
+++ b/.claude/plans/dr-mathematical-compiler-v1.md
@@ -4,18 +4,18 @@
 
 ## Thesis
 
-> DR is the structural ABI between ClassView-declared capabilities and mathematical compilation. The compiler discovers candidates from witnessed observed populations, checks explicit assumptions and counterexamples, normalizes eligible mathematics, proves *transformations* where possible, and retains compiled recipes that may be rebound to later populations.
+> DR is the structural ABI between ClassView-declared capabilities and mathematical compilation. The compiler discovers candidates from witnessed observed populations, checks explicit assumptions and counterexamples, normalizes eligible mathematics, proves *transformations* where possible, and retains certified compiled recipes that may be rebound to later populations (certification and rebinding are open acceptance targets, see below).
 
 Names, CUI/TUI labels, tokens and embedding similarity are not proof of mathematical structure. An observational statement about a finite population, an algebraic theorem conditional on axioms, and an empirical/causal generalization are **three different outputs**. None licenses the next without its own evidence.
 
-The same logical DR contract can bind `Identity × Identity`, `Identity × Property`, `Community × Community` or `Class × Capability`. DR64 is one physical shape (64 × 64 Boolean bits = 512 B); a 256 × 256 presence bitmap is 8 KiB. A physical bit encodes participation, **not** a 16-bit foreign ID, rank, evidence, bag multiplicity, SQL NULL, or a proof. These remain separately bound, witnessed carriers.
+The same logical DR contract can bind `Identity × Identity`, `Identity × Property`, `Community × Community` or `Class × Capability`. DR64 is one physical shape (64 × 64 Boolean bits = 512 B); a 256 × 256 presence bitmap is 8 KiB. A physical bit encodes participation, **not** a 16-bit foreign ID, rank, evidence, bag multiplicity, SQL NULL, or a proof. These remain separately bound carriers, except validity: one validity bit per relation bit travels **with** the relation operand, never as a separately typed plane.
 
 HHTL cascade `(part_of:is_a)` coordinate reading and `hhtl::NiblePath` taxonomy routing are *different* objects. Morton8x8's u16 maps 256 × 256 exact Cartesian positions; HHTL masks refine admissible address ranges. HHTL prefix containment does **not** establish arbitrary ontology membership or causality.
 
 ## Three contracts, independent owners
 
 1. **Semantic/structural (zero-dep contract):** ClassView declares per-method identity, typed operand domains, arity, type/semiring, applicable law, effects, and result demand. `compute_dag` declares dependency order but does not itself implement a method; the ClassView method registry cannot mint facts or authorize writes.
-2. **Binding (Quack-adjacent adapter):** resolve class/method and relation-map identities once, then bind borrowed canonical SoA/ordered relation/DR operands with exact row/column coordinates, source+map+palette/index seals, focus, snapshot, validity, authorization scope and method capability. No hot labels, DTO hydration, implicit global→local gather, or storage ownership. A bound 64×64 register may be consumed directly by existing SIMD kernels; R2IL is the general SIMD polyfill, **not** mandatory re-dispatch over prepared bits.
+2. **Binding (Quack-adjacent adapter):** resolve class/method and relation-map identities once, then bind borrowed canonical SoA/ordered relation/DR operands with exact row/column coordinates and method capability, under **three independent guards**: the **frame** (identity: source, relation map, coordinates and index seals; issued by the store that owns them and compared by issue identity, so equal revision numbers from two stores do not alias), the **focus** (motion: which window of the frame is read; moving it does not change the frame) and the **scope** (policy: what the reader may see, checked as its own guard at borrow time, never part of frame identity). Validity accompanies the relation data. The three guards are never collapsed into one generic witness. No hot labels, DTO hydration, implicit global→local gather, or storage ownership. A bound 64×64 register may be consumed directly by existing SIMD kernels; R2IL is the general SIMD polyfill, **not** mandatory re-dispatch over prepared bits.
 3. **Mathematical compilation (cold and replayable):** RelAlg/typed AST expresses admissible mathematics; source-independent oracles (scalar, MORK, datafrog, PostgreSQL as appropriate) test hypotheses; Ruler/Enumo-style guarded law candidates enter egglog; eggcc-inspired extraction respects effects/order; independently checkable proof artifacts and cost model select existing R2IL/Quack/mask-risc procedures. No egglog/MORK interpreter in the runtime hot fold, no new opcodes by default.
 
 `MeTTa` is a declaration frontend, not the numeric executor. `MORK` / `PathMap` are independent differential/reverse-engineering arms, not a canonical relation store. `datafrog` checks fixed-point recursion, not unearned production support. `Thought-Git` may record immutable law/proof/recipe/binding/replay/commit references, but retains its independent write/version authority. ACT-R / Rubicon / Kanban / cognitive-shader-driver consume results and create *proposals*, never become mathematical-ISA owners.
@@ -39,9 +39,9 @@ typed DR/SoA relation + scope, versions, capability, admissible carriers
           ↓ normalized RelAlg / algebraic AST (no row execution)
 candidate rules + independent differential oracles
           ↓ cold Ruler/Enumo → egglog → effect-aware extraction
-proof-checked law + compiled R2IL/Quack recipe + target/ABI identity
+certificate from the certified-compiler boundary (proof verified, law admitted, lowering validated) + compiled recipe + target/ABI identity
           ↓ cache of mathematical recipe (not source-specific fact)
-runtime: re-BIND current witnesses → choose admitted carrier
+runtime: check frame, focus, scope (each on its own) → choose admitted carrier
           ↓ direct resident SIMD OR R2IL/Quack → mask-risc → ndarray::simd
 result + read receipt  ──────→ consumer ACT-R/Rubicon/MedCare/IAM/etc.
                                   effect proposal → independent commit gate
@@ -71,8 +71,24 @@ No new evaluator: physical-specialized folds may consume already-bound DR regist
 
 Each stage is independently reviewable and STACKED upon the prior draft branch. Only after source attestation, oracle checks, independent proof checker and full cost tests may a specific pattern become a production capability. Each must refuse unsupported shapes, not silently degrade semantics.
 
+## Three boundaries
+
+The charter keeps three questions apart:
+
+1. **What mathematics permits.** An algebraic identity holds under stated axioms over a stated domain, independently of this codebase.
+2. **What the compiler has certified.** A `RecipeCertificate` is issued only by a certified-compiler boundary, after independent proof verification (egglog checks its own derivations), typed law admission (the assumptions the law holds under) and target-lowering validation. A caller-asserted proof status or digest is never sufficient. Until that boundary exists for a law shape, admission refuses (`NoCertifiedCompiler`). Stage B's `ReplayCapsule` is replay and audit evidence for its own E1 language, not a proof authority.
+3. **What one execution may bind.** Every execution checks frame identity, focus, scope authorization and relation validity on its own.
+
+Proving that a derivation follows from admitted laws does not show those laws hold for a newly observed population; that remains the finite-population / empirical question of Stage 2.
+
 ## Experimental success criterion
 
-One ClassView-declared method over a witnessed `Identity×Property` DR64, and one `Identity²` relation, normalize to the same **correctly typed** mathematical primitive *only when warranted by guards*; a independently evaluated finite population falsifies wrong assumptions; a checked law allows compiling a reusable target recipe; the same recipe binds to two fresh, different snapshots without sharing their source data. Report bind, indexing, prefetch, execution, extraction, storage, proof-check, cold/warm amortization and negative controls. No performance claim in this document.
+One ClassView-declared method over a guarded `Identity×Property` DR64, and one `Identity²` relation, normalize to the same **correctly typed** mathematical primitive *only when warranted by guards*; an independently evaluated finite population falsifies wrong assumptions.
+
+A checked mathematical law may become an executable recipe only after independent proof verification, typed law admission, and target-lowering validation by a certified-compiler boundary. The first candidate is **associativity of Boolean relation composition** across compatible ClassView domains, `(R ∘ S) ∘ T = R ∘ (S ∘ T)` over OR/AND. The identity itself is established algebra; what is open is whether the typed RelAlg representation, the egglog proof/checking route, the lowering, the certificate and runtime selection preserve it. Its integration, certification and specialization-selection gates remain open hypotheses. The first selection gate compares verified implementations or association orders **of the same typed operation**, with correctness established before cost decides. GF(2) elimination or M4RI-style methods compute over XOR/AND, not OR/AND, and may be considered only through an explicit semantics-preserving reduction, never as interchangeable kernels.
+
+Recipe reuse across two distinct store-issued snapshot frames is a separate probe (coresearch X8). Each execution must independently validate frame identity, focus motion, scope authorization and relation validity. A changed binding must neither silently reuse stale operands nor be counted as successful recipe rebinding when execution falls back to baseline (Stage B's catalogue falls back on any binding change today, `catalogue.rs` `BindingChanged`).
+
+Until certification and rebinding are demonstrated, these remain acceptance targets, not shipped capabilities. Report bind, indexing, prefetch, execution, extraction, storage, proof-check, cold/warm amortization and negative controls. No performance claim in this document.
 
 **This is an architecture and experiment charter, not implementation, permission to merge or an achieved scientific discovery.**
diff --git a/.github/workflows/dr-math-binding-probe.yml b/.github/workflows/dr-math-binding-probe.yml
new file mode 100644
index 000000000..b5cc18156
--- /dev/null
+++ b/.github/workflows/dr-math-binding-probe.yml
@@ -0,0 +1,64 @@
+name: DR Mathematical Binding Probe
+# Own [workspace] excluded from root tests; a lab gate, not production
+# admission. Mirrors egglog-r2il-probe.yml's toolchain setup: the pinned
+# toolchain from rust-toolchain.toml, never `stable`.
+on:
+  pull_request:
+    paths:
+      - "crates/dr-math-binding-probe/**"
+      - "crates/lance-graph-contract/**"
+      - "crates/lance-graph-act-r/**"
+      - ".github/workflows/dr-math-binding-probe.yml"
+      - "rust-toolchain.toml"
+  push:
+    branches: [main]
+    paths:
+      - "crates/dr-math-binding-probe/**"
+      - "crates/lance-graph-contract/**"
+      - "crates/lance-graph-act-r/**"
+      - ".github/workflows/dr-math-binding-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:
+  isolated-probe:
+    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: 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/dr-math-binding-probe
+      - name: fmt
+        run: cargo fmt --manifest-path crates/dr-math-binding-probe/Cargo.toml --check
+      - name: clippy
+        run: cargo clippy --manifest-path crates/dr-math-binding-probe/Cargo.toml --all-targets -- -D warnings
+      - name: tests
+        run: cargo test --release --manifest-path crates/dr-math-binding-probe/Cargo.toml
diff --git a/crates/dr-math-binding-probe/Cargo.toml b/crates/dr-math-binding-probe/Cargo.toml
new file mode 100644
index 000000000..1ee8ff503
--- /dev/null
+++ b/crates/dr-math-binding-probe/Cargo.toml
@@ -0,0 +1,15 @@
+# D-DRMC-1: isolated, non-production structural binding probe.
+[package]
+name = "dr-math-binding-probe"
+version = "0.0.0"
+edition = "2024"
+publish = false
+description = "Borrowed DR64 / ClassView-style typed structure and source witness admission probe; never executes population rows."
+
+[workspace]
+
+[dependencies]
+lance-graph-contract = { path = "../lance-graph-contract" }
+
+[dev-dependencies]
+lance-graph-act-r = { path = "../lance-graph-act-r" }
diff --git a/crates/dr-math-binding-probe/END_TO_END_GATES.md b/crates/dr-math-binding-probe/END_TO_END_GATES.md
new file mode 100644
index 000000000..5acb4c3b4
--- /dev/null
+++ b/crates/dr-math-binding-probe/END_TO_END_GATES.md
@@ -0,0 +1,53 @@
+# D-DRMC-4 — integration, harvesting and downstream acceptance
+
+**Status: STAGED LAB TEST + FUTURE DEPENDENCY MATRIX, not production completion.**
+
+## What this stacked PR actually exercises
+
+- An actual `ClassView` fixture declares `memberOf -> effectiveRoles` via the existing `compute_dag` method and its Kahn-order contract.
+- Stage 1 binds typed `Identity×Property` DR64 planes as borrowed words against caller-supplied source/map/focus/scope numbers.
+- Stage 2 compares constrained finite-focus observations to reference mask counting (and its scalar differential tests).
+- Stage 3 gates a *synthetic* mathematical proof reference against a distinct compiled artifact identity. **The checked proof flag is not real checker attestation.**
+- The existing `lance-graph-act-r` crate accepts eligible outputs to arbitrate a deterministic decision proposal and refuses a changed snapshot. No ActionDef or write, no Cognitive Shader Driver dependency.
+
+This tests boundary shapes and refusals only. It does **not** run an egglog theorem compiler, execute R2IL, attest a Lance snapshot or execute a real class method. A positive CI job is *not* the science result.
+
+## Remaining staged, independently owned gates
+
+| Gate | Reused owner / implementation | Proof or falsifier |
+| --- | --- | --- |
+| G0 Class method -> operation | `class_view::compute_dag`; D-QSP/D-RFT #1667 and EXO-121 | Method-specific law, declared dependencies, non-participating fields, no semantic label inside hot register |
+| G1 Real source / map seal | OGAR, D-RMAP-1A separate RelationshipMaps/MapPalettes, Quack binding | Immutable dataset+branch+version; map/index row-address seal; scope/ACL; coordinate rollover; >64 focus frontier; no invented foreign gather |
+| G2 Discovery and constraint scope | DR bounded register + independent population observer | Empty/unknown/one false/out-of-focus counterexample, bag vs distinct; held-out reality generalization explicitly separate |
+| G3 Oracle intake | MeTTa declaration frontend; MORK/PathMap unification; datafrog recursion; scalar/PG K3 | Count Set and BAG separately; output identity vs support; per-loop cycle; no self-support/negative recursion silently accepted |
+| G4 Candidate rewrite discovery | Ruler/Enumo-style rule proposal, `set_rules`, egglog | Type/sort and arithmetic law guards, explicit premise consistency, finite fuel, independent oracle differential |
+| G5 Effect-safe extraction | eggcc-inspired stateful extraction / GKAT `gkat-probe` | Prefetch and source/permission gates not reordered; K3 guard valid; side-effect proposal not committed; causal assumptions declared |
+| G6 Certified compilation | `egglog-r2il-probe` #1690–#1698 (owner) | External portable proof checker, range/overflow/domain witness, checked target ABI, reproducible law/compiler version |
+| G7 Physical execution | R2IL/Quack lowering → mask-risc/ndarray SIMD; direct prepared-DR native folds | Same answer vs independent oracle; no second hot evaluator; count bind/index/readahead/prefetch/scratch/output costs |
+| G8 Deterministic orchestration | ACT-R, Rubicon, Kanban, cognitive-shader-driver; Thought-Git separate | Stale eligibility refusal; proposal vs action permission vs commit receipts; replay traces and separate writing authority |
+| G9 Heritage and cross-domain reuse | Thought-Git audit references; proposed 27-atom hypothesis | Historical source quotation/attribution separately verified; one law + proof + compiled recipe, two different classes and snapshots; counterexample discovers bad abstraction |
+
+### Math heritage example (not implemented)
+
+A *product rule* ascribed to Leibniz is a source lead. Only after faithful source transcription, formal differentiation semantics, independent proof, domain constraints and target lowering may it be called a compiled theorem. Merely storing a label `Leibniz` or egglog rendering a term is no certificate. The 27 mathematical low-code atoms are a falsifiable empirical compression *hypothesis*; measure coverage over published proofs, not a universal basis claim.
+
+### Performance / amortization
+
+Design a controlled 256-rule × 4096-frame experiment with a baseline that must include non-sharing, cold compile/certification, binding/index building, source snapshot validation, state updates, warm/cold caches, direct DR register SIMD vs generic Quack/R2IL, generated code size, and false-positive/escape frontier. An expected fast fold by itself does not amortize a slow binder or compiler. No timings asserted here.
+
+### Ownership and flow
+
+- Do not modify overlapping #1698 mathematics-correction branch, #1667 method/SQL parity plans, EXO-98 Thought-Git storage, or `cognitive-shader-driver`.
+- Preserve the fast resident-register SIMD ruling for #1685: consuming already-prepared bits is **not** a forbidden bypass of R2IL; R2IL remains the general polyfill, not compulsory redispatch of prepared operands.
+- A law proof is not evidence of a causal connection in nature. Theorems, observational finite certificates, generalization evidence, executable artifact and committed effects are independently versioned objects.
+- No merges or production API promotions without a separately owned change, targeted CI, independent truth oracle and reviewer agreement.
+
+## Run
+
+`cargo test --manifest-path crates/dr-math-binding-probe/Cargo.toml`
+
+`cargo clippy --manifest-path crates/dr-math-binding-probe/Cargo.toml --all-targets -- -D warnings`
+
+`cargo fmt --manifest-path crates/dr-math-binding-probe/Cargo.toml --all -- --check`
+
+This crate has its own workspace and is intentionally not covered by every root-workspace test. The workflow in this PR provides a separate CI gate.
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/README.md b/crates/dr-math-binding-probe/README.md
new file mode 100644
index 000000000..67a671d24
--- /dev/null
+++ b/crates/dr-math-binding-probe/README.md
@@ -0,0 +1,18 @@
+# D-DRMC-1: DR64 typed borrow admission probe
+
+A **lab-only** carrier/binder seam next to Quack's existing developer-name-to-numeric resolution, not a replacement for `lance-graph-quack::bind::Binder`. Uses `lance_graph_contract::class_view::ClassId` and `morton8x8` directly; does not add types to the zero-dependency contract, modify the shared Quack binding code or implement another bulk executor.
+
+Run from the crate's directory (own `[workspace]`): `cargo test`.
+
+## Proved by these tests (once executed)
+
+- A DR64 register is borrowed as exactly `&[u64; 64]` (512 bytes), not copied or hydrated.
+- `Identity×Identity` and `Identity×Property` are different **semantic method signatures** even with identical physical bits.
+- Method ordinal matters within the same ClassView class.
+- A three-valued method binds only with its validity bits, which travel WITH the relation bits (`Operand`); a two-valued method refuses validity; BAG is refused. No FALSE/UNKNOWN collapse and no lost multiplicity.
+- Three guards, three types: the **frame** (source, relationship map, coordinates) is a store-issued seal compared by identity, so two stores at equal revisions do not alias and a re-seal is a new frame; the **focus** (motion) and the **scope** (policy) are separate guards that leave the frame valid when they move. Each moved revision is its own refusal.
+- Morton 8×8 arithmetic addresses `(x,y)` precisely but does not establish relation truth.
+
+**Explicit non-proofs:** `FrameStore` is a lab stand-in for the source owner (the seal proves issue identity, not that the revisions describe real data); focus and scope are caller-supplied values, `MethodSignature` is a fixture rather than registry-resolved ClassView method metadata, no optimized fold or real foreign relation binder executes, no ACL policy is evaluated. Production admission requires the existing source owner, D-RMAP-1A table bindings, D-RFT/D-QSP method law, index seal and permission checks. A bitmap is not a universal row binding and cannot express all graph path multiplicities.
+
+Next stack: finite population claim/violation ledger, then compiler recipe eligibility.
diff --git a/crates/dr-math-binding-probe/RECIPE_ADMISSION.md b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md
new file mode 100644
index 000000000..c431c4989
--- /dev/null
+++ b/crates/dr-math-binding-probe/RECIPE_ADMISSION.md
@@ -0,0 +1,15 @@
+# D-DRMC-3 — law, proof, compiled recipe, runtime bind and effect are distinct
+
+This experimental metadata layer enforces the **shape of reuse**, not its scientific truth or physical execution. A `LawReference` keys a mathematical statement by primitive, row/column *kinds*, truth family, population semantics and law revision. It intentionally does not key on `ClassId`, method name, frame or source revision. A theorem about a genuinely common law could therefore be used by multiple ClassViews, after each class method is resolved to a matching mathematical shape. The fully typed method and witnesses remain on each `BoundDr64` and are never stored as law identity.
+
+Authority is split and none of it sits in this layer. **egglog** derives equivalences from admitted laws and checks its own proofs. **Law admission** owns the assumptions a law holds under. A **certified-compiler boundary**, after both of those and a lowering check, issues a `RecipeCertificate`: an opaque value with no public constructor and no caller-set status, so a caller can neither declare a law checked nor attach a digest of its own (the earlier hole, where any nonzero digest passed). Stage B's `ReplayCapsule` is replay and audit evidence for its own E1 substitution language; it is not a proof authority and is not used here. `CompiledReference` identifies compiler revision, code artifact, target ABI and backend. `RecipeOffer` remains **metadata**, not bytes to execute.
+
+**No DR64 certificate exists.** A certified-compiler boundary for Boolean-DR64 laws needs a typed relational statement language, egglog laws over it with checked proofs, and a lowering check; none exists. `admit_recipe` therefore runs every metadata check (effect capability, law shape, law identity, code identity, target) and then refuses with `NoCertifiedCompiler`. The tests pin each earlier refusal and that the end of the path is that refusal, never an offer.
+
+Stage 2's finite-focus `PopulationReport` CANNOT produce a `RecipeCertificate`. Even a complete 64x64 population pass is not a theorem outside its declared scope, and a proof that a derivation follows from admitted laws does not show the laws hold for a newly observed population.
+
+Relevant existing foundation: merged #1690–#1696 `egglog-r2il-probe` E1, with #1698 handling contradictory assumptions and exact-vs-checked overflow in a *different owned branch*. This PR does not reimplement or change egglog, Ruler, Enumo, eggcc or their proof format. Their admission must happen COLD, with source/outcome provenance, scalar/domain oracles, deterministic replay, effect-order constraints, measured costs and a target ABI gate.
+
+The next integration stage must prove an actual **ClassView→relation frame→method law→RelAlg AST→compiled recipe→mask-risc/native SIMD** round trip, including refusals, independent oracles and full cold/amortized economics. Until then this is an isolated falsifiable seam.
+
+ACT-R/Rubicon/kanban/cognitive-shader-driver are downstream consumers and are not allowed to use a mathematical proof as effect authorization. Thought-Git may link immutable law/proof/recipe/binding/replay/commit references when its own write and provenance contracts are ready.
diff --git a/crates/dr-math-binding-probe/src/lib.rs b/crates/dr-math-binding-probe/src/lib.rs
new file mode 100644
index 000000000..7d6cd9909
--- /dev/null
+++ b/crates/dr-math-binding-probe/src/lib.rs
@@ -0,0 +1,279 @@
+//! D-DRMC-1: borrowed typed DR64 operand admission, NOT an evaluator.
+//!
+//! This is a stand-alone probe of the ClassView -> Quack-style BIND contract.
+//! It does not implement a ClassView registry, own RelationshipMap data, decide
+//! mathematical equivalence, attest a source, or run any per-row operation.
+//! Canonical code will remain in the existing owners; this lab tests the shape.
+//!
+//! The bitplane is precisely 64 rows of 64 participation bits (512 B). It
+//! carries neither global ids, bag multiplicity nor provenance. A three-valued
+//! method carries its validity bits WITH the relation bits (see [`Operand`]).
+#![forbid(unsafe_code)]
+
+use std::sync::{Arc, Weak};
+
+use lance_graph_contract::class_view::ClassId;
+
+/// What one numeric coordinate means according to the resolved ClassView.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum AxisKind {
+    Identity,
+    Property,
+    Community,
+    Capability,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub struct Axis {
+    pub class: ClassId,
+    pub kind: AxisKind,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum Truth {
+    TwoValued,
+    ThreeValued,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum Population {
+    Distinct,
+    Bag,
+}
+
+/// Per-method semantic law; *not* a single semantics choice for a whole class.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub struct MethodSignature {
+    pub owner_class: ClassId,
+    pub method_ordinal: u16,
+    pub row: Axis,
+    pub column: Axis,
+    pub truth: Truth,
+    pub population: Population,
+}
+
+impl MethodSignature {
+    pub const fn presence(
+        owner_class: ClassId,
+        method_ordinal: u16,
+        row: Axis,
+        column: Axis,
+    ) -> Self {
+        Self {
+            owner_class,
+            method_ordinal,
+            row,
+            column,
+            truth: Truth::TwoValued,
+            population: Population::Distinct,
+        }
+    }
+}
+
+/// The revisions that identify the reference: which source, which relation
+/// map, which coordinate assignment.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct FrameRevisions {
+    pub source: u64,
+    pub relation_map: u64,
+    pub coordinates: u64,
+}
+
+/// Lab stand-in for the owner of a frame. Only it issues [`Frame`]s, and a
+/// frame compares by identity of that issue, never by value: two stores that
+/// sit at the same numbers do not alias, and re-sealing equal numbers is a
+/// new frame. The mechanism mirrors `dir-rmap-probe`'s `Witness` (a
+/// `Weak<Snapshot>` compared by `ptr_eq`); that type is tied to dir-sim's
+/// `VersionStore`, so it is not reused here.
+#[derive(Debug)]
+pub struct FrameStore {
+    identity: Arc<()>,
+    current: Arc<FrameRevisions>,
+}
+
+impl FrameStore {
+    pub fn new(revisions: FrameRevisions) -> Self {
+        Self {
+            identity: Arc::new(()),
+            current: Arc::new(revisions),
+        }
+    }
+
+    /// Seal the current frame.
+    pub fn seal(&self) -> Frame {
+        Frame {
+            store: Arc::downgrade(&self.identity),
+            seal: Arc::downgrade(&self.current),
+            at: *self.current,
+        }
+    }
+
+    /// Move to new revisions; every frame sealed before is stale from now on.
+    pub fn advance(&mut self, revisions: FrameRevisions) {
+        self.current = Arc::new(revisions);
+    }
+
+    pub fn revisions(&self) -> FrameRevisions {
+        *self.current
+    }
+
+    /// `Ok` iff `frame` is this store's current seal. A frame of another store
+    /// is `ForeignFrame` even at equal numbers; a stale frame of this store
+    /// names the first revision that moved, or `FrameResealed` if none did.
+    pub fn check(&self, frame: &Frame) -> Result<(), Refusal> {
+        if !Weak::ptr_eq(&frame.store, &Arc::downgrade(&self.identity)) {
+            return Err(Refusal::ForeignFrame);
+        }
+        if Weak::ptr_eq(&frame.seal, &Arc::downgrade(&self.current)) {
+            return Ok(());
+        }
+        let (then, now) = (frame.at, *self.current);
+        Err(if then.source != now.source {
+            Refusal::SourceChanged
+        } else if then.relation_map != now.relation_map {
+            Refusal::MapChanged
+        } else if then.coordinates != now.coordinates {
+            Refusal::CoordinatesChanged
+        } else {
+            Refusal::FrameResealed
+        })
+    }
+}
+
+/// A store-issued seal over the reference revisions. No public constructor: a
+/// caller cannot build a frame from numbers, only receive one from
+/// [`FrameStore::seal`].
+#[derive(Clone, Debug)]
+pub struct Frame {
+    store: Weak<()>,
+    seal: Weak<FrameRevisions>,
+    at: FrameRevisions,
+}
+
+impl Frame {
+    /// The revisions this frame was sealed at (for reporting, never identity).
+    pub fn revisions(&self) -> FrameRevisions {
+        self.at
+    }
+
+    /// Same issue of the same store.
+    pub fn same_issue(&self, other: &Frame) -> bool {
+        Weak::ptr_eq(&self.store, &other.store) && Weak::ptr_eq(&self.seal, &other.seal)
+    }
+}
+
+/// Which 64x64 window of the frame is read. Motion, not reference: a new
+/// focus over the same frame is not a new frame.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct Focus {
+    pub revision: u64,
+}
+
+/// What the reader is authorized to see. Policy, checked as its own guard at
+/// borrow time; never part of frame identity.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct Scope {
+    pub id: u64,
+}
+
+/// What a binding was made under.
+#[derive(Clone, Debug)]
+pub struct Guards {
+    pub frame: Frame,
+    pub focus: Focus,
+    pub scope: Scope,
+}
+
+/// The borrowed relation bits and, for a three-valued method, which of them
+/// are known. Validity is a carrier OF R (one bit per R bit, like an Arrow
+/// validity bitmap or Quack's `BoundField.validity`), never a separately typed
+/// plane with a method of its own.
+#[derive(Clone, Copy, Debug)]
+pub struct Operand<'a> {
+    pub rows: &'a [u64; 64],
+    pub validity: Option<&'a [u64; 64]>,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum Refusal {
+    MethodChanged,
+    AxisChanged,
+    SemanticsChanged,
+    ThreeValuedNeedsValidity,
+    TwoValuedHasNoValidity,
+    BagNeedsMultiplicity,
+    ForeignFrame,
+    SourceChanged,
+    MapChanged,
+    CoordinatesChanged,
+    FrameResealed,
+    FocusChanged,
+    ScopeChanged,
+}
+
+/// Borrowed fixed-width register with its resolved type and guards. Never
+/// owns the payload or reinterprets bits into foreign keys.
+#[derive(Clone, Debug)]
+pub struct BoundDr64<'a> {
+    pub method: MethodSignature,
+    pub frame: Frame,
+    pub focus: Focus,
+    pub scope: Scope,
+    pub rows: &'a [u64; 64],
+    pub validity: Option<&'a [u64; 64]>,
+}
+
+/// Validate the declaration, then each guard on its own: the frame against
+/// the store that issued it, then the focus, then the scope. Checks seal
+/// identity and equality of focus and scope, not their authenticity; a
+/// production binder also needs the ClassView registry, the tenant ACL and
+/// the source owner.
+pub fn bind_dr64<'a>(
+    store: &FrameStore,
+    declared: MethodSignature,
+    requested: MethodSignature,
+    bound_at: &Guards,
+    now: (Focus, Scope),
+    operand: Operand<'a>,
+) -> Result<BoundDr64<'a>, Refusal> {
+    if (declared.owner_class, declared.method_ordinal)
+        != (requested.owner_class, requested.method_ordinal)
+    {
+        return Err(Refusal::MethodChanged);
+    }
+    if (declared.row, declared.column) != (requested.row, requested.column) {
+        return Err(Refusal::AxisChanged);
+    }
+    if (declared.truth, declared.population) != (requested.truth, requested.population) {
+        return Err(Refusal::SemanticsChanged);
+    }
+    match (declared.truth, operand.validity) {
+        (Truth::ThreeValued, None) => return Err(Refusal::ThreeValuedNeedsValidity),
+        (Truth::TwoValued, Some(_)) => return Err(Refusal::TwoValuedHasNoValidity),
+        _ => {}
+    }
+    if declared.population != Population::Distinct {
+        return Err(Refusal::BagNeedsMultiplicity);
+    }
+    store.check(&bound_at.frame)?;
+    if bound_at.focus != now.0 {
+        return Err(Refusal::FocusChanged);
+    }
+    if bound_at.scope != now.1 {
+        return Err(Refusal::ScopeChanged);
+    }
+    Ok(BoundDr64 {
+        method: declared,
+        frame: bound_at.frame.clone(),
+        focus: now.0,
+        scope: now.1,
+        rows: operand.rows,
+        validity: operand.validity,
+    })
+}
+
+/// Independent 64x64 finite-population reference audit; NEVER a production evaluator.
+pub mod population;
+
+/// Reusable mathematical law / proof / compiled artifact identity separation (lab only).
+pub mod recipe;
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/src/recipe.rs b/crates/dr-math-binding-probe/src/recipe.rs
new file mode 100644
index 000000000..d727d7766
--- /dev/null
+++ b/crates/dr-math-binding-probe/src/recipe.rs
@@ -0,0 +1,168 @@
+//! D-DRMC-3: mathematical LAW identity != compiled TARGET recipe != current DATA binding.
+//!
+//! Metadata-only guarded admission, NEVER a compiler, runtime scheduler,
+//! binary loader, effect executor or data source attestor. The math law key
+//! deliberately excludes class/method and source versions so a proof about a
+//! mathematical shape can potentially be reused across ClassViews.
+//!
+//! Authority is split, and none of it sits here:
+//! - egglog derives equivalences from admitted laws and checks its own proofs;
+//! - law admission owns the assumptions a law holds under (a finite-population
+//!   report never admits a law);
+//! - a certified-compiler boundary, after both of those and a lowering check,
+//!   issues a [`RecipeCertificate`];
+//! - Stage B's `ReplayCapsule` is replay and audit evidence for its own E1
+//!   substitution language, not a proof authority for anything else.
+//!
+//! No certified-compiler boundary exists for a Boolean-DR64 law yet, so this
+//! layer checks everything it can and then refuses with `NoCertifiedCompiler`.
+use crate::{AxisKind, BoundDr64, Population, Truth};
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub enum Primitive {
+    Selection,
+    BooleanCompose,
+    ArgmaxMasked,
+    CountViolations,
+}
+
+/// Semantics on which a *single mathematical transformation* is conditional.
+/// Not a ClassId/MethodId, not a data snapshot or a cache address.
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub struct LawShape {
+    pub primitive: Primitive,
+    pub row_kind: AxisKind,
+    pub column_kind: AxisKind,
+    pub truth: Truth,
+    pub population: Population,
+}
+
+impl LawShape {
+    pub fn for_method(method: crate::MethodSignature, primitive: Primitive) -> Self {
+        Self {
+            primitive,
+            row_kind: method.row.kind,
+            column_kind: method.column.kind,
+            truth: method.truth,
+            population: method.population,
+        }
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
+pub struct LawReference {
+    pub id: u64,
+    pub revision: u32,
+    pub shape: LawShape,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum Backend {
+    R2ilMaskRisc,
+    ResidentDr64Simd,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct CompiledReference {
+    pub law: LawReference,
+    pub compiled_digest: [u8; 32],
+    pub compiler_revision: u32,
+    pub target_abi: u32,
+    pub backend: Backend,
+}
+
+/// The only thing that makes a recipe reusable: issued by the certified-
+/// compiler boundary once egglog's proof check, law admission and the lowering
+/// check have all passed. No public constructor and no caller-set status, so a
+/// caller can neither declare a law checked nor attach a digest of its own.
+///
+/// ```compile_fail
+/// use dr_math_binding_probe::recipe::RecipeCertificate;
+/// let forged = RecipeCertificate { law: todo!(), compiled: todo!() };
+/// ```
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub struct RecipeCertificate {
+    law: LawReference,
+    compiled: CompiledReference,
+}
+
+impl RecipeCertificate {
+    pub fn law(&self) -> &LawReference {
+        &self.law
+    }
+
+    pub fn compiled(&self) -> &CompiledReference {
+        &self.compiled
+    }
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum Capability {
+    PureMathematics,
+    Proposal,
+    EffectfulAction,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum RecipeRefusal {
+    UnsupportedMathematicalShape,
+    LawChanged,
+    MissingCodeIdentity,
+    WrongTarget,
+    EffectRequiresSeparateAuthorization,
+    /// Every other check passed, but no certified-compiler boundary exists
+    /// for this law shape, so no certificate can be issued.
+    NoCertifiedCompiler,
+}
+
+/// This is a *selection receipt* for a certified compiled artifact, not
+/// executable machine code or a substitute for source/version validation.
+#[derive(Clone, Debug)]
+pub struct RecipeOffer<'a> {
+    pub operand: BoundDr64<'a>,
+    pub certificate: RecipeCertificate,
+}
+
+/// Cold-stage metadata admission for a mathematically typed, already-bound
+/// register: effect capability, law shape, law identity, code identity and
+/// target first, then certification. Certification refuses for every shape
+/// today; see the module docs.
+pub fn admit_recipe<'a>(
+    operand: BoundDr64<'a>,
+    primitive: Primitive,
+    law: LawReference,
+    compiled: CompiledReference,
+    runtime_abi: u32,
+    capability: Capability,
+) -> Result<RecipeOffer<'a>, RecipeRefusal> {
+    if capability != Capability::PureMathematics {
+        return Err(RecipeRefusal::EffectRequiresSeparateAuthorization);
+    }
+    if law.shape != LawShape::for_method(operand.method, primitive) {
+        return Err(RecipeRefusal::UnsupportedMathematicalShape);
+    }
+    if law != compiled.law {
+        return Err(RecipeRefusal::LawChanged);
+    }
+    if compiled.compiler_revision == 0 || compiled.compiled_digest == [0u8; 32] {
+        return Err(RecipeRefusal::MissingCodeIdentity);
+    }
+    if compiled.target_abi != runtime_abi {
+        return Err(RecipeRefusal::WrongTarget);
+    }
+    let certificate = certify(law, compiled)?;
+    Ok(RecipeOffer {
+        operand,
+        certificate,
+    })
+}
+
+/// The certified-compiler boundary. It has no implementation for any
+/// Boolean-DR64 law shape: that needs a typed relational statement language,
+/// egglog laws over it with checked proofs, and a lowering check.
+fn certify(
+    _law: LawReference,
+    _compiled: CompiledReference,
+) -> Result<RecipeCertificate, RecipeRefusal> {
+    Err(RecipeRefusal::NoCertifiedCompiler)
+}
diff --git a/crates/dr-math-binding-probe/tests/binding.rs b/crates/dr-math-binding-probe/tests/binding.rs
new file mode 100644
index 000000000..ef07254d2
--- /dev/null
+++ b/crates/dr-math-binding-probe/tests/binding.rs
@@ -0,0 +1,256 @@
+use dr_math_binding_probe::{
+    Axis, AxisKind, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand,
+    Population, Refusal, Scope, Truth, bind_dr64,
+};
+use lance_graph_contract::morton8x8::Morton8x8;
+
+fn id() -> Axis {
+    Axis {
+        class: 12,
+        kind: AxisKind::Identity,
+    }
+}
+fn property() -> Axis {
+    Axis {
+        class: 12,
+        kind: AxisKind::Property,
+    }
+}
+fn revisions() -> FrameRevisions {
+    FrameRevisions {
+        source: 7,
+        relation_map: 11,
+        coordinates: 3,
+    }
+}
+const FOCUS: Focus = Focus { revision: 5 };
+const SCOPE: Scope = Scope { id: 100 };
+fn guards(store: &FrameStore) -> Guards {
+    Guards {
+        frame: store.seal(),
+        focus: FOCUS,
+        scope: SCOPE,
+    }
+}
+fn signature() -> MethodSignature {
+    MethodSignature::presence(12, 1, id(), property())
+}
+fn bits() -> [u64; 64] {
+    let mut rows = [0u64; 64];
+    rows[17] |= 1u64 << 29;
+    rows
+}
+fn two_valued(rows: &[u64; 64]) -> Operand<'_> {
+    Operand {
+        rows,
+        validity: None,
+    }
+}
+
+#[test]
+fn bind_borrows_exact_bytes_no_materialization() {
+    let store = FrameStore::new(revisions());
+    let rows = bits();
+    let bound = bind_dr64(
+        &store,
+        signature(),
+        signature(),
+        &guards(&store),
+        (FOCUS, SCOPE),
+        two_valued(&rows),
+    )
+    .unwrap();
+    assert!(std::ptr::eq(bound.rows, &rows));
+    assert_eq!(bound.rows[17], 1u64 << 29);
+    assert_eq!(std::mem::size_of_val(&rows), 512);
+}
+
+#[test]
+fn physical_equal_identity_squared_and_identity_property_are_not_interchangeable() {
+    let store = FrameStore::new(revisions());
+    let rows = bits();
+    let identity_squared = MethodSignature::presence(12, 1, id(), id());
+    assert_eq!(
+        bind_dr64(
+            &store,
+            signature(),
+            identity_squared,
+            &guards(&store),
+            (FOCUS, SCOPE),
+            two_valued(&rows)
+        )
+        .unwrap_err(),
+        Refusal::AxisChanged
+    );
+}
+
+#[test]
+fn method_is_not_just_a_class_semantics() {
+    let store = FrameStore::new(revisions());
+    let rows = bits();
+    let other_method = MethodSignature::presence(12, 2, id(), property());
+    assert_eq!(
+        bind_dr64(
+            &store,
+            signature(),
+            other_method,
+            &guards(&store),
+            (FOCUS, SCOPE),
+            two_valued(&rows)
+        )
+        .unwrap_err(),
+        Refusal::MethodChanged
+    );
+}
+
+/// Validity travels with R and is typed by R's method: a three-valued method
+/// needs it, a two-valued one must not carry it. There is no second method a
+/// validity plane could be bound to, so a "validity of a foreign method"
+/// cannot be written.
+#[test]
+fn validity_is_a_carrier_of_the_relation_typed_by_its_method() {
+    let store = FrameStore::new(revisions());
+    let rows = bits();
+    let known = bits();
+    let mut k3 = signature();
+    k3.truth = Truth::ThreeValued;
+    let bind = |m: MethodSignature, operand| {
+        bind_dr64(&store, m, m, &guards(&store), (FOCUS, SCOPE), operand)
+    };
+    assert_eq!(
+        bind(k3, two_valued(&rows)).unwrap_err(),
+        Refusal::ThreeValuedNeedsValidity
+    );
+    let with_validity = Operand {
+        rows: &rows,
+        validity: Some(&known),
+    };
+    let bound = bind(k3, with_validity).unwrap();
+    assert!(std::ptr::eq(bound.validity.unwrap(), &known));
+    assert_eq!(
+        bind(signature(), with_validity).unwrap_err(),
+        Refusal::TwoValuedHasNoValidity
+    );
+    let mut bag = signature();
+    bag.population = Population::Bag;
+    assert_eq!(
+        bind(bag, two_valued(&rows)).unwrap_err(),
+        Refusal::BagNeedsMultiplicity
+    );
+}
+
+/// Each moved revision is its own refusal, and a re-seal at equal numbers is
+/// still a new frame.
+#[test]
+fn every_frame_revision_is_a_separate_refusal() {
+    let rows = bits();
+    let r = revisions();
+    let cases = [
+        (FrameRevisions { source: 8, ..r }, Refusal::SourceChanged),
+        (
+            FrameRevisions {
+                relation_map: 12,
+                ..r
+            },
+            Refusal::MapChanged,
+        ),
+        (
+            FrameRevisions {
+                coordinates: 4,
+                ..r
+            },
+            Refusal::CoordinatesChanged,
+        ),
+        (r, Refusal::FrameResealed),
+    ];
+    for (moved, expected) in cases {
+        let mut store = FrameStore::new(r);
+        let bound_at = guards(&store);
+        store.advance(moved);
+        assert_eq!(
+            bind_dr64(
+                &store,
+                signature(),
+                signature(),
+                &bound_at,
+                (FOCUS, SCOPE),
+                two_valued(&rows)
+            )
+            .unwrap_err(),
+            expected
+        );
+    }
+}
+
+/// The seal is store-issued identity, not equality of numbers: a frame of a
+/// second store at the same revisions does not bind against the first.
+#[test]
+fn two_stores_at_equal_revisions_do_not_alias() {
+    let rows = bits();
+    let first = FrameStore::new(revisions());
+    let second = FrameStore::new(revisions());
+    assert_eq!(first.revisions(), second.revisions());
+    assert!(!first.seal().same_issue(&second.seal()));
+    assert!(first.seal().same_issue(&first.seal()));
+    assert_eq!(
+        bind_dr64(
+            &first,
+            signature(),
+            signature(),
+            &guards(&second),
+            (FOCUS, SCOPE),
+            two_valued(&rows)
+        )
+        .unwrap_err(),
+        Refusal::ForeignFrame
+    );
+}
+
+/// Focus is motion and scope is policy: each is its own guard, and moving
+/// either leaves the frame valid.
+#[test]
+fn focus_and_scope_are_guards_apart_from_the_frame() {
+    let store = FrameStore::new(revisions());
+    let rows = bits();
+    let bound_at = guards(&store);
+    let bind = |now| {
+        bind_dr64(
+            &store,
+            signature(),
+            signature(),
+            &bound_at,
+            now,
+            two_valued(&rows),
+        )
+    };
+    assert_eq!(
+        bind((Focus { revision: 6 }, SCOPE)).unwrap_err(),
+        Refusal::FocusChanged
+    );
+    assert_eq!(
+        bind((FOCUS, Scope { id: 101 })).unwrap_err(),
+        Refusal::ScopeChanged
+    );
+    assert_eq!(store.check(&bound_at.frame), Ok(()));
+    assert!(bind((FOCUS, SCOPE)).is_ok());
+}
+
+#[test]
+fn cartesian_global_coordinate_is_not_a_foreign_relation_proof() {
+    let code = Morton8x8::from_xy(17, 29);
+    assert_eq!((code.x(), code.y()), (17, 29));
+    // Cartesian addressability is exact; occupancy and semantics still
+    // require a DR relationship bit and a ClassView domain binding.
+    let store = FrameStore::new(revisions());
+    let rows = bits();
+    let b = bind_dr64(
+        &store,
+        signature(),
+        signature(),
+        &guards(&store),
+        (FOCUS, SCOPE),
+        two_valued(&rows),
+    )
+    .unwrap();
+    assert_eq!(b.rows[17] & (1u64 << 29), 1u64 << 29);
+}
diff --git a/crates/dr-math-binding-probe/tests/contract_handoff.rs b/crates/dr-math-binding-probe/tests/contract_handoff.rs
new file mode 100644
index 000000000..ff46aec0e
--- /dev/null
+++ b/crates/dr-math-binding-probe/tests/contract_handoff.rs
@@ -0,0 +1,198 @@
+//! D-DRMC-4: cross-layer *contract* fixture, no proof engine or write path.
+//! No certified-compiler boundary exists for DR64 laws, so the recipe offer
+//! refuses with `NoCertifiedCompiler`; ACT-R arbitration runs on the census
+//! eligibility alone and never on a proof.
+use dr_math_binding_probe::{
+    Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand,
+    Scope, bind_dr64,
+    population::observe_focus,
+    recipe::{
+        Backend, Capability, CompiledReference, LawReference, LawShape, Primitive, RecipeRefusal,
+        admit_recipe,
+    },
+};
+use lance_graph_act_r::{
+    Candidate, Refusal as ArbitrationRefusal, Snapshot, arbitrate, witness_matches,
+};
+use lance_graph_contract::class_view::{ClassId, ClassView, ComputeEdge, compute_dag_topo_order};
+use lance_graph_contract::ontology::{DisplayTemplate, FieldRef};
+
+static COMPUTED_ROLES: [ComputeEdge; 1] = [ComputeEdge {
+    target: 1,
+    inputs: &[0],
+}];
+struct FixtureClass {
+    fields: [FieldRef; 2],
+}
+impl FixtureClass {
+    fn new() -> Self {
+        Self {
+            fields: [
+                FieldRef::new("urn:fixture:memberOf", "memberOf"),
+                FieldRef::new("urn:fixture:effectiveRoles", "effectiveRoles"),
+            ],
+        }
+    }
+}
+impl ClassView for FixtureClass {
+    fn fields(&self, class: ClassId) -> &[FieldRef] {
+        if class == 7 { &self.fields } else { &[] }
+    }
+    fn template(&self, _: ClassId) -> DisplayTemplate {
+        DisplayTemplate::Detail
+    }
+    fn dolce_category_id(&self, _: ClassId) -> u8 {
+        0
+    }
+    fn compute_dag(&self, class: ClassId) -> &[ComputeEdge] {
+        if class == 7 { &COMPUTED_ROLES } else { &[] }
+    }
+}
+const FOCUS: Focus = Focus { revision: 12 };
+const SCOPE: Scope = Scope { id: 13 };
+
+fn signature(method: u16) -> MethodSignature {
+    MethodSignature::presence(
+        7,
+        method,
+        Axis {
+            class: 7,
+            kind: AxisKind::Identity,
+        },
+        Axis {
+            class: 7,
+            kind: AxisKind::Property,
+        },
+    )
+}
+fn store() -> FrameStore {
+    FrameStore::new(FrameRevisions {
+        source: 9,
+        relation_map: 10,
+        coordinates: 11,
+    })
+}
+fn bind<'a>(st: &FrameStore, m: MethodSignature, rows: &'a [u64; 64]) -> BoundDr64<'a> {
+    let at = Guards {
+        frame: st.seal(),
+        focus: FOCUS,
+        scope: SCOPE,
+    };
+    bind_dr64(
+        st,
+        m,
+        m,
+        &at,
+        (FOCUS, SCOPE),
+        Operand {
+            rows,
+            validity: None,
+        },
+    )
+    .unwrap()
+}
+const ABI: u32 = 3;
+fn law() -> LawReference {
+    LawReference {
+        id: 42,
+        revision: 1,
+        shape: LawShape::for_method(signature(1), Primitive::CountViolations),
+    }
+}
+fn compiled(backend: Backend) -> CompiledReference {
+    CompiledReference {
+        law: law(),
+        compiled_digest: [2; 32],
+        compiler_revision: 1,
+        target_abi: ABI,
+        backend,
+    }
+}
+
+#[test]
+fn class_dependency_to_mathematical_offer_to_act_r_proposal_has_no_effect_path() {
+    let view = FixtureClass::new();
+    assert_eq!(compute_dag_topo_order(view.compute_dag(7)), Some(vec![1]));
+    let st = store();
+    // Gamma and R are different bits: R holds the selected pair and one more.
+    let mut selected = [0u64; 64];
+    selected[2] = 1u64 << 17;
+    let mut relation = [0u64; 64];
+    relation[2] = (1u64 << 17) | (1u64 << 18);
+    assert_ne!(selected, relation);
+    let g = bind(&st, signature(2), &selected);
+    let r = bind(&st, signature(1), &relation);
+    let report = observe_focus(&st, &g, &r).unwrap();
+    let checked = report.universal_on_focus().unwrap();
+    assert_eq!(
+        (
+            checked.eligible,
+            checked.true_pairs,
+            checked.false_pairs,
+            checked.unknown_pairs
+        ),
+        (1, 1, 0, 0)
+    );
+
+    // Every metadata check passes; no DR64 certificate can be issued.
+    assert_eq!(
+        admit_recipe(
+            r.clone(),
+            Primitive::CountViolations,
+            law(),
+            compiled(Backend::R2ilMaskRisc),
+            ABI,
+            Capability::PureMathematics,
+        )
+        .unwrap_err(),
+        RecipeRefusal::NoCertifiedCompiler
+    );
+
+    // ACT-R consumes external eligibility only. No action executor or write.
+    // The snapshot version comes from the bound frame, not a second literal.
+    let observed = Snapshot {
+        thought_address: 77,
+        witness_version: r.frame.revisions().source,
+    };
+    let candidate = Candidate {
+        rule_id: 19,
+        eligible: checked.false_pairs == 0,
+        utility: 0.7,
+        activation: 0.4,
+        evaluated_at: observed,
+    };
+    let decision = arbitrate(observed, &[candidate]).unwrap();
+    assert_eq!(decision.rule_id, 19);
+    assert!(witness_matches(&decision, observed));
+
+    let moved = Snapshot {
+        thought_address: 77,
+        witness_version: observed.witness_version + 1,
+    };
+    assert!(matches!(
+        arbitrate(moved, &[candidate]),
+        Err(ArbitrationRefusal::StaleCandidate { rule_id: 19, .. })
+    ));
+}
+
+#[test]
+fn class_declares_a_dependency_not_permission_to_write() {
+    let view = FixtureClass::new();
+    assert_eq!(view.compute_dag(7)[0].inputs, &[0]);
+    let st = store();
+    let mut selected = [0u64; 64];
+    selected[2] = 1u64 << 17;
+    let b = bind(&st, signature(1), &selected);
+    assert_eq!(
+        admit_recipe(
+            b,
+            Primitive::CountViolations,
+            law(),
+            compiled(Backend::ResidentDr64Simd),
+            ABI,
+            Capability::EffectfulAction
+        )
+        .unwrap_err(),
+        RecipeRefusal::EffectRequiresSeparateAuthorization
+    );
+}
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))
+    );
+}
diff --git a/crates/dr-math-binding-probe/tests/recipe.rs b/crates/dr-math-binding-probe/tests/recipe.rs
new file mode 100644
index 000000000..651d1fecc
--- /dev/null
+++ b/crates/dr-math-binding-probe/tests/recipe.rs
@@ -0,0 +1,197 @@
+//! No certified-compiler boundary exists for a Boolean-DR64 law, so every
+//! admission that passes the metadata checks ends in `NoCertifiedCompiler`.
+//! The tests pin that each earlier check refuses on its own, and that nothing
+//! (no flag, no digest, no finite-population report) produces a certificate.
+use dr_math_binding_probe::{
+    Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand,
+    Scope, bind_dr64,
+    recipe::{
+        Backend, Capability, CompiledReference, LawReference, LawShape, Primitive, RecipeRefusal,
+        admit_recipe,
+    },
+};
+
+const FOCUS: Focus = Focus { revision: 4 };
+const SCOPE: Scope = Scope { id: 5 };
+const ABI: u32 = 3;
+
+fn store() -> FrameStore {
+    FrameStore::new(FrameRevisions {
+        source: 1,
+        relation_map: 2,
+        coordinates: 3,
+    })
+}
+/// Non-empty operand, so a test cannot pass only because the register is zero.
+fn rows() -> [u64; 64] {
+    let mut rows = [0u64; 64];
+    rows[3] = (1 << 5) | (1 << 40);
+    rows[60] = 1 << 1;
+    rows
+}
+fn method(class: u16, ordinal: u16, property: bool) -> MethodSignature {
+    let kind = if property {
+        AxisKind::Property
+    } else {
+        AxisKind::Identity
+    };
+    MethodSignature::presence(
+        class,
+        ordinal,
+        Axis {
+            class,
+            kind: AxisKind::Identity,
+        },
+        Axis { class, kind },
+    )
+}
+fn bind<'a>(st: &FrameStore, m: MethodSignature, rows: &'a [u64; 64]) -> BoundDr64<'a> {
+    let at = Guards {
+        frame: st.seal(),
+        focus: FOCUS,
+        scope: SCOPE,
+    };
+    bind_dr64(
+        st,
+        m,
+        m,
+        &at,
+        (FOCUS, SCOPE),
+        Operand {
+            rows,
+            validity: None,
+        },
+    )
+    .unwrap()
+}
+fn law(m: MethodSignature) -> LawReference {
+    LawReference {
+        id: 41,
+        revision: 7,
+        shape: LawShape::for_method(m, Primitive::CountViolations),
+    }
+}
+fn compiled(l: LawReference) -> CompiledReference {
+    CompiledReference {
+        law: l,
+        compiled_digest: [18; 32],
+        compiler_revision: 2,
+        target_abi: ABI,
+        backend: Backend::R2ilMaskRisc,
+    }
+}
+fn admit(
+    st: &FrameStore,
+    m: MethodSignature,
+    l: LawReference,
+    c: CompiledReference,
+    runtime_abi: u32,
+    capability: Capability,
+) -> RecipeRefusal {
+    let r = rows();
+    admit_recipe(
+        bind(st, m, &r),
+        Primitive::CountViolations,
+        l,
+        c,
+        runtime_abi,
+        capability,
+    )
+    .unwrap_err()
+}
+
+/// One law key serves two classes (the key holds no ClassId); both pass every
+/// metadata check and stop at certification, which does not exist for DR64.
+#[test]
+fn one_law_key_spans_two_classes_and_neither_is_certified() {
+    let st = store();
+    let (m1, m2) = (method(1, 2, true), method(22, 8, true));
+    assert_eq!(law(m1), law(m2));
+    assert_ne!(m1.owner_class, m2.owner_class);
+    for m in [m1, m2] {
+        assert_eq!(
+            admit(
+                &st,
+                m,
+                law(m1),
+                compiled(law(m1)),
+                ABI,
+                Capability::PureMathematics
+            ),
+            RecipeRefusal::NoCertifiedCompiler
+        );
+    }
+}
+
+#[test]
+fn same_bytes_but_different_axes_cannot_reuse_law() {
+    let st = store();
+    let l = law(method(1, 2, true));
+    assert_eq!(
+        admit(
+            &st,
+            method(1, 2, false),
+            l,
+            compiled(l),
+            ABI,
+            Capability::PureMathematics
+        ),
+        RecipeRefusal::UnsupportedMathematicalShape
+    );
+}
+
+#[test]
+fn changed_law_revision_or_target_refuses_before_certification() {
+    let st = store();
+    let m = method(1, 2, true);
+    let mut c = compiled(law(m));
+    c.law.revision += 1;
+    assert_eq!(
+        admit(&st, m, law(m), c, ABI, Capability::PureMathematics),
+        RecipeRefusal::LawChanged
+    );
+    assert_eq!(
+        admit(
+            &st,
+            m,
+            law(m),
+            compiled(law(m)),
+            ABI + 1,
+            Capability::PureMathematics
+        ),
+        RecipeRefusal::WrongTarget
+    );
+}
+
+#[test]
+fn missing_code_identity_refuses() {
+    let st = store();
+    let m = method(1, 2, true);
+    for broken in [
+        CompiledReference {
+            compiled_digest: [0; 32],
+            ..compiled(law(m))
+        },
+        CompiledReference {
+            compiler_revision: 0,
+            ..compiled(law(m))
+        },
+    ] {
+        assert_eq!(
+            admit(&st, m, law(m), broken, ABI, Capability::PureMathematics),
+            RecipeRefusal::MissingCodeIdentity
+        );
+    }
+}
+
+#[test]
+fn proof_of_math_never_authorizes_a_cognitive_commit() {
+    let st = store();
+    let m = method(1, 2, true);
+    for kind in [Capability::Proposal, Capability::EffectfulAction] {
+        assert_eq!(
+            admit(&st, m, law(m), compiled(law(m)), ABI, kind),
+            RecipeRefusal::EffectRequiresSeparateAuthorization
+        );
+    }
+}