[harvest — do not merge] nal W4 (D-NALP-4): exact truth-law oracle and measurement, kept as a reminder

.claude/board/STATUS_BOARD.md

@@ -93,14 +93,15 @@ Plan: `.claude/plans/nal-polyfill-v1.md`. Template: D-SQLP. No opcode, tenant or
 | **D-NALP-1** | Statement layout + declared ClassView reading; additive `WideFieldMask` projection path on `ClassView`; binder's mask; term width decision | Partial: #1525 merged `08635ed` (NodeGuid reading `nal-statement-v1`, term width u16, aperture selection); ClassView wide projection and binder mask Queued | only the mask's lanes are read; undeclared reading and masked-out field refuse; Small = Wide answers |
 | **D-NALP-2** | Query procedures: select, truth threshold, choice by confidence, support count | Shipped #1525 `08635ed` (`crates/lance-graph-nal`: NodeGuid key, byte apertures; 7 oracle tests, 7 disable runs red; 19–248 ns at 1,048,576 rows); support count and argmax not built | equal to a row-at-a-time oracle; one-pattern threshold disable red; no new opcode |
 | **D-NALP-3** | Revision as `GroupCrossPowerSumsI32` over stored `w`/`f` | Shipped #1538 `4ceaab3` (`nal::Revision`, key = evidence class from the stamps; refuses overlap and missing provenance; 11 tests, 7 disable runs red; ONA's mid-fold saturation is a documented divergence, the fold keeps the exact sum) | equal to exact integer revision; OpenNARS revision points; duplicate evidence counts once |
-| **D-NALP-4** | Per-row truth law into a lane: `MapPairU8` vs fixed-point multiply-high | Queued | insufficiency proof; per-row parity with `isa::truth`, error in codes; one shape also serves SQL nullable arithmetic |
+| **D-NALP-4** | Per-row truth law into a lane: `MapPairU8` vs fixed-point multiply-high | In progress (oracle + shape measured: integer-valued `f64` exact on all 2³² rows of the four laws, the table shape off on 10–18 %; kernel and terminal not built; entry `2026-10-13-d-nalp-4-truth-law-shape.md`) | insufficiency proof; per-row parity with `isa::truth`, error in codes; one shape also serves SQL nullable arithmetic |
 | **D-NALP-5** | Deduction / induction / abduction / analogy over populations | Queued (after D-NALP-4) | equals pairwise scalar rule; abduction direction test red for the reversed statement |
 | **D-NALP-6** | `lance-graph-nal`: typed `nal::{Operation}` surface (`NalOp`), parser (tokens only), binder over the reverse label index, `NAL::narsese()`, typed refusals | Queued | text and typed calls give byte-identical `Program`s; no string in the plan, rows or wire; ambiguous / unknown label refuses; lowers from the bound plan; no fallback; no `Program` outside procedures |
 | **D-NALP-7** | Oracle parity on NAL-1/2 fixtures vs pinned OpenNARS, `jc::reliability` | Queued | within D-HL-4 tolerance per rule |
 | **D-NALP-8** | `ogar-nal` arity table for earned bytes only (OGAR request); after D-NALP-4/5, before D-NALP-6 | Queued | one NAL table in the tree; no byte a procedure can express |
 | **D-NALP-9** | `narsese!{}` declared mode via the D-SQLP-4 generator | Blocked (D-SQLP-4) | generated = interpreted; ≤ 1.05× hand-built; no dispatch in hot loop |
 | **D-NALP-10** | Benchmark, D-SQLP-3 protocol | Queued | answers equal before timing; interpreted ≤ 1.05× hand-built |
 | **D-NALP-11** | One spelling: quack / cypher-quack / Java route through the procedures | Queued | byte-identical `Program`s; Java `ApiSurfaceTest` green |
