probes: a signed derivational witness preserves falsifier depth the Belief scalar discards - #1007
Merged
Merged
Conversation
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KCGhDYoQBXs3poaR7sFuqp
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_64dc762b-d1f9-4eaa-b91f-3a12b41c10a7) |
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Plus Run ID: Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
… 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KCGhDYoQBXs3poaR7sFuqp
AdaWorldAPI
pushed a commit
that referenced
this pull request
Aug 23, 2026
Addresses the review of #1006. The audit findings stand; two conclusions drawn from them did not. 1. WITHDRAWN: "mint a FacetCascade address per belief position (even a trivial per-arena-position one), implement one accumulate fold, check whether it reproduces the arena." That is backwards. An address derived from arena POSITION turns a Vec index into a pretty 16-byte Vec index -- still a second physical belief universe, now wearing the canonical address format as camouflage. An address must come from the canonical node/relation identity or it is not an address; inventing one to make a hypothesis testable invents the result too. Recorded as withdrawn in place rather than deleted, so it is not re-derived. 2. CORRECTED OVERSTATEMENT on premises. Established: real cardinality <= 2 (11 admit_derived call sites, 4 tactics mint sites, all arity <= 2), so this is not the "cardinality = more rows" case. NOT established, and previously implied: that two u32 premise identities FIT in two 8:8 tiles, still less two signed i4 nibbles. Cardinality and physical width are different facts. A u32 arena index is not an address; whether the identity it stands for is expressible in a tile or a nibble depends on a locality/address transformation nobody has designed. The width question is OPEN and belongs to step 2. 3. The two operator-ruled items are restated as HYPOTHESES awaiting the step 2 ruling, not directions awaiting implementation: - rung = HHTL depth: the answerable question is whether derivation depth is reconstructible from SUPPORT topology, which needs no address at all. (Since measured on one fixture -- #1007 gate A2, 10/10 -- but that is evidence about support topology, not HHTL depth, and one fixture is not a general result.) - stamp = accumulation: any replacement must reproduce Stamp's load-bearing IDENTITY semantics (disjointness, overlap, source-set union, no-double-count, belief.rs:39-48). A generic commutative fold is not automatically a source-set union. The [ABSENT] verdicts themselves -- no Belief is ever minted an HHTL/FacetCascade address; no children-and-siblings accumulate fold exists anywhere -- are unchanged, and remain the audit's actual output. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KCGhDYoQBXs3poaR7sFuqp
AdaWorldAPI
changed the title
This was referenced Aug 23, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two probes over shipped types. Recut after review (commit
f990e0b) — one headline claim withdrawn as circular, one semantic-contract violation fixed, plus the rustfmt failure.What was wrong, and what changed
1. A9 semantic-contract violation (the important one). Both probes wrote derivational magnitudes through
Locus::SupportedBy/Contradiction.CausalWitnessFacet's A9 reading is operator-locked "loci, not magnitudes" — every namedLocusis 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; acknowledging it in a doc comment did not make it lawful.Fixed with a probe-local
SignedTarskiWitnessView([u8; 12])— own slot names (TarskiSlot::{ConstructiveDepth, FalsifyingDepth}), own nibble accessors, 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 in the Tarski register, the mediator POINTER 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_dockstookb.rung, wrote it into a nibble, then checked the nibble equalledb.rung— proving only that an i4 field can hold 0..7. Withdrawn by name in the module docs.Replaced with
derive_depth_from_support(): depth from the premise DAG alone (0if no premises, else1 + max(depth(premises))), never readingb.rung; the arena's stored scalar is the oracle it's checked against. ReturnsNoneon 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.3.
CausalRowis labelled a PROBE FIXTURE in the type doc, honesty box, and verdict line. It is an AoS test object and is never evidence about the resident SoA layout.4. The premise-route nondeterminism finding no longer calls routes "decoration." Two proof routes with tied truth may carry different provenance, so a route chosen by
HashMaporder is a real reproducibility question. What's 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 -- --checkis now clean — the original commit ran clippy but never fmt, which is what Style Check caught.The measured claim, at the strength the evidence supports
PROBE-TARSKI-SIGNED-WITNESS-1 — 11/11. The load-bearing results are the negative ones: B1 — a falsifying counter-derivation is invisible to the scalar state; the shipped
admit_derivedCHOICE law (belief.rs:247, strict-expectation-gain only) drops it, and every fixture-A belief is bit-identical afterward. B4 — two falsifier depths (2 vs 3 hops) are scalar-identical in the arena, zero bits of depth surviving, while the witness distinguishes them. Plus A2 (non-circular parity), A3/B2/B3 (silence and discrimination), C1 (byte-identical restore), P1/P2 (i4 ceiling clamps not widens; slot isolation across all 24 nibbles).PROBE-FOUR-PLANE-CAUSAL-MEDIUM-1 — 7/7. 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. FP3 — a falsifier in the evidence plane does not flipCausalTopologyorReasoningBand. FP6 — the true-mediator intervention closes the loop: binds theKausalpointer, upgradesIndirectUnknownIntermediates → IndirectKnownIntermediates, leaves magnitude/band/address bit-identical.Scope, stated honestly
The four-plane "world" is a known 3-event toy oracle. This tests the ABI representation loop, not causal discovery. Whether this geometry helps discover structure that predicts unseen interventions (Uhler-style CRL) is the external falsifier and is out of scope.
Probe-local classids (
0xFFFF_0009/000A/000B) are placeholders, never OGAR mints. No tenant. No layout change.