chore(dr-math): land the stranded D-DRMC stack (#1701-#1704 + charter amendment)

.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.**

.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

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" }

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.