+| **D-NALP-12** | OGAR Loco → lance-graph R2IL method composition: resolve one OGAR method declaration through a stable method identity and an existing Loco inventory, bind it to a shipped NAL operation (W3 `Revision`), compile through `FoldDialect` into mask-risc, run it over a witnessed belief population | Queued (requested 2026-10-13; starts once W4/W5 have moved far enough). Constraints: `lance-graph-contract` stays dependency-free; no second evaluator, NARS engine or workflow runner; `lance-graph-loco` / `lance-graph-ona` only if each earns its keep | same answer through the typed API as through the OGAR method; missing identity or body, wrong schema/classid/generation, an inventory-local `FnAddr` used as identity, stale scratch across folds, repeated evidence: each refused; OGAR opcode/arity tests and r2sleigh behaviour unchanged; no contract → OGAR edge |
 
 ## D-HL — CE64 hypothesis layers over an immutable address (2026-10-12)
 

.claude/board/entries/2026-10-13-d-nalp-4-truth-law-shape.md

@@ -0,0 +1,37 @@
+# 2026-10-13 — D-NALP-4: which realization of the per-row truth laws is exact (W4)
+
+**Status:** MEASURED (shape exactness); the lane-producing kernel and terminal are OPEN.
+
+**MEASURED:** `cargo run --release --manifest-path crates/lance-graph-nal/Cargo.toml --example w4_truth_law_probe`
+on an AVX-512 host (the probe prints the tier; it is a scalar probe, so it
+measures exactness, not speed). Every input, `(f1, c1, f2, c2)` ∈ 256⁴ = 2³²
+rows per law, against the exact integer law rounded once, half up
+(`crates/lance-graph-nal/tests/common/truth_law.rs`):
+
+| law | table (256² `u8` laws) | `f32`, codes decoded to `x/255` (`isa::truth`) | `f32`, integer-valued | `f64`, integer-valued |
+|---|---|---|---|---|
+| deduction | 419,227,709 rows off | 2,413 | 1,368 | **0** |
+| analogy | 521,640,704 | 512 | 0 | **0** |
+| induction | 775,161,856 | 4,352 | 7,680 | **0** |
+| abduction | 775,161,856 | 4,352 | 7,680 | **0** |
+
+Every miss is one code on the confidence; the frequency never differs.
+
+**What follows:**
+- The table shape (plan §4 C candidate 1, `MapPairU8`) rounds at every stage
+  and misses 10–18 % of all rows. Rejected.
+- `f32` misses a few thousand rows per law, on either encoding.
+- Integer-valued `f64` (products of codes, one division, one rounding) is
+  exact on all 2³² rows of all four laws. It is also the shape that covers
+  the variable division of `w / (w + k)`, which a multiply-high by a constant
+  (§4 C candidate 2) cannot.
+
+**OPEN:**
+- Speed: no SIMD kernel exists yet; `F64x8` has `floor` and `mul_add` but no
+  lane conversion from the `I32` truth lanes. Cost per element is measured on
+  the kernel, not on this scalar probe.
+- The plan's gate "one shape serves SQL nullable arithmetic too" is not met by
+  this measurement: `f64` is exact for `i32` sums and differences, not for
+  every `i32` product (past 2⁵³).
+- Which premise is "1" in induction/abduction is W5's join (ONA swaps the
+  arguments of its `Truth_Induction`); the laws here are two-input laws.

.claude/board/entries/README.md

@@ -25,11 +25,12 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately
 opposite directions; the stranding this convention prevents shows up in
 exactly one of them, never both.
 
-326 entries, 2026-08-06 .. 2026-10-13.
+327 entries, 2026-08-06 .. 2026-10-13.
 
 | date | entry id | finding | file |
 |---|---|---|---|
 | 2026-10-13 | `D-PROD-V4` |  | [2026-10-13-production-targets-v4.md](2026-10-13-production-targets-v4.md) |
+| 2026-10-13 | `D-NALP-4` |  | [2026-10-13-d-nalp-4-truth-law-shape.md](2026-10-13-d-nalp-4-truth-law-shape.md) |
 | 2026-10-12 | `D-SAG-1` |  | [2026-10-12-software-awareness-graph.md](2026-10-12-software-awareness-graph.md) |
 | 2026-10-12 | `D-CMR-RESET` | method layer was a second algebra beside the folds and slower than a row loop (430–480 µs vs 283 µs); moved to backup, rebuild as bindings over existing folds | [2026-10-12-session-reset-inventory.md](2026-10-12-session-reset-inventory.md) |
 | 2026-10-12 | `D-SAG-5-0` | Post-#1509 SAG self-querying, provenance and limited attention with NARS/Hyperon/PLN comparisons; research prompt and high-signal falsifiers | [2026-10-12-sag-reflexive-cognition-research.md](2026-10-12-sag-reflexive-cognition-research.md) |

