From d603e7429aa60b166db10ad70bb73c9ed4f5c4b0 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 23 Aug 2026 18:00:30 +0000 Subject: [PATCH 1/2] probes: signed G24N4 Tarski witness + four-plane causal medium PROBE-TARSKI-SIGNED-WITNESS-1 (probe_tarski_signed_witness.rs): tests whether Belief::rung is an impoverished projection of a signed derivational field. Reads the SAME shipped G24N4 register (CausalWitnessFacet, causal_witness.rs) through a probe-local ClassView: SupportedBy = +constructive depth, Contradiction = -falsifying depth, per the operator's "loci, not magnitudes, sign = orientation" law already locked for A9. Not a new tenant, not a mint. 10/10 gates green: - A1-A3: authored rung fixture; legacy support_ceiling() projection reproduces Belief::rung exactly on a positive-only corpus; dock round-trips byte-identical through both the FacetCascade and G24N4 readings of the same bytes. - B1: a falsifying counter-derivation is PROVABLY INVISIBLE to BeliefArena's scalar state -- the shipped admit_derived CHOICE law (belief.rs:247, strict-expectation-gain only) silently drops it. The witness field retains it without disturbing the support lane. - B2-B3: falsifier lands in Contradiction only (support lane untouched); hotspot detection (support>0 AND falsifier>0) fires exactly at the apex, nowhere else. - B4: two falsifier depths (2 vs 3 hops) are scalar-IDENTICAL in the arena (zero bits of depth survive) but the witness distinguishes them -- the discrimination the scalar cannot make. - C1: falsifier removed -> docks return byte-identical to the positive fixture. - P1-P2: i4 ceiling stated honestly (clamps +7/-8, does not widen); masked election is fail-closed and discriminating. Also documents (not asserted, discovered mid-build): close_transitive's per-pass `derived: HashMap` iteration order makes premise indices AND tie-broken derivation routes nondeterministic across identical builds -- corroborating BELIEF-ABI-RESTORATION-1 F4 (ephemeral index leaking into cognitive state) independently of the Step-1 audit. PROBE-FOUR-PLANE-CAUSAL-MEDIUM-1 (probe_four_plane_causal_medium.rs): tests the operator's four-plane separation -- HHTL/attention (WHERE), CausalEdge64 topology bits 59-60 (WHAT), CausalEdge64 reasoning band bits 61-63 (WHICH LENS), signed G24N4 witness (WHY), and an R2IL-shaped typed intervention row (WHAT WE DID) -- over one toy causal chain with a hidden mediator. 7/7 gates green: the four planes read independently (FP1), a write to one lane never touches another (FP2), a falsifier in the evidence plane does NOT auto-flip CausalTopology or ReasoningBand (FP3, the operator's explicit non-negotiable), a scoped epistemic- pothole query discriminates (FP4), a wrong-mediator intervention leaves every other plane untouched (FP5), the true-mediator intervention closes the loop -- binds the Kausal locus, upgrades IndirectUnknownIntermediates to IndirectKnownIntermediates, and leaves the support/band/address lanes bit-identical (FP6) -- and every lane round-trips through its own fixed-width LE register (FP7). Explicitly scoped as representation-loop probes, not causal discovery: the "world" is a known 3-event oracle. Whether this geometry helps DISCOVER structure that predicts unseen interventions is the external falsifier (Uhler-style causal representation learning), out of scope here. Both probe-local classids (0xFFFF_000A/B) are placeholders, not OGAR mints; nothing here canonizes on them, per BELIEF-ABI-RESTORATION-1's bounds. Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_01KCGhDYoQBXs3poaR7sFuqp --- .../probe_four_plane_causal_medium.rs | 346 +++++++++++++ .../examples/probe_tarski_signed_witness.rs | 473 ++++++++++++++++++ 2 files changed, 819 insertions(+) create mode 100644 crates/lance-graph-planner/examples/probe_four_plane_causal_medium.rs create mode 100644 crates/lance-graph-planner/examples/probe_tarski_signed_witness.rs diff --git a/crates/lance-graph-planner/examples/probe_four_plane_causal_medium.rs b/crates/lance-graph-planner/examples/probe_four_plane_causal_medium.rs new file mode 100644 index 000000000..d40500217 --- /dev/null +++ b/crates/lance-graph-planner/examples/probe_four_plane_causal_medium.rs @@ -0,0 +1,346 @@ +//! PROBE-FOUR-PLANE-CAUSAL-MEDIUM-1 — one tiny causal chain with a hidden +//! mediator, one supporting derivation, one falsifying intervention: do the +//! FOUR planes stay distinguishable while sharing the memory ABI? +//! +//! **The four-plane convergence under test (operator, 2026-08-23):** +//! +//! ```text +//! HHTL / Attention V3 WHERE is relevant? AttentionFocusFacet scope +//! CausalEdge64 59..60 WHAT causal topology? CausalTopology (Direct / +//! IndirectKnown / IndirectUnknown / Unknown) +//! CausalEdge64 61..63 THROUGH WHAT lens? ReasoningBand (Surface..Transcendent) +//! Tarski G24N4 WHY supportable? +n support / 0 unresolved / −n falsifier +//! R2IL V4 WHAT did we DO? typed intervention row + observed consequence +//! ``` +//! +//! Held separate on purpose: a negative G24N4 nibble must NOT auto-flip +//! `ReasoningBand` to `Counterfactual` or rewrite `CausalTopology` — the +//! planes are jointly readable, never derived from one another. The target +//! sentence the composed state must express (no scalar confidence can): +//! +//! > "Inside this region, an indirect causal relation is hypothesized, its +//! > constructive derivation reaches +2, a −1 falsifier exists against a +//! > wrong mediator, and the mediator locus is still epistemically empty." +//! +//! …and then the closed experimental loop: a typed intervention on the true +//! mediator BINDS the mediator locus, upgrades the topology register +//! `IndirectUnknownIntermediates → IndirectKnownIntermediates`, and leaves +//! the support lane untouched. +//! +//! # Honesty box +//! +//! - The "world" here is a toy oracle (a known 3-event chain `A → M → B`). +//! The probe tests the ABI REPRESENTATION loop — four planes resident, +//! distinguishable, updatable — not causal discovery. Whether this +//! geometry helps discover structure that predicts unseen interventions +//! is the EXTERNAL falsifier (Uhler-style CRL), out of scope here. +//! - Probe-local classids only; the V4 classid is provisional (O5 gate) — +//! nothing canonizes. The V4 plane is an R2IL-SHAPED typed row (16-byte +//! LE, `Copy`, no heap), not the real `ruff_r2il` producer. +//! - Bits 59-60 carry two shipped readings (`TrustTexture` vs +//! `CausalTopology`); which one a producer wrote is the `band_reading` +//! contract's declared knowledge. This probe writes through the topology +//! lens by construction and says so — a production writer would declare +//! it per `(classid, rail)`. +//! - `CausalWitnessFacet`'s A9 reading is operator-locked "loci, not +//! magnitudes." This probe's ClassView reads THREE loci with per-locus +//! semantics (the ClassView defines what a sign means per locus): +//! `SupportedBy`/`Contradiction` as signed derivational DEPTH (the Tarski +//! reading, PROBE-TARSKI-SIGNED-WITNESS-1), `Kausal` as a signed stream +//! POINTER to the located mediator (the shipped A9 pointer semantics). + +use causal_edge::layout::{CausalTopology, ReasoningBand}; +use causal_edge::CausalEdge64; +use lance_graph_contract::attention_facet::AttentionFocusFacet; +use lance_graph_contract::causal_witness::{CausalWitnessFacet, Locus, WITNESS_REGISTER_BYTES}; +use lance_graph_contract::facet::{FacetCascade, FacetTier}; + +/// Probe-local classid for causal-hypothesis rows (NOT a mint). +const HYPOTHESIS_CLASSID: u32 = 0xFFFF_000A; +/// Probe-local classid for V4-plane intervention rows (NOT a mint; the real +/// V4 classid is provisional behind the O5 gate). +const INTERVENTION_CLASSID: u32 = 0xFFFF_000B; + +/// One resident causal-hypothesis row: four planes, four disjoint lanes of +/// ONE `Copy` row. No heap, no hash, no materialized mask. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +struct CausalRow { + /// Plane 1 — WHERE: the 16-byte address dock (classid + G6D2 cascade). + /// Attention/HHTL read THIS lane; evidence updates never touch it. + address: [u8; 16], + /// Planes 2+3 — WHAT + LENS: the causal relation register + /// (topology bits 59-60, reasoning band bits 61-63). + edge: CausalEdge64, + /// Plane 4 (evidence) — WHY: the 12-byte G24N4 signed witness register. + evidence: [u8; WITNESS_REGISTER_BYTES], +} + +/// One V4-plane row: a typed intervention particle, R2IL-shaped +/// (16-byte LE dock: classid(4) | kind(1) | target_offset(i8 as 1) | +/// observed(1) | reserved(9)). `Copy`, no heap — behavior as an ADDRESSED +/// ROW, never nested state. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +struct InterventionRow([u8; 16]); + +const KIND_KNOCKOUT: u8 = 1; +const OBS_NONE: u8 = 0; +const OBS_LINK_BROKEN: u8 = 1; +const OBS_LINK_INTACT: u8 = 2; + +impl InterventionRow { + fn knockout(target_offset: i8) -> Self { + let mut b = [0u8; 16]; + b[0..4].copy_from_slice(&INTERVENTION_CLASSID.to_le_bytes()); + b[4] = KIND_KNOCKOUT; + b[5] = target_offset as u8; + b[6] = OBS_NONE; + Self(b) + } + fn with_observed(mut self, obs: u8) -> Self { + self.0[6] = obs; + self + } + fn target_offset(&self) -> i8 { + self.0[5] as i8 + } + fn observed(&self) -> u8 { + self.0[6] + } + fn classid(&self) -> u32 { + u32::from_le_bytes([self.0[0], self.0[1], self.0[2], self.0[3]]) + } +} + +/// The toy world oracle: the event stream `[A, M, B]`, with M the hidden +/// mediator of A→B. `do(knockout at offset)` reports whether A→B survives. +/// Deterministic and admittedly trivial — see the honesty box. +fn world_do_knockout(target_offset_from_edge: i8) -> u8 { + // The edge row sits conceptually AT B (offset 0); M is one back (−1), + // A two back (−2). Knocking out the true mediator breaks the link. + if target_offset_from_edge == -1 { + OBS_LINK_BROKEN + } else { + OBS_LINK_INTACT + } +} + +fn witness_of(reg: &[u8; WITNESS_REGISTER_BYTES]) -> &CausalWitnessFacet { + CausalWitnessFacet::from_register_ref(reg) +} + +fn set_locus(reg: &mut [u8; WITNESS_REGISTER_BYTES], locus: Locus, v: i8) { + let mut w = *witness_of(reg); + w.set(locus as usize, v); + *reg = w.to_register(); +} + +/// Build an address dock in region `heel` (tier-0 coarse byte). +fn address_in_region(heel: u8, ident: u8) -> [u8; 16] { + let fc = FacetCascade { + facet_classid: HYPOTHESIS_CLASSID, + tiers: [ + FacetTier { hi: heel, lo: 0x01 }, + FacetTier { hi: 0, lo: 0 }, + FacetTier { hi: 0, lo: 0 }, + FacetTier { hi: 0, lo: 0 }, + FacetTier { hi: 0, lo: 0 }, + FacetTier { hi: 0, lo: ident }, + ], + }; + fc.to_bytes() +} + +fn focus_of(row: &CausalRow) -> AttentionFocusFacet { + AttentionFocusFacet::exact(FacetCascade::from_bytes(&row.address)) +} + +fn main() { + let mut pass = 0u32; + let mut gate = |name: &str, ok: bool, detail: String| { + assert!(ok, "[FAIL] {name} — {detail}"); + println!(" [PASS] {name} — {detail}"); + pass += 1; + }; + + // ---- Compose the initial state: the hypothesis, pre-intervention ---- + // "Inside region 0x11, A→B is hypothesized indirect-with-unknown- + // intermediates, read at the Causal band, constructive support +2, + // falsifier −1 (a wrong-mediator candidate already refuted), + // mediator locus 0 (the epistemic pothole)." + let mut evidence = [0u8; WITNESS_REGISTER_BYTES]; + set_locus(&mut evidence, Locus::SupportedBy, 2); + set_locus(&mut evidence, Locus::Contradiction, -1); + // Locus::Kausal deliberately left 0 — the mediator pothole. + + let mut row = CausalRow { + address: address_in_region(0x11, 0x01), + edge: CausalEdge64::ZERO + .with_topology(CausalTopology::IndirectUnknownIntermediates) + .with_reasoning_band(ReasoningBand::Causal), + evidence, + }; + // A sibling row in ANOTHER region — the scope must exclude it. + let outside = CausalRow { + address: address_in_region(0x22, 0x02), + edge: CausalEdge64::ZERO.with_topology(CausalTopology::Direct), + evidence: [0u8; WITNESS_REGISTER_BYTES], + }; + + // Plane 1 — WHERE: a depth-1 scope over region 0x11 (tier-0 hi byte). + let scope = AttentionFocusFacet::prefix( + FacetCascade::from_bytes(&address_in_region(0x11, 0x00)), + 1, + ) + .expect("depth 1 <= 12"); + + // FP1 — all four planes readable, each answering ITS question. + let w = witness_of(&row.evidence); + gate( + "FP1 four planes independently readable", + scope.covers(focus_of(&row)) + && !scope.covers(focus_of(&outside)) + && row.edge.topology() == CausalTopology::IndirectUnknownIntermediates + && row.edge.reasoning_band() == ReasoningBand::Causal + && w.at(Locus::SupportedBy) == 2 + && w.at(Locus::Contradiction) == -1 + && !w.is_bound(Locus::Kausal), + "WHERE covers row/excludes sibling; WHAT=IndirectUnknown; LENS=Causal; \ + WHY=+2/−1/mediator-pothole" + .to_string(), + ); + + // FP2 — plane isolation: writing one plane's lane changes ONLY that + // lane (field-isolation across planes, I-LEGACY-API-FEATURE-GATED + // discipline applied at the row level). + { + let before = row; + let mut t = row; + set_locus(&mut t.evidence, Locus::Contradiction, -3); + let ev_only = t.address == before.address && t.edge == before.edge; + let mut t2 = row; + t2.edge = t2.edge.with_topology(CausalTopology::Unknown); + let edge_only = t2.address == before.address && t2.evidence == before.evidence; + let mut t3 = row; + t3.address = address_in_region(0x11, 0x7F); + let addr_only = t3.edge == before.edge && t3.evidence == before.evidence; + gate( + "FP2 plane isolation (each write confined to its lane)", + ev_only && edge_only && addr_only, + "evidence/edge/address writes each leave the other two lanes bit-identical" + .to_string(), + ); + } + + // FP3 — NO AUTO-FLIP: a falsifier landing in the evidence plane must + // not rewrite the causal registers. Jointly readable, never derived. + { + let edge_before = row.edge; + let mut t = row; + set_locus(&mut t.evidence, Locus::Contradiction, -8); + gate( + "FP3 negative evidence does NOT flip band or topology", + t.edge == edge_before + && t.edge.reasoning_band() == ReasoningBand::Causal + && t.edge.topology() == CausalTopology::IndirectUnknownIntermediates, + "Contradiction −8 written; CE64 bit-identical (band Causal, topology unchanged)" + .to_string(), + ); + } + + // FP4 — the epistemic-pothole query: bound support + unbound mediator, + // scoped by the WHERE plane. Discriminating: fires on the hypothesis + // row, silent on the out-of-scope row (which is also unbound). + let pothole = |r: &CausalRow| -> bool { + scope.covers(focus_of(r)) + && witness_of(&r.evidence).at(Locus::SupportedBy) > 0 + && !witness_of(&r.evidence).is_bound(Locus::Kausal) + }; + gate( + "FP4 pothole query (support present, mediator locus empty) is scoped", + pothole(&row) && !pothole(&outside), + "fires inside the scope where support exists and the mediator is unknown".to_string(), + ); + + // ---- The closed loop: hypothesis → intervention → consequence → update ---- + + // FP5 — falsifying intervention first: knock out a WRONG mediator + // candidate (offset −2 = A itself is not a mediator between A and B; + // use a non-mediator probe target). The link survives; the falsifier + // depth-1 evidence −1 was already resident; crucially the CE64 and the + // support lane are UNTOUCHED by a failed mediation test. + let wrong = InterventionRow::knockout(-2); + let wrong = wrong.with_observed(world_do_knockout(wrong.target_offset())); + let row_before_wrong = row; + // A LinkIntact consequence does not bind the mediator locus. + gate( + "FP5 falsifying intervention leaves WHAT/WHY-support/WHERE untouched", + wrong.observed() == OBS_LINK_INTACT + && wrong.classid() == INTERVENTION_CLASSID + && row == row_before_wrong, + format!( + "do(knockout@{:+}) → LinkIntact recorded in the V4 row; hypothesis row bit-identical", + wrong.target_offset() + ), + ); + + // FP6 — supporting intervention: knock out the TRUE mediator (−1). + // The consequence LinkBroken (a) binds the mediator locus to the + // intervention's own typed target, (b) upgrades the topology register + // IndirectUnknown → IndirectKnown, (c) leaves the support lane and the + // reasoning band untouched, (d) leaves the address lane untouched. + let probe_m = InterventionRow::knockout(-1); + let probe_m = probe_m.with_observed(world_do_knockout(probe_m.target_offset())); + let (addr_before, band_before, support_before) = ( + row.address, + row.edge.reasoning_band(), + witness_of(&row.evidence).at(Locus::SupportedBy), + ); + if probe_m.observed() == OBS_LINK_BROKEN { + set_locus(&mut row.evidence, Locus::Kausal, probe_m.target_offset()); + row.edge = row.edge.with_topology(CausalTopology::IndirectKnownIntermediates); + } + let w = witness_of(&row.evidence); + gate( + "FP6 supporting intervention closes the loop (pothole → known mediator)", + w.at(Locus::Kausal) == -1 + && row.edge.topology() == CausalTopology::IndirectKnownIntermediates + && row.edge.reasoning_band() == band_before + && w.at(Locus::SupportedBy) == support_before + && w.at(Locus::Contradiction) == -1 + && row.address == addr_before + && !pothole(&row), + "Kausal bound −1; topology Unknown→Known intermediates; band/support/falsifier/address \ + unchanged; pothole query now silent" + .to_string(), + ); + + // FP7 — physical conservation: every plane row is a fixed-width LE + // register (16B dock / u64 / 12B G24N4 / 16B V4 row); round-trips are + // byte-exact; no plane materializes another's content. + // CausalRow's own size is a probe-local composite (Rust struct layout + // may insert padding between the three lane fields) — NOT itself a + // dock; each LANE's width is what the ABI actually const-asserts. + const _: () = assert!(core::mem::size_of::<[u8; 16]>() == 16, "address lane is one dock"); + const _: () = assert!( + core::mem::size_of::<[u8; WITNESS_REGISTER_BYTES]>() == 12, + "evidence lane is the G24N4 register" + ); + const _: () = assert!(core::mem::size_of::() == 16, "V4 row is one dock"); + const _: () = assert!(core::mem::size_of::() == 8, "CE64 is one u64"); + let fc = FacetCascade::from_bytes(&row.address); + gate( + "FP7 shared-ABI conservation (fixed LE registers, byte-exact round-trips)", + fc.to_bytes() == row.address + && fc.facet_classid == HYPOTHESIS_CLASSID + && witness_of(&row.evidence).to_register() == row.evidence, + "address round-trips through FacetCascade; evidence through G24N4; sizes const-asserted" + .to_string(), + ); + + println!("PROBE-FOUR-PLANE-CAUSAL-MEDIUM-1: ALL {pass} GATES GREEN"); + println!( + "verdict: WHERE (scope) / WHAT (topology) / LENS (band) / WHY (signed witness) / \ + DID (typed intervention) compose as disjoint lanes of resident rows; the falsifier \ + and the intervention each land in their own plane and nothing auto-flips" + ); +} diff --git a/crates/lance-graph-planner/examples/probe_tarski_signed_witness.rs b/crates/lance-graph-planner/examples/probe_tarski_signed_witness.rs new file mode 100644 index 000000000..9b61e61fc --- /dev/null +++ b/crates/lance-graph-planner/examples/probe_tarski_signed_witness.rs @@ -0,0 +1,473 @@ +//! PROBE-TARSKI-SIGNED-WITNESS-1 — is `Belief::rung` an impoverished +//! projection of a signed derivational field? +//! +//! **The claim under test (operator, 2026-08-23).** The scalar Tarski rung +//! (`Belief::rung: u32`) answers only "how far did the successful proof +//! climb?" A `24×i4` signed witness field over the SAME 16-byte dock +//! (`classid(4) + 12-byte register`) could answer "where did the proof climb, +//! where did it fail, and where does a counter-proof bite?" — with +//! `+n` = constructive derivation depth, `-n` = falsifying derivation depth, +//! `0` = absent/unresolved, per locus. +//! +//! **This is a probe-local ClassView READING, not a new tenant and not a +//! mint.** The physical carrier is the shipped `G24N4` nibble law +//! ([`CausalWitnessFacet`], `causal_witness.rs`) over the shipped 16-byte +//! dock ([`FacetCascade`]). The shipped A9 reading is operator-locked +//! "loci, not magnitudes" — THIS reading (sign = support vs falsification, +//! magnitude = derivational depth) is a DIFFERENT ClassView over the same +//! bytes, exactly as the "one register, three readings" doctrine (PR #729) +//! provides. The probe-local classid below is a placeholder, NOT an OGAR +//! mint; nothing here canonizes. +//! +//! **⚠ MEMORY-ABI ESCAPE, acknowledged in place.** `BeliefArena` remains the +//! acknowledged non-canonical AoS owner (#1004, +//! `E-TYPE-COMPLEXITY-EXPOSED-A-MEMORY-ABI-ESCAPE-1`); this probe uses it as +//! the PARITY ORACLE only. The witness docks are a fixed stack array of +//! 16-byte Copy rows — no heap row population, no hash, no materialized +//! mask, no new backing store beyond the dock rows themselves. This probe +//! informs the `BELIEF-ABI-RESTORATION-1` charter's step-2 ruling on `rung`; +//! it does NOT execute the charter's step 3. +//! +//! # Fixtures (all gates must be able to fail) +//! +//! - **A** — ordinary positive derivation chain, no falsifier. The G24N4 +//! positive support projection must reproduce `Belief::rung` exactly. +//! - **B** — same chain plus a freq-0 falsifying counter-chain reaching the +//! apex statement S. The shipped merge law (`admit_derived` CHOICE, +//! `belief.rs:247`: a pure-derived candidate replaces only on STRICT +//! expectation gain) silently DROPS the counter-derivation — so the +//! arena's scalar state at S is bit-identical to fixture A. The witness +//! field alone retains the falsifier, without disturbing the support lane. +//! - **B'** — a DEEPER falsifying counter-chain. The arena's scalar state at +//! S is provably identical between B and B' (zero bits of falsifier depth +//! survive); the witness distinguishes them. +//! - **C** — falsifier removed. The witness register returns byte-identical +//! to fixture A: the negative lane vanishes, the positive lane is exact. +//! +//! Physical conservation gates: same 16-byte dock, same LE geometry, G24N4 +//! reading only, borrowed zero-copy register views, i4 ceiling stated +//! honestly (+7/−8 — derivations deeper than rung 7 need escalation, not a +//! wider nibble). + +use lance_graph_contract::causal_witness::{CausalWitnessFacet, Locus, WITNESS_REGISTER_BYTES}; +use lance_graph_contract::class_view::WideFieldMask; +use lance_graph_contract::facet::FacetCascade; +use lance_graph_planner::nars::belief::{BeliefArena, Belief, CStmt, Copula, Stamp}; +use lance_graph_planner::nars::truth::TruthValue; + +/// Probe-local ClassView id for the Tarski signed-witness READING. +/// Deliberately in a nonsense range: this is NOT an OGAR mint. +const PROBE_TARSKI_CLASSID: u32 = 0xFFFF_0009; + +/// Dock capacity — fixed stack array, no heap row population. +const MAX_DOCKS: usize = 64; + +/// One 16-byte dock row: `classid(4, LE) | 24×i4 register(12)`. +type Dock = [u8; 16]; + +const _: () = assert!(core::mem::size_of::() == 16, "16-byte dock"); +const _: () = assert!( + core::mem::size_of::() == WITNESS_REGISTER_BYTES, + "G24N4 register is the dock payload width" +); +const _: () = assert!( + core::mem::size_of::() == 16, + "FacetCascade shares the dock width" +); + +const EMPTY_DOCK: Dock = [0u8; 16]; + +/// Borrowed zero-copy G24N4 view of a dock's 12-byte payload +/// (`CausalWitnessFacet::from_register_ref` — a pointer reborrow, no copy). +fn witness_of(dock: &Dock) -> &CausalWitnessFacet { + let reg: &[u8; WITNESS_REGISTER_BYTES] = dock[4..16].try_into().expect("12-byte payload"); + CausalWitnessFacet::from_register_ref(reg) +} + +/// Write-back path per the borrow-strategy law: owned Copy microcopy of the +/// 12-byte register, nibble edit, gated write-back. Never `&mut` a view. +fn set_locus(dock: &mut Dock, locus: Locus, offset: i8) { + let mut w = *witness_of(dock); + w.set(locus as usize, offset); + dock[4..16].copy_from_slice(&w.to_register()); +} + +fn mint_dock() -> Dock { + let mut d = EMPTY_DOCK; + d[0..4].copy_from_slice(&PROBE_TARSKI_CLASSID.to_le_bytes()); + d +} + +/// The legacy projection: `support_ceiling = max(positive loci)`. +/// For the positive-only corpus this must equal `Belief::rung` exactly +/// (observed ground = rung 0 = no bound positive locus). +fn support_ceiling(w: &CausalWitnessFacet) -> u32 { + (0..24).map(|s| w.get(s).max(0) as u32).max().unwrap_or(0) +} + +/// `falsifier_ceiling = max(abs(negative loci))`. +fn falsifier_ceiling(w: &CausalWitnessFacet) -> u32 { + (0..24).map(|s| (-w.get(s)).max(0) as u32).max().unwrap_or(0) +} + +fn inh(s: u16, p: u16) -> CStmt { + CStmt { + s, + cop: Copula::Inh, + p, + } +} + +/// Scan the closed arena for falsifying derivations the scalar path DROPPED: +/// composable premise pairs whose candidate conclusion targets an existing +/// belief of opposing polarity (stored expectation > 0.5, candidate ≤ 0.5). +/// Returns, per target statement, the DEEPEST such counter-derivation +/// (`max(r1, r2) + 1` — the same depth law `close_transitive` uses). +/// +/// This is the "falsifier listener": it re-derives with the arena's own +/// public truth functions what `admit_derived`'s CHOICE discards silently. +fn scan_falsifiers(arena: &BeliefArena) -> Vec<(CStmt, u32)> { + let entries = arena.entries(); + let mut out: Vec<(CStmt, u32)> = Vec::new(); + for ei in entries { + if !ei.stmt.cop.transits() { + continue; + } + for ej in entries { + if ej.stmt.cop != ei.stmt.cop || ej.stmt.s != ei.stmt.p { + continue; + } + let stmt = CStmt { + s: ei.stmt.s, + cop: ei.stmt.cop, + p: ej.stmt.p, + }; + let Some(stored) = arena.get(stmt) else { + continue; + }; + let cand = ei.truth.deduction(&ej.truth); + if stored.truth.expectation() > 0.5 + 1e-6 && cand.expectation() <= 0.5 + 1e-6 { + let depth = ei.rung.max(ej.rung) + 1; + match out.iter_mut().find(|(s, _)| *s == stmt) { + Some((_, d)) => *d = (*d).max(depth), + None => out.push((stmt, depth)), + } + } + } + } + out +} + +/// Mint the witness docks for a closed arena: positive lane +/// (`Locus::SupportedBy`) = derivation rung; negative lane +/// (`Locus::Contradiction`) = deepest dropped falsifying derivation. +/// Panics (probe-honesty) if any depth exceeds the i4 ceiling. +fn mint_witness_docks(arena: &BeliefArena) -> ([Dock; MAX_DOCKS], usize) { + let mut docks = [EMPTY_DOCK; MAX_DOCKS]; + let n = arena.entries().len(); + assert!(n <= MAX_DOCKS, "probe capacity"); + for (i, b) in arena.entries().iter().enumerate() { + docks[i] = mint_dock(); + if b.rung > 0 { + assert!(b.rung <= 7, "i4 ceiling: rung {} > +7 needs escalation", b.rung); + set_locus(&mut docks[i], Locus::SupportedBy, b.rung as i8); + } + } + for (stmt, depth) in scan_falsifiers(arena) { + assert!(depth <= 8, "i4 ceiling: falsifier depth {depth} > 8"); + let idx = arena + .entries() + .iter() + .position(|b| b.stmt == stmt) + .expect("falsifier target exists"); + set_locus(&mut docks[idx], Locus::Contradiction, -(depth as i8)); + } + (docks, n) +} + +/// Positive fixture: the 4-link chain `1→2→3→4→5`, f=1.0, c=0.9, disjoint +/// stamps, closed to fixed point. +fn build_positive_arena() -> BeliefArena { + let mut a = BeliefArena::new(); + for (k, (s, p)) in [(1u16, 2u16), (2, 3), (3, 4), (4, 5)].iter().enumerate() { + a.observe( + inh(*s, *p), + TruthValue::new(1.0, 0.9), + Stamp::source(k as u32 + 1), + ); + } + a.close_transitive(16); + assert!(a.reached_fixed_point, "fixture chain must close"); + a +} + +/// Add a falsifying counter-chain `1→…→5` whose LAST link has frequency 0, +/// then re-close. `hops` = number of links (3 → counter-depth 2; 5 → 3). +fn add_falsifier_chain(a: &mut BeliefArena, hops: usize) { + // concepts 6.. are counter-branch intermediates + let mut nodes: Vec = vec![1]; + for i in 0..hops - 1 { + nodes.push(6 + i as u16); + } + nodes.push(5); + for (k, w) in nodes.windows(2).enumerate() { + let f = if k == hops - 1 { 0.0 } else { 1.0 }; + a.observe( + inh(w[0], w[1]), + TruthValue::new(f, 0.9), + Stamp::source(10 + k as u32), + ); + } + a.close_transitive(16); + assert!(a.reached_fixed_point, "falsifier closure must fix"); +} + +/// Bit-exact scalar-state snapshot of one belief (f32s by bit pattern). +/// +/// Premises are EXCLUDED from the snapshot — a measured necessity, not a +/// convenience, and itself charter evidence (BELIEF-ABI-RESTORATION-1 F4: +/// ephemeral indexes leaking into cognitive state). Two IDENTICALLY-built +/// arenas diverge in `premises` at TWO layers, both from `close_transitive` +/// admitting its per-pass `derived: HashMap` in iteration order: +/// 1. **index values** — the same derivation stores different numeric arena +/// indices (observed live: `(1,5)` premises `[6,4]` vs `[5,6]`); +/// 2. **route ties** — equal-expectation derivations (`(1,4)` via +/// `(1,3)∘(3,4)` vs `(1,2)∘(2,4)`) are tie-broken by whichever the +/// HashMap yields first, so even statement-RESOLVED premises differ. +/// +/// The epistemically stable scalar state is (stmt, truth, stamp, rung, +/// contradiction); the premise route is nondeterministic decoration. +fn scalar_state(b: &Belief) -> (CStmt, u32, u32, u64, u32, u32) { + ( + b.stmt, + b.truth.frequency.to_bits(), + b.truth.confidence.to_bits(), + b.stamp.0, + b.rung, + b.contradiction.to_bits(), + ) +} + +fn main() { + let mut pass = 0u32; + let mut gate = |name: &str, ok: bool, detail: String| { + assert!(ok, "[FAIL] {name} — {detail}"); + println!(" [PASS] {name} — {detail}"); + pass += 1; + }; + + // ================= Fixture A ================= + let arena_a = build_positive_arena(); + let (docks_a, n_a) = mint_witness_docks(&arena_a); + + // A1 — hand-authored rung expectations (balanced composition: rung is + // ~log2 of span, NOT span length — the #1002 arc's law, restated here). + let expected: [((u16, u16), u32); 10] = [ + ((1, 2), 0), + ((2, 3), 0), + ((3, 4), 0), + ((4, 5), 0), + ((1, 3), 1), + ((2, 4), 1), + ((3, 5), 1), + ((1, 4), 2), + ((2, 5), 2), + ((1, 5), 2), + ]; + let mut a1_ok = arena_a.entries().len() == expected.len(); + for ((s, p), r) in expected { + a1_ok &= arena_a.get(inh(s, p)).map(|b| b.rung) == Some(r); + } + gate( + "A1 authored rung fixture", + a1_ok, + format!("{} statements, rungs 0/1/2 as authored", expected.len()), + ); + + // A2 — legacy projection parity + negative lane silent in fixture A. + let mut a2_ok = true; + for (i, b) in arena_a.entries().iter().enumerate() { + let w = witness_of(&docks_a[i]); + a2_ok &= support_ceiling(w) == b.rung; + a2_ok &= falsifier_ceiling(w) == 0; + } + gate( + "A2 support projection == Belief::rung, falsifier lane silent", + a2_ok, + format!("{n_a}/{n_a} docks: support_ceiling parity, zero negatives"), + ); + + // A3 — dock conservation: LE geometry, classid recovery via the shipped + // FacetCascade reading, register identity through the borrowed view. + let mut a3_ok = true; + for dock in docks_a.iter().take(n_a) { + let fc = FacetCascade::from_bytes(dock); + a3_ok &= fc.facet_classid == PROBE_TARSKI_CLASSID; + // Full LE round-trip through the shipped classid reading: the dock's + // bytes survive the FacetCascade decode/encode unchanged. (NOT + // `tier_bytes()` — that is the coarse→fine hi:lo LADDER view; the + // wire order per tier is `[lo, hi]`, from_bytes' own doc.) + a3_ok &= fc.to_bytes() == *dock; + a3_ok &= witness_of(dock).to_register() == dock[4..16]; + } + gate( + "A3 dock conservation (classid LE + register identity, both readings)", + a3_ok, + format!("{n_a} docks read identically as FacetCascade and G24N4 view"), + ); + + let s_apex = inh(1, 5); + let apex_idx = arena_a + .entries() + .iter() + .position(|b| b.stmt == s_apex) + .expect("apex"); + let apex_a_state = scalar_state(&arena_a.entries()[apex_idx]); + let apex_a_dock = docks_a[apex_idx]; + + // ================= Fixture B (falsifier, depth 2) ================= + let mut arena_b = build_positive_arena(); + add_falsifier_chain(&mut arena_b, 3); + let (docks_b, _n_b) = mint_witness_docks(&arena_b); + + // B1 — the falsifier is INVISIBLE to the scalar state: every fixture-A + // belief (apex included) is bit-identical after the counter-chain. This + // is the shipped CHOICE law doing the discarding (belief.rs:247). + let mut b1_ok = true; + for b in arena_a.entries() { + let after = arena_b.get(b.stmt).expect("fixture-A statement survives"); + b1_ok &= scalar_state(after) == scalar_state(b); + } + gate( + "B1 falsifier invisible in scalar state (CHOICE drops it)", + b1_ok, + format!("{n_a}/{n_a} fixture-A beliefs bit-identical post-falsifier"), + ); + + // B2 — the witness RETAINS what the scalar dropped, without touching the + // support lane: apex dock differs from fixture A in EXACTLY the + // Contradiction nibble; +2 support survives beside −2 falsifier. + let apex_b_idx = arena_b + .entries() + .iter() + .position(|b| b.stmt == s_apex) + .expect("apex in B"); + let apex_b_dock = docks_b[apex_b_idx]; + let wb = witness_of(&apex_b_dock); + let changed_slots: Vec = (0..24) + .filter(|&s| wb.get(s) != witness_of(&apex_a_dock).get(s)) + .collect(); + gate( + "B2 falsifier lands beside support (neither overwrites the other)", + wb.at(Locus::SupportedBy) == 2 + && wb.at(Locus::Contradiction) == -2 + && changed_slots == vec![Locus::Contradiction as usize], + format!( + "apex: SupportedBy {:+}, Contradiction {:+}, changed slots {:?}", + wb.at(Locus::SupportedBy), + wb.at(Locus::Contradiction), + changed_slots + ), + ); + + // B3 — can-stay-silent: the falsifier channel fires ONLY at the apex. + let hotspots: Vec = arena_b + .entries() + .iter() + .enumerate() + .filter(|(i, _)| { + let w = witness_of(&docks_b[*i]); + support_ceiling(w) > 0 && falsifier_ceiling(w) > 0 + }) + .map(|(_, b)| b.stmt) + .collect(); + gate( + "B3 dialectical hotspot detection is discriminating", + hotspots == vec![s_apex], + format!("exactly one hotspot (the apex), {} beliefs scanned", arena_b.entries().len()), + ); + + // ================= Fixture B' (falsifier, depth 3) ================= + let mut arena_b2 = build_positive_arena(); + add_falsifier_chain(&mut arena_b2, 5); + let (docks_b2, _) = mint_witness_docks(&arena_b2); + let apex_b2_idx = arena_b2 + .entries() + .iter() + .position(|b| b.stmt == s_apex) + .expect("apex in B'"); + let wb2 = witness_of(&docks_b2[apex_b2_idx]); + + // B4 — the depth discrimination the scalar CANNOT make: apex scalar + // state is identical between depth-2 and depth-3 falsifier worlds + // (zero bits of falsifier depth survive in the arena), while the + // witness field distinguishes them. + let b_state = scalar_state(&arena_b.entries()[apex_b_idx]); + let b2_state = scalar_state(&arena_b2.entries()[apex_b2_idx]); + gate( + "B4 scalar state identical across falsifier depths; witness differs", + b_state == b2_state + && b_state == apex_a_state + && wb.at(Locus::Contradiction) == -2 + && wb2.at(Locus::Contradiction) == -3, + format!( + "apex scalar bit-equal in A/B/B'; witness −2 vs {:+}", + wb2.at(Locus::Contradiction) + ), + ); + + // ================= Fixture C (falsifier removed) ================= + let arena_c = build_positive_arena(); + let (docks_c, n_c) = mint_witness_docks(&arena_c); + // Per-STATEMENT comparison, not per-index: admission order is HashMap- + // nondeterministic (the F4 finding above), so entry i of two identical + // builds need not be the same statement. + let mut c1_ok = n_c == n_a; + for (i, b) in arena_a.entries().iter().enumerate() { + let ci = arena_c + .entries() + .iter() + .position(|cb| cb.stmt == b.stmt) + .expect("fixture-C statement set matches A"); + c1_ok &= docks_c[ci] == docks_a[i]; + } + gate( + "C1 falsifier removal restores byte-identical docks", + c1_ok, + format!("{n_a} docks byte-equal to fixture A (negative lane vanished)"), + ); + + // ================= Physical honesty gates ================= + // P1 — the i4 ceiling is +7/−8: depth beyond it CLAMPS, it does not + // widen. Deeper derivations need escalation (ClassView re-election / + // bucket rollover), never a wider nibble in this reading. + let mut probe = mint_dock(); + set_locus(&mut probe, Locus::SupportedBy, 9); + let clamped_hi = witness_of(&probe).at(Locus::SupportedBy); + set_locus(&mut probe, Locus::Contradiction, -9); + let clamped_lo = witness_of(&probe).at(Locus::Contradiction); + gate( + "P1 i4 depth ceiling stated honestly (+7/−8, clamp not widen)", + clamped_hi == 7 && clamped_lo == -8, + format!("+9 → {clamped_hi:+}, −9 → {clamped_lo:+}"), + ); + + // P2 — masked election over the signed field is fail-closed and + // discriminating: electing ONLY the support lane reads +2 at the apex + // and refuses the bound-but-unelected falsifier lane. + let support_mask = WideFieldMask::from_positions(&[Locus::SupportedBy as u8]); + gate( + "P2 locus election reads support, refuses unelected falsifier", + wb.elected(&support_mask, Locus::SupportedBy) == Some(2) + && wb.elected(&support_mask, Locus::Contradiction).is_none() + && wb.elected(&WideFieldMask::EMPTY, Locus::SupportedBy).is_none(), + "elected(SupportedBy)=+2; Contradiction unelected → None; EMPTY fail-closed".to_string(), + ); + + println!("PROBE-TARSKI-SIGNED-WITNESS-1: ALL {pass} GATES GREEN"); + println!( + "verdict: Belief::rung is the positive-lane projection of a signed \ + G24N4 derivational field; the falsifier lane carries what the \ + shipped CHOICE law provably discards" + ); +} From f990e0b536227e125852753c14535b0f39a17986 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 23 Aug 2026 18:23:33 +0000 Subject: [PATCH 2/2] recut: separate the Tarski ClassView from A9, de-circularize the rung claim Addresses the review of #1007. Three substantive defects fixed, one headline claim withdrawn, plus the rustfmt failure. 1. A9 SEMANTIC-CONTRACT VIOLATION (the important one). Both probes wrote derivational MAGNITUDES through `Locus::SupportedBy`/`Contradiction`, while CausalWitnessFacet's A9 reading is operator-locked "loci, not magnitudes" -- every named Locus is a signed context POINTER, and the module states verbatim that the rung level occupies ZERO slots. Using A9's semantic API to mean something A9 forbids is exactly the smuggle the DOCK/ROUTE law exists to prevent, and acknowledging it in a doc comment did not make it lawful. Fix: a probe-local `SignedTarskiWitnessView([u8; 12])` with its own slot names (`TarskiSlot::{ConstructiveDepth, FalsifyingDepth}`), its own nibble accessors, and its own classid. Same physical geometry, different ClassView, zero shared vocabulary. In the four-plane probe this splits the WHY plane into TWO registers, which is the architecturally correct shape and now demonstrates the law instead of violating it: magnitudes live in the Tarski register; the mediator POINTER lives in a genuine A9 register read through `Locus::Kausal`, which is what that name actually means. FP2 gained a fourth arm proving the pointer lane is isolated too. 2. THE POSITIVE PROOF WAS CIRCULAR. `mint_witness_docks` took `b.rung`, wrote it into a nibble, and `support_ceiling()` read it back and checked it equalled `b.rung` -- proving only that an i4 field can hold 0..7. Withdrawn in the module docs by name. Fix: `derive_depth_from_support()` derives depth from the premise DAG alone (`depth(b) = 0` if no premises, else `1 + max(depth(premises))`), never reading `b.rung`; the arena's stored scalar is the ORACLE it is checked against. Returns None on a premise cycle rather than papering over it. A2 now measures something falsifiable and passes 10/10 -- which is a real result rather than a tautology. Headline claim recast to what is actually established: a signed i4 derivational witness PRESERVES falsifier depth the Belief scalar state provably discards (B1/B4, the genuinely novel half), and on this fixture the independently-derived constructive lane reproduces rung. 3. `CausalRow` is now labelled a PROBE FIXTURE in the type doc, the module honesty box, and the verdict line. It is an AoS test object and must never be cited as evidence about the resident SoA layout. 4. The premise-route nondeterminism finding no longer calls the routes "decoration". Two proof routes with tied truth may carry different provenance, so a route chosen by HashMap order is a real reproducibility problem; what is established is only that the route is not currently STABLE, hence unusable as a parity key here. 5. rustfmt: `cargo fmt -p lance-graph-planner -- --check` now clean. The original commit ran clippy but never fmt, which is what Style Check caught. Gates: 11/11 (Tarski, up from 10 -- added slot-isolation across all 24 nibbles) and 7/7 (four-plane), both green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01KCGhDYoQBXs3poaR7sFuqp --- .../probe_four_plane_causal_medium.rs | 178 ++++-- .../examples/probe_tarski_signed_witness.rs | 533 ++++++++++++------ 2 files changed, 476 insertions(+), 235 deletions(-) diff --git a/crates/lance-graph-planner/examples/probe_four_plane_causal_medium.rs b/crates/lance-graph-planner/examples/probe_four_plane_causal_medium.rs index d40500217..0a7bd8c7c 100644 --- a/crates/lance-graph-planner/examples/probe_four_plane_causal_medium.rs +++ b/crates/lance-graph-planner/examples/probe_four_plane_causal_medium.rs @@ -42,12 +42,22 @@ //! contract's declared knowledge. This probe writes through the topology //! lens by construction and says so — a production writer would declare //! it per `(classid, rail)`. -//! - `CausalWitnessFacet`'s A9 reading is operator-locked "loci, not -//! magnitudes." This probe's ClassView reads THREE loci with per-locus -//! semantics (the ClassView defines what a sign means per locus): -//! `SupportedBy`/`Contradiction` as signed derivational DEPTH (the Tarski -//! reading, PROBE-TARSKI-SIGNED-WITNESS-1), `Kausal` as a signed stream -//! POINTER to the located mediator (the shipped A9 pointer semantics). +//! - **The WHY plane is TWO registers, not one — deliberately.** +//! `CausalWitnessFacet`'s A9 reading is operator-locked *"loci, not +//! magnitudes"*: every named `Locus` is a signed context POINTER. So the +//! evidence plane's signed derivational MAGNITUDES live in their own +//! probe-local register (`TARSKI_CLASSID`, own slot names — mirroring +//! `PROBE-TARSKI-SIGNED-WITNESS-1`'s `SignedTarskiWitnessView`), and the +//! mediator POINTER lives in a genuine A9 register read through +//! `Locus::Kausal`, which is what that name actually means. An earlier +//! revision put magnitudes and a pointer in ONE A9 register; that mixed +//! two semantic systems in one ClassView and is withdrawn. Same +//! geometry, two classids, two readings, no vocabulary shared. +//! +//! - **`CausalRow` is a PROBE FIXTURE, not the implementation shape.** It is +//! an AoS test object holding the lanes side by side so the gates can +//! compare them; it is NOT evidence about the resident SoA layout and must +//! never be cited as such. use causal_edge::layout::{CausalTopology, ReasoningBand}; use causal_edge::CausalEdge64; @@ -61,8 +71,21 @@ const HYPOTHESIS_CLASSID: u32 = 0xFFFF_000A; /// V4 classid is provisional behind the O5 gate). const INTERVENTION_CLASSID: u32 = 0xFFFF_000B; -/// One resident causal-hypothesis row: four planes, four disjoint lanes of -/// ONE `Copy` row. No heap, no hash, no materialized mask. +/// Probe-local slot: signed constructive derivation depth (`+n`). +const TARSKI_CONSTRUCTIVE: usize = 0; +/// Probe-local slot: signed falsifying derivation depth (`−n`). +const TARSKI_FALSIFYING: usize = 1; + +/// **PROBE FIXTURE** — an AoS test object holding one hypothesis's lanes +/// side by side so the gates can compare them. This is NOT the resident +/// layout and is never evidence about it (see the honesty box). Five lanes: +/// +/// | lane | plane | reading | +/// |---|---|---| +/// | `address` | WHERE | `FacetCascade` / `AttentionFocusFacet` | +/// | `edge` | WHAT + LENS | `CausalTopology` / `ReasoningBand` | +/// | `evidence` | WHY (magnitudes) | probe-local signed-Tarski | +/// | `pointers` | WHY (pointers) | shipped A9 `Locus` | #[derive(Clone, Copy, PartialEq, Eq, Debug)] struct CausalRow { /// Plane 1 — WHERE: the 16-byte address dock (classid + G6D2 cascade). @@ -71,8 +94,14 @@ struct CausalRow { /// Planes 2+3 — WHAT + LENS: the causal relation register /// (topology bits 59-60, reasoning band bits 61-63). edge: CausalEdge64, - /// Plane 4 (evidence) — WHY: the 12-byte G24N4 signed witness register. + /// Plane 4a — WHY, MAGNITUDE half: a 12-byte register read through the + /// probe-local signed-Tarski ClassView (depths, not pointers). NOT an + /// A9 register: A9's contract forbids magnitudes in a `Locus`. evidence: [u8; WITNESS_REGISTER_BYTES], + /// Plane 4b — WHY, POINTER half: a genuine A9 register, read through + /// `Locus::Kausal` = a signed stream pointer to the located mediator, + /// which is exactly what that `Locus` name means. + pointers: CausalWitnessFacet, } /// One V4-plane row: a typed intervention particle, R2IL-shaped @@ -124,14 +153,34 @@ fn world_do_knockout(target_offset_from_edge: i8) -> u8 { } } -fn witness_of(reg: &[u8; WITNESS_REGISTER_BYTES]) -> &CausalWitnessFacet { - CausalWitnessFacet::from_register_ref(reg) +/// Signed depth at a probe-local Tarski slot (sign-extended nibble). This is +/// the MAGNITUDE reading — its own accessors, deliberately not A9's, because +/// A9's `Locus` names mean pointers. +fn tarski_get(reg: &[u8; WITNESS_REGISTER_BYTES], slot: usize) -> i8 { + if slot >= 24 { + return 0; + } + let byte = reg[slot / 2]; + let nib = if slot & 1 == 0 { + byte & 0x0F + } else { + (byte >> 4) & 0x0F + }; + ((nib << 4) as i8) >> 4 } -fn set_locus(reg: &mut [u8; WITNESS_REGISTER_BYTES], locus: Locus, v: i8) { - let mut w = *witness_of(reg); - w.set(locus as usize, v); - *reg = w.to_register(); +/// Set a probe-local Tarski slot; clamps to `[−8, +7]`. +fn tarski_set(reg: &mut [u8; WITNESS_REGISTER_BYTES], slot: usize, depth: i8) { + if slot >= 24 { + return; + } + let v = (depth.clamp(-8, 7) as u8) & 0x0F; + let bi = slot / 2; + if slot & 1 == 0 { + reg[bi] = (reg[bi] & 0xF0) | v; + } else { + reg[bi] = (reg[bi] & 0x0F) | (v << 4); + } } /// Build an address dock in region `heel` (tier-0 coarse byte). @@ -168,9 +217,10 @@ fn main() { // falsifier −1 (a wrong-mediator candidate already refuted), // mediator locus 0 (the epistemic pothole)." let mut evidence = [0u8; WITNESS_REGISTER_BYTES]; - set_locus(&mut evidence, Locus::SupportedBy, 2); - set_locus(&mut evidence, Locus::Contradiction, -1); - // Locus::Kausal deliberately left 0 — the mediator pothole. + tarski_set(&mut evidence, TARSKI_CONSTRUCTIVE, 2); + tarski_set(&mut evidence, TARSKI_FALSIFYING, -1); + // The A9 pointer register: Locus::Kausal deliberately left 0 (unbound) + // — the mediator pothole. A9 semantics, A9 register. let mut row = CausalRow { address: address_in_region(0x11, 0x01), @@ -178,32 +228,32 @@ fn main() { .with_topology(CausalTopology::IndirectUnknownIntermediates) .with_reasoning_band(ReasoningBand::Causal), evidence, + pointers: CausalWitnessFacet::ZERO, }; // A sibling row in ANOTHER region — the scope must exclude it. let outside = CausalRow { address: address_in_region(0x22, 0x02), edge: CausalEdge64::ZERO.with_topology(CausalTopology::Direct), evidence: [0u8; WITNESS_REGISTER_BYTES], + pointers: CausalWitnessFacet::ZERO, }; // Plane 1 — WHERE: a depth-1 scope over region 0x11 (tier-0 hi byte). - let scope = AttentionFocusFacet::prefix( - FacetCascade::from_bytes(&address_in_region(0x11, 0x00)), - 1, - ) - .expect("depth 1 <= 12"); + let scope = + AttentionFocusFacet::prefix(FacetCascade::from_bytes(&address_in_region(0x11, 0x00)), 1) + .expect("depth 1 <= 12"); - // FP1 — all four planes readable, each answering ITS question. - let w = witness_of(&row.evidence); + // FP1 — all four planes readable, each answering ITS question, and the + // WHY plane's two halves read through their OWN ClassViews. gate( "FP1 four planes independently readable", scope.covers(focus_of(&row)) && !scope.covers(focus_of(&outside)) && row.edge.topology() == CausalTopology::IndirectUnknownIntermediates && row.edge.reasoning_band() == ReasoningBand::Causal - && w.at(Locus::SupportedBy) == 2 - && w.at(Locus::Contradiction) == -1 - && !w.is_bound(Locus::Kausal), + && tarski_get(&row.evidence, TARSKI_CONSTRUCTIVE) == 2 + && tarski_get(&row.evidence, TARSKI_FALSIFYING) == -1 + && !row.pointers.is_bound(Locus::Kausal), "WHERE covers row/excludes sibling; WHAT=IndirectUnknown; LENS=Causal; \ WHY=+2/−1/mediator-pothole" .to_string(), @@ -215,18 +265,29 @@ fn main() { { let before = row; let mut t = row; - set_locus(&mut t.evidence, Locus::Contradiction, -3); - let ev_only = t.address == before.address && t.edge == before.edge; + tarski_set(&mut t.evidence, TARSKI_FALSIFYING, -3); + let ev_only = + t.address == before.address && t.edge == before.edge && t.pointers == before.pointers; let mut t2 = row; t2.edge = t2.edge.with_topology(CausalTopology::Unknown); - let edge_only = t2.address == before.address && t2.evidence == before.evidence; + let edge_only = t2.address == before.address + && t2.evidence == before.evidence + && t2.pointers == before.pointers; let mut t3 = row; t3.address = address_in_region(0x11, 0x7F); - let addr_only = t3.edge == before.edge && t3.evidence == before.evidence; + let addr_only = t3.edge == before.edge + && t3.evidence == before.evidence + && t3.pointers == before.pointers; + let mut t4 = row; + t4.pointers = t4.pointers.with(Locus::Kausal, -1); + let ptr_only = t4.address == before.address + && t4.edge == before.edge + && t4.evidence == before.evidence; gate( - "FP2 plane isolation (each write confined to its lane)", - ev_only && edge_only && addr_only, - "evidence/edge/address writes each leave the other two lanes bit-identical" + "FP2 lane isolation (each write confined to its lane)", + ev_only && edge_only && addr_only && ptr_only, + "magnitude/edge/address/pointer writes each leave the other three lanes \ + bit-identical" .to_string(), ); } @@ -236,13 +297,13 @@ fn main() { { let edge_before = row.edge; let mut t = row; - set_locus(&mut t.evidence, Locus::Contradiction, -8); + tarski_set(&mut t.evidence, TARSKI_FALSIFYING, -8); gate( "FP3 negative evidence does NOT flip band or topology", t.edge == edge_before && t.edge.reasoning_band() == ReasoningBand::Causal && t.edge.topology() == CausalTopology::IndirectUnknownIntermediates, - "Contradiction −8 written; CE64 bit-identical (band Causal, topology unchanged)" + "falsifying depth −8 written; CE64 bit-identical (band Causal, topology unchanged)" .to_string(), ); } @@ -252,8 +313,8 @@ fn main() { // row, silent on the out-of-scope row (which is also unbound). let pothole = |r: &CausalRow| -> bool { scope.covers(focus_of(r)) - && witness_of(&r.evidence).at(Locus::SupportedBy) > 0 - && !witness_of(&r.evidence).is_bound(Locus::Kausal) + && tarski_get(&r.evidence, TARSKI_CONSTRUCTIVE) > 0 + && !r.pointers.is_bound(Locus::Kausal) }; gate( "FP4 pothole query (support present, mediator locus empty) is scoped", @@ -293,20 +354,23 @@ fn main() { let (addr_before, band_before, support_before) = ( row.address, row.edge.reasoning_band(), - witness_of(&row.evidence).at(Locus::SupportedBy), + tarski_get(&row.evidence, TARSKI_CONSTRUCTIVE), ); if probe_m.observed() == OBS_LINK_BROKEN { - set_locus(&mut row.evidence, Locus::Kausal, probe_m.target_offset()); - row.edge = row.edge.with_topology(CausalTopology::IndirectKnownIntermediates); + // The mediator is a POINTER — it lands in the A9 register, through + // the Locus that actually means "my cause". + row.pointers = row.pointers.with(Locus::Kausal, probe_m.target_offset()); + row.edge = row + .edge + .with_topology(CausalTopology::IndirectKnownIntermediates); } - let w = witness_of(&row.evidence); gate( "FP6 supporting intervention closes the loop (pothole → known mediator)", - w.at(Locus::Kausal) == -1 + row.pointers.at(Locus::Kausal) == -1 && row.edge.topology() == CausalTopology::IndirectKnownIntermediates && row.edge.reasoning_band() == band_before - && w.at(Locus::SupportedBy) == support_before - && w.at(Locus::Contradiction) == -1 + && tarski_get(&row.evidence, TARSKI_CONSTRUCTIVE) == support_before + && tarski_get(&row.evidence, TARSKI_FALSIFYING) == -1 && row.address == addr_before && !pothole(&row), "Kausal bound −1; topology Unknown→Known intermediates; band/support/falsifier/address \ @@ -320,27 +384,35 @@ fn main() { // CausalRow's own size is a probe-local composite (Rust struct layout // may insert padding between the three lane fields) — NOT itself a // dock; each LANE's width is what the ABI actually const-asserts. - const _: () = assert!(core::mem::size_of::<[u8; 16]>() == 16, "address lane is one dock"); + const _: () = assert!( + core::mem::size_of::<[u8; 16]>() == 16, + "address lane is one dock" + ); const _: () = assert!( core::mem::size_of::<[u8; WITNESS_REGISTER_BYTES]>() == 12, "evidence lane is the G24N4 register" ); - const _: () = assert!(core::mem::size_of::() == 16, "V4 row is one dock"); + const _: () = assert!( + core::mem::size_of::() == 16, + "V4 row is one dock" + ); const _: () = assert!(core::mem::size_of::() == 8, "CE64 is one u64"); let fc = FacetCascade::from_bytes(&row.address); gate( "FP7 shared-ABI conservation (fixed LE registers, byte-exact round-trips)", fc.to_bytes() == row.address && fc.facet_classid == HYPOTHESIS_CLASSID - && witness_of(&row.evidence).to_register() == row.evidence, - "address round-trips through FacetCascade; evidence through G24N4; sizes const-asserted" + && row.pointers.to_register().len() == WITNESS_REGISTER_BYTES, + "address round-trips through FacetCascade; the magnitude lane through the Tarski view; \ + the pointer lane through A9; every lane width const-asserted" .to_string(), ); println!("PROBE-FOUR-PLANE-CAUSAL-MEDIUM-1: ALL {pass} GATES GREEN"); println!( - "verdict: WHERE (scope) / WHAT (topology) / LENS (band) / WHY (signed witness) / \ - DID (typed intervention) compose as disjoint lanes of resident rows; the falsifier \ - and the intervention each land in their own plane and nothing auto-flips" + "verdict: WHERE (scope) / WHAT (topology) / LENS (band) / WHY-magnitude (Tarski view) / \ + WHY-pointer (A9 Locus) / DID (typed intervention) stay separable across a write to \ + any one of them; nothing auto-flips, and no ClassView's vocabulary is used to mean \ + another's. Probe FIXTURE, not evidence about the resident SoA shape." ); } diff --git a/crates/lance-graph-planner/examples/probe_tarski_signed_witness.rs b/crates/lance-graph-planner/examples/probe_tarski_signed_witness.rs index 9b61e61fc..fea000d76 100644 --- a/crates/lance-graph-planner/examples/probe_tarski_signed_witness.rs +++ b/crates/lance-graph-planner/examples/probe_tarski_signed_witness.rs @@ -1,64 +1,73 @@ -//! PROBE-TARSKI-SIGNED-WITNESS-1 — is `Belief::rung` an impoverished -//! projection of a signed derivational field? +//! PROBE-TARSKI-SIGNED-WITNESS-1 — can a signed `24×i4` derivational +//! witness preserve falsifier depth that `Belief`'s scalar state discards? //! -//! **The claim under test (operator, 2026-08-23).** The scalar Tarski rung -//! (`Belief::rung: u32`) answers only "how far did the successful proof -//! climb?" A `24×i4` signed witness field over the SAME 16-byte dock -//! (`classid(4) + 12-byte register`) could answer "where did the proof climb, -//! where did it fail, and where does a counter-proof bite?" — with -//! `+n` = constructive derivation depth, `-n` = falsifying derivation depth, -//! `0` = absent/unresolved, per locus. +//! **The measured claim, stated at the strength the evidence supports:** //! -//! **This is a probe-local ClassView READING, not a new tenant and not a -//! mint.** The physical carrier is the shipped `G24N4` nibble law -//! ([`CausalWitnessFacet`], `causal_witness.rs`) over the shipped 16-byte -//! dock ([`FacetCascade`]). The shipped A9 reading is operator-locked -//! "loci, not magnitudes" — THIS reading (sign = support vs falsification, -//! magnitude = derivational depth) is a DIFFERENT ClassView over the same -//! bytes, exactly as the "one register, three readings" doctrine (PR #729) -//! provides. The probe-local classid below is a placeholder, NOT an OGAR -//! mint; nothing here canonizes. +//! > A signed i4 derivational witness CAN preserve falsifier depth that the +//! > current `Belief` scalar state provably discards. Whether the positive +//! > Tarski rung is itself *derivable* from that field is measured here +//! > against an independent oracle and reported — not assumed. +//! +//! An earlier revision of this probe claimed to prove `Belief::rung` IS the +//! projection of a derivational field. **That proof was circular** and the +//! claim is withdrawn: it wrote `b.rung` into a nibble and then checked the +//! nibble equalled `b.rung`, which proves only that an i4 field can hold +//! 0..7. The positive lane here is now derived **independently from support +//! topology** (the premise DAG — [`derive_depth_from_support`], which never +//! reads `b.rung`), with the arena's stored scalar as the ORACLE it is +//! checked against. +//! +//! # This probe does NOT use the A9 `Locus` API (deliberate, load-bearing) +//! +//! `CausalWitnessFacet`'s A9 reading is **operator-locked**: *"Loci, not +//! magnitudes"* — every named `Locus` is a signed context POINTER, `0` is +//! unbound, and the module states verbatim that *"the rung level occupies +//! ZERO slots."* Writing a derivational MAGNITUDE through `Locus:: +//! SupportedBy` would be using A9's semantic API to mean something A9's +//! contract forbids — the same-geometry/different-meaning smuggle the +//! DOCK/ROUTE law exists to prevent. +//! +//! So this probe carries its own [`SignedTarskiWitnessView`] over the same +//! **physical** 12-byte / 24-nibble geometry, with its own slot names +//! ([`TarskiSlot`]) and its own nibble accessors. Same bytes, same dock, +//! **different ClassView** — which is exactly what the law licenses: +//! +//! > Same physical geometry may support different ClassViews. That does not +//! > license using one ClassView's semantic API to mean another thing. +//! +//! The probe-local classid is a placeholder, NOT an OGAR mint. //! //! **⚠ MEMORY-ABI ESCAPE, acknowledged in place.** `BeliefArena` remains the //! acknowledged non-canonical AoS owner (#1004, //! `E-TYPE-COMPLEXITY-EXPOSED-A-MEMORY-ABI-ESCAPE-1`); this probe uses it as -//! the PARITY ORACLE only. The witness docks are a fixed stack array of -//! 16-byte Copy rows — no heap row population, no hash, no materialized -//! mask, no new backing store beyond the dock rows themselves. This probe -//! informs the `BELIEF-ABI-RESTORATION-1` charter's step-2 ruling on `rung`; -//! it does NOT execute the charter's step 3. +//! the PARITY ORACLE only and repairs nothing. The witness docks are a fixed +//! stack array of 16-byte `Copy` rows — a bounded **probe fixture**, not a +//! claim about the resident SoA shape. //! -//! # Fixtures (all gates must be able to fail) +//! # Fixtures //! -//! - **A** — ordinary positive derivation chain, no falsifier. The G24N4 -//! positive support projection must reproduce `Belief::rung` exactly. -//! - **B** — same chain plus a freq-0 falsifying counter-chain reaching the -//! apex statement S. The shipped merge law (`admit_derived` CHOICE, -//! `belief.rs:247`: a pure-derived candidate replaces only on STRICT -//! expectation gain) silently DROPS the counter-derivation — so the -//! arena's scalar state at S is bit-identical to fixture A. The witness -//! field alone retains the falsifier, without disturbing the support lane. -//! - **B'** — a DEEPER falsifying counter-chain. The arena's scalar state at -//! S is provably identical between B and B' (zero bits of falsifier depth -//! survive); the witness distinguishes them. -//! - **C** — falsifier removed. The witness register returns byte-identical -//! to fixture A: the negative lane vanishes, the positive lane is exact. -//! -//! Physical conservation gates: same 16-byte dock, same LE geometry, G24N4 -//! reading only, borrowed zero-copy register views, i4 ceiling stated -//! honestly (+7/−8 — derivations deeper than rung 7 need escalation, not a -//! wider nibble). +//! - **A** — positive derivation chain, no falsifier. Measures whether an +//! independently-derived support depth agrees with the arena's `rung`. +//! - **B** — same chain plus a freq-0 falsifying counter-chain. The shipped +//! merge law (`admit_derived` CHOICE, `belief.rs:247`: replace only on +//! STRICT expectation gain) DROPS the counter-derivation, so the arena's +//! scalar state is bit-identical to fixture A. The witness alone retains it. +//! - **B'** — a DEEPER counter-chain, scalar-indistinguishable from B. +//! - **C** — falsifier removed; the register returns byte-identical to A. -use lance_graph_contract::causal_witness::{CausalWitnessFacet, Locus, WITNESS_REGISTER_BYTES}; -use lance_graph_contract::class_view::WideFieldMask; use lance_graph_contract::facet::FacetCascade; -use lance_graph_planner::nars::belief::{BeliefArena, Belief, CStmt, Copula, Stamp}; +use lance_graph_planner::nars::belief::{Belief, BeliefArena, CStmt, Copula, Stamp}; use lance_graph_planner::nars::truth::TruthValue; -/// Probe-local ClassView id for the Tarski signed-witness READING. -/// Deliberately in a nonsense range: this is NOT an OGAR mint. +/// Probe-local ClassView id for the signed-Tarski READING. Deliberately in +/// a nonsense range: this is NOT an OGAR mint. const PROBE_TARSKI_CLASSID: u32 = 0xFFFF_0009; +/// The content-blind register width shared with every 12-byte reading. +const REGISTER_BYTES: usize = 12; +/// 12 bytes = 24 nibbles. +const TARSKI_SLOTS: usize = 24; + /// Dock capacity — fixed stack array, no heap row population. const MAX_DOCKS: usize = 64; @@ -66,10 +75,6 @@ const MAX_DOCKS: usize = 64; type Dock = [u8; 16]; const _: () = assert!(core::mem::size_of::() == 16, "16-byte dock"); -const _: () = assert!( - core::mem::size_of::() == WITNESS_REGISTER_BYTES, - "G24N4 register is the dock payload width" -); const _: () = assert!( core::mem::size_of::() == 16, "FacetCascade shares the dock width" @@ -77,19 +82,112 @@ const _: () = assert!( const EMPTY_DOCK: Dock = [0u8; 16]; -/// Borrowed zero-copy G24N4 view of a dock's 12-byte payload -/// (`CausalWitnessFacet::from_register_ref` — a pointer reborrow, no copy). -fn witness_of(dock: &Dock) -> &CausalWitnessFacet { - let reg: &[u8; WITNESS_REGISTER_BYTES] = dock[4..16].try_into().expect("12-byte payload"); - CausalWitnessFacet::from_register_ref(reg) +/// Probe-local slot names for the signed-Tarski reading. **Deliberately NOT +/// `Locus` variants** — under A9 those names mean signed context pointers, +/// and this view's slots carry signed derivational DEPTHS. Two readings of +/// the same physical nibbles must not share a vocabulary. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +enum TarskiSlot { + /// `+n` — the constructive derivation reaching this statement has depth n. + ConstructiveDepth = 0, + /// `−n` — a falsifying counter-derivation of depth n bites this statement. + FalsifyingDepth = 1, } -/// Write-back path per the borrow-strategy law: owned Copy microcopy of the -/// 12-byte register, nibble edit, gated write-back. Never `&mut` a view. -fn set_locus(dock: &mut Dock, locus: Locus, offset: i8) { - let mut w = *witness_of(dock); - w.set(locus as usize, offset); - dock[4..16].copy_from_slice(&w.to_register()); +/// The signed-Tarski reading: a 12-byte content-blind register carved as 24 +/// signed `i4` **derivational magnitudes**. +/// +/// Sign is polarity (`+` constructive / `−` falsifying / `0` unresolved); +/// magnitude is derivational depth. This is a DIFFERENT ClassView from +/// `CausalWitnessFacet`'s A9 reading of the identical geometry, and shares +/// none of its accessors — see the module docs. +#[derive(Clone, Copy, PartialEq, Eq, Debug, Default)] +#[repr(transparent)] +struct SignedTarskiWitnessView([u8; REGISTER_BYTES]); + +const _: () = assert!( + core::mem::size_of::() == REGISTER_BYTES, + "the view is exactly its backing register" +); + +impl SignedTarskiWitnessView { + const ZERO: Self = Self([0u8; REGISTER_BYTES]); + + /// Borrowed zero-cost read of a raw register (repr(transparent) reborrow). + fn from_register_ref(reg: &[u8; REGISTER_BYTES]) -> &Self { + // SAFETY: `#[repr(transparent)]` over `[u8; REGISTER_BYTES]` with + // identical size (const-asserted above), so the reinterpretation is + // layout-identical and defined. No read of the bytes occurs here. + unsafe { &*(reg as *const [u8; REGISTER_BYTES] as *const Self) } + } + + /// Signed depth at slot `0..24` (sign-extended nibble; even slot = low + /// nibble, odd = high). Own implementation — this view does not borrow + /// A9's accessors any more than it borrows A9's meanings. + fn get(self, slot: usize) -> i8 { + if slot >= TARSKI_SLOTS { + return 0; + } + let byte = self.0[slot / 2]; + let nib = if slot & 1 == 0 { + byte & 0x0F + } else { + (byte >> 4) & 0x0F + }; + ((nib << 4) as i8) >> 4 + } + + /// Set the signed depth at slot `0..24`; clamps to `[−8, +7]`. + fn set(&mut self, slot: usize, depth: i8) { + if slot >= TARSKI_SLOTS { + return; + } + let v = (depth.clamp(-8, 7) as u8) & 0x0F; + let bi = slot / 2; + if slot & 1 == 0 { + self.0[bi] = (self.0[bi] & 0xF0) | v; + } else { + self.0[bi] = (self.0[bi] & 0x0F) | (v << 4); + } + } + + fn at(self, slot: TarskiSlot) -> i8 { + self.get(slot as usize) + } + + fn to_register(self) -> [u8; REGISTER_BYTES] { + self.0 + } + + /// `max(positive slots)` — the constructive-support ceiling. + fn support_ceiling(self) -> u32 { + (0..TARSKI_SLOTS) + .map(|s| self.get(s).max(0) as u32) + .max() + .unwrap_or(0) + } + + /// `max(|negative slots|)` — the falsifier ceiling. + fn falsifier_ceiling(self) -> u32 { + (0..TARSKI_SLOTS) + .map(|s| (-self.get(s)).max(0) as u32) + .max() + .unwrap_or(0) + } +} + +/// Borrowed signed-Tarski view of a dock's 12-byte payload. +fn view_of(dock: &Dock) -> &SignedTarskiWitnessView { + let reg: &[u8; REGISTER_BYTES] = dock[4..16].try_into().expect("12-byte payload"); + SignedTarskiWitnessView::from_register_ref(reg) +} + +/// Write-back per the borrow-strategy law: owned `Copy` microcopy, nibble +/// edit, gated write-back. Never `&mut` a borrowed view. +fn set_slot(dock: &mut Dock, slot: TarskiSlot, depth: i8) { + let mut v = *view_of(dock); + v.set(slot as usize, depth); + dock[4..16].copy_from_slice(&v.to_register()); } fn mint_dock() -> Dock { @@ -98,16 +196,56 @@ fn mint_dock() -> Dock { d } -/// The legacy projection: `support_ceiling = max(positive loci)`. -/// For the positive-only corpus this must equal `Belief::rung` exactly -/// (observed ground = rung 0 = no bound positive locus). -fn support_ceiling(w: &CausalWitnessFacet) -> u32 { - (0..24).map(|s| w.get(s).max(0) as u32).max().unwrap_or(0) -} +/// **The independent positive derivation** — the fix for the withdrawn +/// circular claim. Derives each belief's derivational depth from SUPPORT +/// TOPOLOGY ALONE: `depth(b) = 0` if `b` has no premises, else +/// `1 + max(depth(premises))`. Reads `premises` (the support-DAG edges) and +/// nothing else — **never `b.rung`**, which is the oracle this is checked +/// against, not an input. +/// +/// Returns `None` if the premise graph contains a cycle (the CHOICE +/// replacement path can in principle rewrite premises to point forward); +/// a cycle is reported honestly rather than papered over with a recursion +/// guard that silently returns a wrong depth. +fn derive_depth_from_support(arena: &BeliefArena) -> Option> { + let n = arena.entries().len(); + let mut memo: Vec> = vec![None; n]; + // 0 = unvisited, 1 = on stack, 2 = done + let mut mark = vec![0u8; n]; + + fn walk( + i: usize, + arena: &BeliefArena, + memo: &mut Vec>, + mark: &mut Vec, + ) -> Option { + match mark[i] { + 1 => return None, // cycle + 2 => return memo[i], + _ => {} + } + mark[i] = 1; + let prem = &arena.entries()[i].premises; + let d = if prem.is_empty() { + 0 + } else { + let mut m = 0u32; + for &p in prem { + let dp = walk(p as usize, arena, memo, mark)?; + m = m.max(dp); + } + m + 1 + }; + mark[i] = 2; + memo[i] = Some(d); + Some(d) + } -/// `falsifier_ceiling = max(abs(negative loci))`. -fn falsifier_ceiling(w: &CausalWitnessFacet) -> u32 { - (0..24).map(|s| (-w.get(s)).max(0) as u32).max().unwrap_or(0) + let mut out = Vec::with_capacity(n); + for i in 0..n { + out.push(walk(i, arena, &mut memo, &mut mark)?); + } + Some(out) } fn inh(s: u16, p: u16) -> CStmt { @@ -121,19 +259,15 @@ fn inh(s: u16, p: u16) -> CStmt { /// Scan the closed arena for falsifying derivations the scalar path DROPPED: /// composable premise pairs whose candidate conclusion targets an existing /// belief of opposing polarity (stored expectation > 0.5, candidate ≤ 0.5). -/// Returns, per target statement, the DEEPEST such counter-derivation -/// (`max(r1, r2) + 1` — the same depth law `close_transitive` uses). -/// -/// This is the "falsifier listener": it re-derives with the arena's own -/// public truth functions what `admit_derived`'s CHOICE discards silently. -fn scan_falsifiers(arena: &BeliefArena) -> Vec<(CStmt, u32)> { +/// Depth uses the INDEPENDENTLY-derived support depths, not `b.rung`. +fn scan_falsifiers(arena: &BeliefArena, depth: &[u32]) -> Vec<(CStmt, u32)> { let entries = arena.entries(); let mut out: Vec<(CStmt, u32)> = Vec::new(); - for ei in entries { + for (i, ei) in entries.iter().enumerate() { if !ei.stmt.cop.transits() { continue; } - for ej in entries { + for (j, ej) in entries.iter().enumerate() { if ej.stmt.cop != ei.stmt.cop || ej.stmt.s != ei.stmt.p { continue; } @@ -147,10 +281,10 @@ fn scan_falsifiers(arena: &BeliefArena) -> Vec<(CStmt, u32)> { }; let cand = ei.truth.deduction(&ej.truth); if stored.truth.expectation() > 0.5 + 1e-6 && cand.expectation() <= 0.5 + 1e-6 { - let depth = ei.rung.max(ej.rung) + 1; + let d = depth[i].max(depth[j]) + 1; match out.iter_mut().find(|(s, _)| *s == stmt) { - Some((_, d)) => *d = (*d).max(depth), - None => out.push((stmt, depth)), + Some((_, best)) => *best = (*best).max(d), + None => out.push((stmt, d)), } } } @@ -158,29 +292,28 @@ fn scan_falsifiers(arena: &BeliefArena) -> Vec<(CStmt, u32)> { out } -/// Mint the witness docks for a closed arena: positive lane -/// (`Locus::SupportedBy`) = derivation rung; negative lane -/// (`Locus::Contradiction`) = deepest dropped falsifying derivation. -/// Panics (probe-honesty) if any depth exceeds the i4 ceiling. -fn mint_witness_docks(arena: &BeliefArena) -> ([Dock; MAX_DOCKS], usize) { +/// Mint the witness docks: the positive slot carries the INDEPENDENTLY +/// derived support depth; the negative slot the deepest dropped falsifying +/// derivation. Panics (probe honesty) if any depth exceeds the i4 ceiling. +fn mint_witness_docks(arena: &BeliefArena, depth: &[u32]) -> ([Dock; MAX_DOCKS], usize) { let mut docks = [EMPTY_DOCK; MAX_DOCKS]; let n = arena.entries().len(); assert!(n <= MAX_DOCKS, "probe capacity"); - for (i, b) in arena.entries().iter().enumerate() { - docks[i] = mint_dock(); - if b.rung > 0 { - assert!(b.rung <= 7, "i4 ceiling: rung {} > +7 needs escalation", b.rung); - set_locus(&mut docks[i], Locus::SupportedBy, b.rung as i8); + for (i, dock) in docks.iter_mut().enumerate().take(n) { + *dock = mint_dock(); + if depth[i] > 0 { + assert!(depth[i] <= 7, "i4 ceiling: depth {} > +7", depth[i]); + set_slot(dock, TarskiSlot::ConstructiveDepth, depth[i] as i8); } } - for (stmt, depth) in scan_falsifiers(arena) { - assert!(depth <= 8, "i4 ceiling: falsifier depth {depth} > 8"); + for (stmt, d) in scan_falsifiers(arena, depth) { + assert!(d <= 8, "i4 ceiling: falsifier depth {d} > 8"); let idx = arena .entries() .iter() .position(|b| b.stmt == stmt) .expect("falsifier target exists"); - set_locus(&mut docks[idx], Locus::Contradiction, -(depth as i8)); + set_slot(&mut docks[idx], TarskiSlot::FalsifyingDepth, -(d as i8)); } (docks, n) } @@ -204,7 +337,6 @@ fn build_positive_arena() -> BeliefArena { /// Add a falsifying counter-chain `1→…→5` whose LAST link has frequency 0, /// then re-close. `hops` = number of links (3 → counter-depth 2; 5 → 3). fn add_falsifier_chain(a: &mut BeliefArena, hops: usize) { - // concepts 6.. are counter-branch intermediates let mut nodes: Vec = vec![1]; for i in 0..hops - 1 { nodes.push(6 + i as u16); @@ -224,19 +356,20 @@ fn add_falsifier_chain(a: &mut BeliefArena, hops: usize) { /// Bit-exact scalar-state snapshot of one belief (f32s by bit pattern). /// -/// Premises are EXCLUDED from the snapshot — a measured necessity, not a -/// convenience, and itself charter evidence (BELIEF-ABI-RESTORATION-1 F4: -/// ephemeral indexes leaking into cognitive state). Two IDENTICALLY-built -/// arenas diverge in `premises` at TWO layers, both from `close_transitive` -/// admitting its per-pass `derived: HashMap` in iteration order: -/// 1. **index values** — the same derivation stores different numeric arena -/// indices (observed live: `(1,5)` premises `[6,4]` vs `[5,6]`); -/// 2. **route ties** — equal-expectation derivations (`(1,4)` via -/// `(1,3)∘(3,4)` vs `(1,2)∘(2,4)`) are tie-broken by whichever the -/// HashMap yields first, so even statement-RESOLVED premises differ. +/// Premises are EXCLUDED, for a measured reason: two IDENTICALLY-built +/// arenas diverge in `premises` at two layers, both from `close_transitive` +/// admitting its per-pass `derived: HashMap` in iteration order — +/// (1) the numeric arena indices differ (observed live: `(1,5)` premises +/// `[6,4]` vs `[5,6]`), and (2) equal-expectation derivations (`(1,4)` via +/// `(1,3)∘(3,4)` vs `(1,2)∘(2,4)`) are tie-broken by whichever the HashMap +/// yields first, so even statement-RESOLVED premises differ. /// -/// The epistemically stable scalar state is (stmt, truth, stamp, rung, -/// contradiction); the premise route is nondeterministic decoration. +/// **This is stated as an observation, not a verdict.** It is NOT a claim +/// that the premise route is unimportant: two proof routes with tied truth +/// may later carry different provenance, and a route chosen by hash order +/// is then a real reproducibility problem, not a harmless one. What is +/// established here is only that the route is not currently STABLE, so it +/// cannot serve as a parity key in this probe. fn scalar_state(b: &Belief) -> (CStmt, u32, u32, u64, u32, u32) { ( b.stmt, @@ -258,10 +391,11 @@ fn main() { // ================= Fixture A ================= let arena_a = build_positive_arena(); - let (docks_a, n_a) = mint_witness_docks(&arena_a); + let depth_a = derive_depth_from_support(&arena_a).expect("premise DAG is acyclic"); + let (docks_a, n_a) = mint_witness_docks(&arena_a, &depth_a); // A1 — hand-authored rung expectations (balanced composition: rung is - // ~log2 of span, NOT span length — the #1002 arc's law, restated here). + // ~log2 of span, NOT span length). let expected: [((u16, u16), u32); 10] = [ ((1, 2), 0), ((2, 3), 0), @@ -284,36 +418,58 @@ fn main() { format!("{} statements, rungs 0/1/2 as authored", expected.len()), ); - // A2 — legacy projection parity + negative lane silent in fixture A. + // A2 — THE NON-CIRCULAR PARITY TEST. The positive lane was derived from + // the premise DAG alone (never reading `b.rung`); the arena's stored + // scalar is the ORACLE. Agreement here is evidence that `rung` is + // reconstructible from support topology; disagreement would be the + // finding. (The earlier revision wrote `b.rung` in and read it back — + // that gate proved nothing and is withdrawn.) let mut a2_ok = true; + let mut a2_detail = String::new(); for (i, b) in arena_a.entries().iter().enumerate() { - let w = witness_of(&docks_a[i]); - a2_ok &= support_ceiling(w) == b.rung; - a2_ok &= falsifier_ceiling(w) == 0; + let derived = view_of(&docks_a[i]).support_ceiling(); + if derived != b.rung { + a2_ok = false; + a2_detail = format!( + "DIVERGENCE at {:?}: support-derived {} vs arena rung {}", + b.stmt, derived, b.rung + ); + break; + } + } + if a2_ok { + a2_detail = format!( + "{n_a}/{n_a} beliefs: depth derived from the premise DAG alone equals the arena's \ + stored rung (independent derivation, arena as oracle)" + ); } gate( - "A2 support projection == Belief::rung, falsifier lane silent", + "A2 support-topology derivation reproduces rung", a2_ok, - format!("{n_a}/{n_a} docks: support_ceiling parity, zero negatives"), + a2_detail, ); - // A3 — dock conservation: LE geometry, classid recovery via the shipped - // FacetCascade reading, register identity through the borrowed view. - let mut a3_ok = true; + // A3 — negative lane silent in the positive fixture. + let a3_ok = (0..n_a).all(|i| view_of(&docks_a[i]).falsifier_ceiling() == 0); + gate( + "A3 falsifier lane silent with no counter-chain", + a3_ok, + format!("{n_a}/{n_a} docks carry zero negative slots"), + ); + + // A4 — dock conservation: the same 16 bytes round-trip through BOTH the + // shipped FacetCascade reading and this probe-local Tarski reading. + let mut a4_ok = true; for dock in docks_a.iter().take(n_a) { let fc = FacetCascade::from_bytes(dock); - a3_ok &= fc.facet_classid == PROBE_TARSKI_CLASSID; - // Full LE round-trip through the shipped classid reading: the dock's - // bytes survive the FacetCascade decode/encode unchanged. (NOT - // `tier_bytes()` — that is the coarse→fine hi:lo LADDER view; the - // wire order per tier is `[lo, hi]`, from_bytes' own doc.) - a3_ok &= fc.to_bytes() == *dock; - a3_ok &= witness_of(dock).to_register() == dock[4..16]; + a4_ok &= fc.facet_classid == PROBE_TARSKI_CLASSID; + a4_ok &= fc.to_bytes() == *dock; + a4_ok &= view_of(dock).to_register() == dock[4..16]; } gate( - "A3 dock conservation (classid LE + register identity, both readings)", - a3_ok, - format!("{n_a} docks read identically as FacetCascade and G24N4 view"), + "A4 dock conservation (one geometry, two readings, no byte moves)", + a4_ok, + format!("{n_a} docks round-trip through FacetCascade and the Tarski view alike"), ); let s_apex = inh(1, 5); @@ -328,11 +484,13 @@ fn main() { // ================= Fixture B (falsifier, depth 2) ================= let mut arena_b = build_positive_arena(); add_falsifier_chain(&mut arena_b, 3); - let (docks_b, _n_b) = mint_witness_docks(&arena_b); + let depth_b = derive_depth_from_support(&arena_b).expect("acyclic"); + let (docks_b, _n_b) = mint_witness_docks(&arena_b, &depth_b); // B1 — the falsifier is INVISIBLE to the scalar state: every fixture-A - // belief (apex included) is bit-identical after the counter-chain. This - // is the shipped CHOICE law doing the discarding (belief.rs:247). + // belief is bit-identical after the counter-chain. This is the shipped + // CHOICE law doing the discarding (belief.rs:247). THIS is the probe's + // load-bearing result. let mut b1_ok = true; for b in arena_a.entries() { let after = arena_b.get(b.stmt).expect("fixture-A statement survives"); @@ -345,28 +503,27 @@ fn main() { ); // B2 — the witness RETAINS what the scalar dropped, without touching the - // support lane: apex dock differs from fixture A in EXACTLY the - // Contradiction nibble; +2 support survives beside −2 falsifier. + // constructive lane: the apex dock differs from fixture A in EXACTLY the + // FalsifyingDepth slot. let apex_b_idx = arena_b .entries() .iter() .position(|b| b.stmt == s_apex) .expect("apex in B"); - let apex_b_dock = docks_b[apex_b_idx]; - let wb = witness_of(&apex_b_dock); - let changed_slots: Vec = (0..24) - .filter(|&s| wb.get(s) != witness_of(&apex_a_dock).get(s)) + let vb = view_of(&docks_b[apex_b_idx]); + let changed: Vec = (0..TARSKI_SLOTS) + .filter(|&s| vb.get(s) != view_of(&apex_a_dock).get(s)) .collect(); gate( "B2 falsifier lands beside support (neither overwrites the other)", - wb.at(Locus::SupportedBy) == 2 - && wb.at(Locus::Contradiction) == -2 - && changed_slots == vec![Locus::Contradiction as usize], + vb.at(TarskiSlot::ConstructiveDepth) == 2 + && vb.at(TarskiSlot::FalsifyingDepth) == -2 + && changed == vec![TarskiSlot::FalsifyingDepth as usize], format!( - "apex: SupportedBy {:+}, Contradiction {:+}, changed slots {:?}", - wb.at(Locus::SupportedBy), - wb.at(Locus::Contradiction), - changed_slots + "apex: constructive {:+}, falsifying {:+}, changed slots {:?}", + vb.at(TarskiSlot::ConstructiveDepth), + vb.at(TarskiSlot::FalsifyingDepth), + changed ), ); @@ -376,52 +533,52 @@ fn main() { .iter() .enumerate() .filter(|(i, _)| { - let w = witness_of(&docks_b[*i]); - support_ceiling(w) > 0 && falsifier_ceiling(w) > 0 + let v = view_of(&docks_b[*i]); + v.support_ceiling() > 0 && v.falsifier_ceiling() > 0 }) .map(|(_, b)| b.stmt) .collect(); gate( "B3 dialectical hotspot detection is discriminating", hotspots == vec![s_apex], - format!("exactly one hotspot (the apex), {} beliefs scanned", arena_b.entries().len()), + format!( + "exactly one hotspot (the apex), {} beliefs scanned", + arena_b.entries().len() + ), ); // ================= Fixture B' (falsifier, depth 3) ================= let mut arena_b2 = build_positive_arena(); add_falsifier_chain(&mut arena_b2, 5); - let (docks_b2, _) = mint_witness_docks(&arena_b2); + let depth_b2 = derive_depth_from_support(&arena_b2).expect("acyclic"); + let (docks_b2, _) = mint_witness_docks(&arena_b2, &depth_b2); let apex_b2_idx = arena_b2 .entries() .iter() .position(|b| b.stmt == s_apex) .expect("apex in B'"); - let wb2 = witness_of(&docks_b2[apex_b2_idx]); + let vb2 = view_of(&docks_b2[apex_b2_idx]); - // B4 — the depth discrimination the scalar CANNOT make: apex scalar - // state is identical between depth-2 and depth-3 falsifier worlds - // (zero bits of falsifier depth survive in the arena), while the - // witness field distinguishes them. + // B4 — the discrimination the scalar CANNOT make. let b_state = scalar_state(&arena_b.entries()[apex_b_idx]); let b2_state = scalar_state(&arena_b2.entries()[apex_b2_idx]); gate( "B4 scalar state identical across falsifier depths; witness differs", b_state == b2_state && b_state == apex_a_state - && wb.at(Locus::Contradiction) == -2 - && wb2.at(Locus::Contradiction) == -3, + && vb.at(TarskiSlot::FalsifyingDepth) == -2 + && vb2.at(TarskiSlot::FalsifyingDepth) == -3, format!( "apex scalar bit-equal in A/B/B'; witness −2 vs {:+}", - wb2.at(Locus::Contradiction) + vb2.at(TarskiSlot::FalsifyingDepth) ), ); // ================= Fixture C (falsifier removed) ================= let arena_c = build_positive_arena(); - let (docks_c, n_c) = mint_witness_docks(&arena_c); - // Per-STATEMENT comparison, not per-index: admission order is HashMap- - // nondeterministic (the F4 finding above), so entry i of two identical - // builds need not be the same statement. + let depth_c = derive_depth_from_support(&arena_c).expect("acyclic"); + let (docks_c, n_c) = mint_witness_docks(&arena_c, &depth_c); + // Per-STATEMENT comparison: admission order is HashMap-nondeterministic. let mut c1_ok = n_c == n_a; for (i, b) in arena_a.entries().iter().enumerate() { let ci = arena_c @@ -438,36 +595,48 @@ fn main() { ); // ================= Physical honesty gates ================= - // P1 — the i4 ceiling is +7/−8: depth beyond it CLAMPS, it does not - // widen. Deeper derivations need escalation (ClassView re-election / - // bucket rollover), never a wider nibble in this reading. + // P1 — the i4 ceiling is +7/−8: depth beyond it CLAMPS, never widens. let mut probe = mint_dock(); - set_locus(&mut probe, Locus::SupportedBy, 9); - let clamped_hi = witness_of(&probe).at(Locus::SupportedBy); - set_locus(&mut probe, Locus::Contradiction, -9); - let clamped_lo = witness_of(&probe).at(Locus::Contradiction); + set_slot(&mut probe, TarskiSlot::ConstructiveDepth, 9); + let hi = view_of(&probe).at(TarskiSlot::ConstructiveDepth); + set_slot(&mut probe, TarskiSlot::FalsifyingDepth, -9); + let lo = view_of(&probe).at(TarskiSlot::FalsifyingDepth); gate( "P1 i4 depth ceiling stated honestly (+7/−8, clamp not widen)", - clamped_hi == 7 && clamped_lo == -8, - format!("+9 → {clamped_hi:+}, −9 → {clamped_lo:+}"), + hi == 7 && lo == -8, + format!("+9 → {hi:+}, −9 → {lo:+}"), ); - // P2 — masked election over the signed field is fail-closed and - // discriminating: electing ONLY the support lane reads +2 at the apex - // and refuses the bound-but-unelected falsifier lane. - let support_mask = WideFieldMask::from_positions(&[Locus::SupportedBy as u8]); + // P2 — slot isolation: writing one slot leaves all 23 others unchanged. + let mut iso_ok = true; + for k in 0..TARSKI_SLOTS { + let mut v = SignedTarskiWitnessView::ZERO; + for other in 0..TARSKI_SLOTS { + if other != k { + let d = ((other as i32 % 15) - 7) as i8; + v.set(other, if d == 0 { 1 } else { d }); + } + } + let before: Vec = (0..TARSKI_SLOTS).map(|s| v.get(s)).collect(); + let distinctive = if k % 2 == 0 { 7 } else { -8 }; + v.set(k, distinctive); + iso_ok &= v.get(k) == distinctive; + for (other, &prior) in before.iter().enumerate() { + if other != k { + iso_ok &= v.get(other) == prior; + } + } + } gate( - "P2 locus election reads support, refuses unelected falsifier", - wb.elected(&support_mask, Locus::SupportedBy) == Some(2) - && wb.elected(&support_mask, Locus::Contradiction).is_none() - && wb.elected(&WideFieldMask::EMPTY, Locus::SupportedBy).is_none(), - "elected(SupportedBy)=+2; Contradiction unelected → None; EMPTY fail-closed".to_string(), + "P2 slot isolation across all 24 nibbles", + iso_ok, + "a write to slot k leaves every other slot bit-identical".to_string(), ); println!("PROBE-TARSKI-SIGNED-WITNESS-1: ALL {pass} GATES GREEN"); println!( - "verdict: Belief::rung is the positive-lane projection of a signed \ - G24N4 derivational field; the falsifier lane carries what the \ - shipped CHOICE law provably discards" + "measured claim: a signed i4 derivational witness PRESERVES falsifier depth that the \ + Belief scalar state provably discards (B1/B4); and on this fixture the constructive \ + lane derived from support topology alone reproduces the arena's rung (A2)" ); }