.claude/plans/nal-polyfill-v1.md

@@ -158,6 +158,13 @@ candidate shapes, chosen by W4's measurement, not here:
    lanes. Fewer table bytes, no per-stage table rounding, and it needs an
    ndarray multiply-high word.
 
+**MEASURED (2026-10-13, W4 probe):** neither candidate as written. Over all
+2³² inputs per law, the table shape misses 10–18 % of rows by one code and
+`f32` misses a few thousand; integer-valued `f64` (products of codes, one
+division, one rounding) is exact on every row of deduction, analogy,
+induction and abduction, and handles the variable division of `w / (w + k)`.
+Entry `2026-10-13-d-nalp-4-truth-law-shape.md`.
+
 Whichever wins, it is solved once for both NAL and SQL nullable arithmetic,
 never twice. The path is: ndarray primitive with parity on every realization
 row → mask-risc terminal with parity → `FoldDialect` wiring → one `ogar-nal`

crates/lance-graph-nal/Cargo.toml

@@ -20,6 +20,10 @@ lance-graph-r2il = { path = "../lance-graph-r2il" }
 # By git `main`, the coordinate `lance-graph-r2il` uses (one `ogar-loco`).
 ogar-loco = { git = "https://github.com/AdaWorldAPI/OGAR", branch = "main" }
 
+[dev-dependencies]
+# The in-tree scalar NARS truth formulas (zero dependencies), the W4 parity reference.
+causal-edge = { path = "../causal-edge" }
+
 [patch."https://github.com/AdaWorldAPI/lance-graph"]
 lance-graph-contract = { path = "../lance-graph-contract" }
 

crates/lance-graph-nal/examples/w4_truth_law_probe.rs

@@ -0,0 +1,189 @@
+//! W4 (D-NALP-4) measurement: how exactly each candidate realization of the
+//! per-row truth laws reproduces the exact law, over EVERY input
+//! (`(f1, c1, f2, c2)` ∈ 256⁴ = 2³² rows per law).
+//!
+//! Shapes measured against `tests/common/truth_law.rs` (exact integers, one
+//! half-up rounding):
+//! - `table`: 256×256 `u8` laws composed, rounding at every stage
+//!   (`mul[a][b] = round(a·b/255)`, `w2c[x] = round(255·x/(x+255))`);
+//! - `f32-dec`: `causal_edge::isa::truth`'s arithmetic, codes decoded to
+//!   `x/255` in `f32`, packed with `(v·255).round()`;
+//! - `f32-int`: the exact integer formula evaluated in `f32` (products of
+//!   codes, one division by the constant, one rounding);
+//! - `f64-int`: the same in `f64`.
+//!
+//! Run: `cargo run --release --example w4_truth_law_probe`.
+
+#[path = "../tests/common/truth_law.rs"]
+mod truth_law;
+
+use std::thread;
+
+type Shape = fn(&str, u8, u8, u8, u8) -> (u8, u8);
+
+fn mul_table() -> Vec<u8> {
+    let mut t = vec![0u8; 256 * 256];
+    for a in 0..256u64 {
+        for b in 0..256u64 {
+            t[(a * 256 + b) as usize] = truth_law::round_div(a * b, 255);
+        }
+    }
+    t
+}
+
+fn w2c_table() -> Vec<u8> {
+    (0..256u64)
+        .map(|x| truth_law::round_div(255 * x, x + 255))
+        .collect()
+}
+
+thread_local! {
+    static MUL: Vec<u8> = mul_table();
+    static W2C: Vec<u8> = w2c_table();
+}
+
+fn table(name: &str, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) {
+    MUL.with(|m| {
+        W2C.with(|w| {
+            let mul = |a: u8, b: u8| m[usize::from(a) * 256 + usize::from(b)];
+            match name {
+                "deduction" => {
+                    let f = mul(f1, f2);
+                    (f, mul(f, mul(c1, c2)))
+                }
+                "analogy" => (mul(f1, f2), mul(mul(c1, c2), f2)),
+                "induction" => (f2, w[usize::from(mul(mul(f1, c1), c2))]),
+                "abduction" => (f1, w[usize::from(mul(mul(f2, c1), c2))]),
+                _ => unreachable!(),
+            }
+        })
+    })
+}
+
+fn pack(v: f32) -> u8 {
+    (v.clamp(0.0, 1.0) * 255.0).round() as u8
+}
+
+fn f32_dec(name: &str, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) {
+    use causal_edge::isa::truth;
+    let d = |x: u8| f32::from(x) / 255.0;
+    let (f, c) = match name {
+        "deduction" => truth::deduction(d(f1), d(c1), d(f2), d(c2)),
+        "induction" => truth::induction(d(f1), d(c1), d(f2), d(c2)),
+        "abduction" => truth::abduction(d(f1), d(c1), d(f2), d(c2)),
+        "analogy" => (d(f1) * d(f2), d(c1) * d(c2) * d(f2)),
+        _ => unreachable!(),
+    };
+    (pack(f), pack(c))
+}
+
+macro_rules! int_shape {
+    ($fname:ident, $t:ty) => {
+        fn $fname(name: &str, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) {
+            let x = |v: u8| <$t>::from(v);
+            let r = |p: $t, q: $t| (p / q + 0.5).floor() as u8;
+            let (k1, k2, k3): ($t, $t, $t) = (255.0, 65025.0, 16581375.0);
+            match name {
+                "deduction" => {
+                    let ff = x(f1) * x(f2);
+                    (r(ff, k1), r(ff * x(c1) * x(c2), k3))
+                }
+                "analogy" => (r(x(f1) * x(f2), k1), r(x(c1) * x(c2) * x(f2), k2)),
+                "induction" => {
+                    let w = x(f1) * x(c1) * x(c2);
+                    (f2, r(255.0 * w, w + k3))
+                }
+                "abduction" => {
+                    let w = x(f2) * x(c1) * x(c2);
+                    (f1, r(255.0 * w, w + k3))
+                }
+                _ => unreachable!(),
+            }
+        }
+    };
+}
+int_shape!(f32_int, f32);
+int_shape!(f64_int, f64);
+
+const SHAPES: [(&str, Shape); 4] = [
+    ("table", table),
+    ("f32-dec", f32_dec),
+    ("f32-int", f32_int),
+    ("f64-int", f64_int),
+];
+
+#[derive(Default, Clone, Copy)]
+struct Tally {
+    rows_off: u64,
+    max_df: u8,
+    max_dc: u8,
+}
+
+fn measure(name: &'static str, law: truth_law::Law) -> [Tally; 4] {
+    let threads = 4u16;
+    let parts: Vec<[Tally; 4]> = thread::scope(|s| {
+        (0..threads)
+            .map(|t| {
+                s.spawn(move || {
+                    let mut tally = [Tally::default(); 4];
+                    let mut f1 = t;
+                    while f1 < 256 {
+                        let f1b = f1 as u8;
+                        for c1 in 0..=255u8 {
+                            for f2 in 0..=255u8 {
+                                for c2 in 0..=255u8 {
+                                    let (ef, ec) = law(f1b, c1, f2, c2);
+                                    for (i, (_, shape)) in SHAPES.iter().enumerate() {
+                                        let (sf, sc) = shape(name, f1b, c1, f2, c2);
+                                        let df = ef.abs_diff(sf);
+                                        let dc = ec.abs_diff(sc);
+                                        let tl = &mut tally[i];
+                                        tl.rows_off += u64::from(df != 0 || dc != 0);
+                                        tl.max_df = tl.max_df.max(df);
+                                        tl.max_dc = tl.max_dc.max(dc);
+                                    }
+                                }
+                            }
+                        }
+                        f1 += threads;
+                    }
+                    tally
+                })
+            })
+            .collect::<Vec<_>>()
+            .into_iter()
+            .map(|h| h.join().expect("worker"))
+            .collect()
+    });
+    let mut out = [Tally::default(); 4];
+    for p in parts {
+        for i in 0..4 {
+            out[i].rows_off += p[i].rows_off;
+            out[i].max_df = out[i].max_df.max(p[i].max_df);
+            out[i].max_dc = out[i].max_dc.max(p[i].max_dc);
+        }
+    }
+    out
+}
+
+fn main() {
+    println!(
+        "tier: avx512f={} avx2={} (scalar probe; exactness, not speed)",
+        cfg!(target_feature = "avx512f"),
+        cfg!(target_feature = "avx2")
+    );
+    println!("rows per law: 2^32 = {}", 1u64 << 32);
+    println!(
+        "{:<10} {:<8} {:>14} {:>8} {:>8}",
+        "law", "shape", "rows off", "max df", "max dc"
+    );
+    for (name, law) in truth_law::LAWS {
+        let t = measure(name, law);
+        for (i, (shape, _)) in SHAPES.iter().enumerate() {
+            println!(
+                "{:<10} {:<8} {:>14} {:>8} {:>8}",
+                name, shape, t[i].rows_off, t[i].max_df, t[i].max_dc
+            );
+        }
+    }
+}

crates/lance-graph-nal/tests/common/mod.rs

@@ -0,0 +1,3 @@
+//! Test oracles shared by the integration tests and the W4 probe.
+
+pub mod truth_law;

crates/lance-graph-nal/tests/common/truth_law.rs

@@ -0,0 +1,72 @@
+//! The exact per-row NAL truth laws over `u8` codes (W4 oracle).
+//!
+//! A code `x` stands for the value `x / 255`. Each law is computed in exact
+//! integer arithmetic and rounded ONCE, half up, back into a code — the one
+//! rounding `causal_edge::isa::truth` performs when it packs (`(v *
+//! 255).round()`), without its intermediate `f32` rounding. This is the
+//! contract a lane-producing realization must meet; it is test code, never a
+//! production path (the production law runs in mask-risc).
+//!
+//! Formulas (horizon `k = 1`, `causal_edge::isa::truth` and the planner's
+//! `TruthValue`):
+//! - deduction: `f = f1·f2`, `c = f1·f2·c1·c2`;
+//! - analogy: `f = f1·f2`, `c = c1·c2·f2`;
+//! - induction: `f = f2`, `c = w / (w + 1)`, `w = f1·c1·c2`;
+//! - abduction: `f = f1`, `c = w / (w + 1)`, `w = f2·c1·c2`.
+//!
+//! Which premise is "1" and which is "2" is the syllogism's business (W5);
+//! these are two-input laws.
+
+#![allow(dead_code)]
+
+/// `round(p / q)`, half up, for `p ≥ 0`, `q > 0`.
+pub fn round_div(p: u64, q: u64) -> u8 {
+    let r = (2 * p + q) / (2 * q);
+    u8::try_from(r).expect("a law value lies in [0, 1]")
+}
+
+const K1: u64 = 255;
+const K2: u64 = 255 * 255;
+const K3: u64 = 255 * 255 * 255;
+
+fn w2c(w_num: u64) -> u8 {
+    // w = w_num / 255³, c = w / (w + 1) = w_num / (w_num + 255³), code = 255·c.
+    round_div(255 * w_num, w_num + K3)
+}
+
+/// `(f, c)` codes of deduction.
+pub fn deduction(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) {
+    let ff = u64::from(f1) * u64::from(f2);
+    (
+        round_div(ff, K1),
+        round_div(ff * u64::from(c1) * u64::from(c2), K3),
+    )
+}
+
+/// `(f, c)` codes of analogy.
+pub fn analogy(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) {
+    let ff = u64::from(f1) * u64::from(f2);
+    let c = u64::from(c1) * u64::from(c2) * u64::from(f2);
+    (round_div(ff, K1), round_div(c, K2))
+}
+
+/// `(f, c)` codes of induction.
+pub fn induction(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) {
+    (f2, w2c(u64::from(f1) * u64::from(c1) * u64::from(c2)))
+}
+
+/// `(f, c)` codes of abduction.
+pub fn abduction(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) {
+    (f1, w2c(u64::from(f2) * u64::from(c1) * u64::from(c2)))
+}
+
+/// A rule, for iteration.
+pub type Law = fn(u8, u8, u8, u8) -> (u8, u8);
+
+/// The four NAL-1 laws by name.
+pub const LAWS: [(&str, Law); 4] = [
+    ("deduction", deduction),
+    ("analogy", analogy),
+    ("induction", induction),
+    ("abduction", abduction),
+];