diff --git a/.claude/board/entries/2026-10-30-coresearch-mistaber-hydration.md b/.claude/board/entries/2026-10-30-coresearch-mistaber-hydration.md new file mode 100644 index 000000000..e78c52625 --- /dev/null +++ b/.claude/board/entries/2026-10-30-coresearch-mistaber-hydration.md @@ -0,0 +1,194 @@ +# 2026-10-30 — Co-research: Mistaber holdings as hydrated nodes, the KJV way + +**Status:** EXPLORATION MAP. Nothing is adopted; the operator chooses. Follows D-MIST-NATIVE-0 (#1873). + +## Question + +How should Mistaber's worlds, propositions, rules and makor citations become addressed SoA nodes the way the KJV is hydrated in `deepnsm-v2`? In that path, `toc::spawn` mints the outline tree, `hydrate::hydrate` addresses each triple at its verse node, and `promote` writes basins at node keys. What does that buy? + +The operator ruled "we don't use Strings": identities are addresses or nodes. The probe still interns names (`Interner(Vec)`). The operator added `contract::revision` (`GadamerRevision`) mid-run. + +## Premise audit (PREMISE-SPLIT) + +The question names three concepts, and each has its own signature. They must not be answered as one. + +| concept | what it is | where it goes | +|---|---|---| +| makor citation | a literary position, like a KJV verse | a TOC node | +| world | an authority scope; accessibility is a multi-parent DAG | an id carried as a value, plus edges | +| holding | a conclusion derived per (proposition, world) | a derived cell; its lineage points at rule and makor nodes | + +A KJV triple is an observation made at a verse; a holding is a conclusion made at an authority. Filing the second under the first's mechanism would be wrong. + +## Anchors + +- No String as identity (operator; D-ARG-1..3, `STATUS_BOARD.md:428-435`). +- Canonical node `16|16|480`: position in the key, summaries in value lanes; V3 mint only. +- Scale is the next cascade level, never a wider field. +- Classids come from the OGAR codebook; worlds are values. +- Authority worlds are not Thought-Git branches. +- The stable-model fragment stays with Clingo. +- No licensing discussion in public artifacts. + +## Crosswalk and verdicts + +Sources (scouts): `toc.rs`, `hydrate.rs`, `promote.rs`, `hhtl.rs`, `causal_audit.rs`, `revision.rs` and the probe (VERIFIED-IN-CODE); the Sefaria index and shape API (fetched); CTS URN and PROV-O (SECTION-READ); arXiv 2202.10766, 2303.12773, 2608.21141, 2505.01944 and Dong et al. VLDB 2009 (SECTION-READ); Soufflé (SECTION-READ); Akoma Ntoso (ABSTRACT-ONLY). + +| # | idea | evidence | verdict | +|---|---|---|---| +| X10 | **Names → label-codebook ids, unknown labels refused** | The probe's `Interner(Vec)` and `WitnessEntry.source_url: Option` both violate D-ARG-1. `promote::key_at` already mints via `mint_for` and refuses V1 keys (`promote.rs:99-115`). D-ARG-1..3 are Queued upstream. | **PROBE** (P10), after D-ARG-1..3 | +| X1 | **makor → TOC node; the capacity limit was misread (corrected by the operator)** | The council said: `toc.rs` gives 2 nibbles per level with a cap of 255 (`toc.rs:47-64,111-118`), Shulchan Arukh YD has 403 simanim (largest seif count 146, at siman 331, from Sefaria), and the key holds only 12 path nibbles. **The 12 is wrong for V3 keys.** A V3 key carries four tiers (heel/hip/twig/leaf): `promote::tiers_of` folds a full 16-nibble `NiblePath` into them (`promote.rs:61-70`; `MAX_DEPTH = 16`, `hhtl.rs:45`). The 3×4 reading applies only to V1 keys. **A level's 255 cap is also not fixed.** A level value can be a 9-bit codec9 lane: u8 magnitude + presence bit = 511 numeric values + the never-touched sentinel (`ndarray::hpc::codec9`, contract `lane_codec` 9-bit lanes). So siman 403 fits one level with no wider nibble path. Current codec9 is the signed DR512 form (±255). An unsigned U9 reading of the same 9 bits is the operator's proposal and has no symbol yet. Ordinal 0 must never encode: P=0 with magnitude 0 is NEVER_TOUCHED. A hilchot level stays optional, as literary structure for basins, not for capacity. The outline code is KJV-specific: it has no level-schema parameter and no generic citation→path mapper (closed search `crates/**/*.rs`). | **PROBE** (P1, revised) | +| X3 | **Worlds as value ids plus an edge DAG, never key prefixes** | `ashk_ah` has two parents (mechaber, rema), but key-prefix ancestry is a tree. The probe already holds accessibility as a 64×64 relation register. D-ACR-12's tree ascent must not be reused for world inheritance. | **ADOPT-NOW** as the design rule; no code | +| X4, X5 | **Holdings point at positions; two lineages stay two edges** | Every system surveyed makes derived facts reference source positions, never live at them. PROV separates `wasDerivedFrom` (world inheritance origin) from `hadPrimarySource` (rule → makor). The probe already computes the two lineages as separate fixpoints. What is missing: lineage values are rule ids, not node addresses, and there are no makor nodes. | **PROBE** (P3) | +| X6 | **SupportLedger counts a quoting source as distinct** | `causal_audit.rs:268-271`: "this ledger has no derived-from link". INDRA lists the derived-from link as OPEN. Interim, with no contract change: key `source` by the attestor (makor or author), never by world. The derived-from slot itself is a contract change, owned by the contract tier and needing operator sign-off. | interim **PROBE** (P4); contract slot **PARK** (owner decision) | +| X9 | **GadamerRevision as the independence policy** | Copied endorsement = inherited root, giving Echo / NoIncrease. Independent observation = a new independent root, giving IncreaseEligible. A machloket = `unresolved_tension`, which accumulates by union and is never cleared (`revision.rs:358-440,428`). Map the ENCOUNTER onto the horizon, never the world: `InterpretiveHorizon` is a reader's state (awareness, question, revision_index), and putting a world inside it is a trap. Bible lanes being inherited calque (operator, 2026-10-04) is the same pattern. | **PROBE** (P8) | +| X12 | **Mistaber goldens as copied-source fixtures for E4 / D-EBM-4 / D-EBM-9** | These gates are specified but not built (`cartesian-epistemic-self-model.md:249-257`; D-EBM scratchpad). Caught by the falsifier designer: C6 vs C6i cannot distinguish attestor-keying from world-keying, since both give 1 vs 2. Only the F1 diamond does: at (p,e), attestor-keyed gives 1 source, world-keyed gives 2. New fixtures needed: C6m (own makor, expect 2), V47-copy (expect 1), V47-indep (expect 47), E4-dup (expect 1). | **PROBE** (P4) | +| X11 | **Basin at the makor/TOC node key, `subject` as a codebook id in a value lane** | Hermeneutik fix vs the subject-keyed D-ACR-6 rail. Promote at the TOC key; `subject` goes in a value lane and never becomes a second key. A size-preserving label-shuffle null is mandatory (E-BASIN-WIDTH-IS-N-ARTIFACT-1). The Mistaber goldens are too small, so this runs on KJV first. | **PROBE** (P5) | +| X8 | **Negative lineage (why a holding does NOT hold)** | Positive-only lineage is incomplete under `not` (2608.21141). The probe records no lineage for `overridden(p,c)`. Restrict to the stratified fragment; anything else is refused and left to Clingo. | **PROBE** (P7) | +| X13 | **Stable identity separate from path** | `promote::key_at` derives the key from the path, so renumbering a seif silently re-addresses a different unit. Needs a per-edition path→identity registry. Akoma Ntoso eId/wId is only a lead (abstract-only). | **PROBE** (P9, a census first) | +| X2 | **Commentaries are separate linked works** | Shach and Taz are each both a commentary (text) and a world (authority); the Rema's gloss is not the `rema` world. `toc` has no linked-work edge. | **PARK** until P6's link-density census | +| X7 | Count source sets, not derivation coefficients | Already how the probe and `revision.rs` work (2202.10766). | **SKIP** (ALREADY-HAVE) | +| X14, X15 | Soufflé rule+height per tuple; LegalRuleML / DDL split | Confirm existing choices. | **SKIP** (ALREADY-HAVE) | +| X16 | Probabilistic copy weighting, (1−c)^outdeg | Conflicts with the deterministic substrate and Gadamer's exact zero weight for echoes. | **SKIP** (CONFLICTS-ANCHOR) | +| X17 | world as `prov:Agent`; holding as an annotation body; override as `wasInvalidatedBy` | Each conflates two of the three signatures. | **SKIP** (CONFLICTS-ANCHOR) | + +## Named probes (pre-registered; none run) + +- **P1, siman capacity (revised).** A 2-nibble, 255-cap level must give exactly 148 refusals for simanim 256..403 and 0 silent aliases. That is the control, showing the cap is real. A 9-bit codec9 level must give 0 refusals and 403 distinct, round-tripping keys. Every SA YD citation must resolve within `MAX_DEPTH = 16`, and its key must read back the same path via `tiers_of`. Ordinal 0 must be refused, never encoded as NEVER_TOUCHED. Disable runs: drop the presence bit (red: 148 aliases or refusals); encode ordinal 0 (red: a citation reads as never touched). +- **P3.** The goldens give identical lineage with node addresses as with strings. +- **P4, independence.** On F1, (p,e) attestor-keyed = 1; switching to world-keying must go red. C6m = 2; V47-copy = 1; V47-indep = 47; E4-dup = 1. +- **P5.** Literary-unit basin vs subject basin against a size-preserving shuffle null on KJV. Kill at ≤ 95th percentile. Fully shuffled control must fail; planted fixture must pass. +- **P6.** Commentary link density, measured before building any `comments_on` edge. +- **P7.** `why_not(r(1,2), curated)` on E-xlog-override returns the override plus the suppressed `r_R_0` support. `why_not(p, c)` on F1 returns `override(c,p)` plus base support. The other five curated propositions return nothing. +- **P8.** C6 → Echo / NoIncrease. C6i → exactly one new root. A machloket fixture leaves `unresolved_tension` uncleared. +- **P9.** Renumbering census across SA editions; then renumber one seif and require that lineage still resolves to the same node. +- **P10.** Unknown labels refused, with exact counts. Disable run: a hash fallback. + +## Addendum: the HHTL16 two-tenant opt-in format (operator, 2026-10-30) + +The operator named the opt-in format: tenant 1 is an `is_a` zipper chain (a distinguished-name chain or a NodeGuid), tenant 2 is `part_of`. Tenant 2 ideally matches tenant 1 vertically, but it may also carry one-to-many, location or membership. Read against the code and the plans: + +- `rail_geometry.rs` already reads two rails per row: `RailAxis::{Taxonomy, Mereology}`, with `RailCarving::AxisSlab` giving 12 levels plus a 12-level continuation, one byte per level (VERIFIED-IN-CODE). `dual_rail_placement` places by the primary rail and overlays the secondary. +- A slot byte stores `1 + index`; 0 is the hole that ends the chain (`read_path`). So a byte level holds **255** children. +- The capstone plan files the 16 × 8-bit ISA and PART_OF zippers as a proposal, not ABI, and says the two must not be composed automatically (`d-qr-abi-classview-rails-capstone-v1.md` §2). + +**Reading: HHTL16, the opt-in format (operator, 2026-10-30).** What the code already defines: + +- The HHTL16 Cartesian address is `Morton8x8` (`contract/src/morton8x8.rs`, VERIFIED-IN-CODE): an `(x, y)` byte pair interleaved into one `u16` Z-order code. Each hex nibble is one 4 × 4 refinement, fan-out 16, and `nibble_climb` reads the trie ascent from `a XOR b`. +- The D-DRDT amendment names it: "DR = HHTL16 Cartesian addressing" (`d-drdt-dr-dt-ownership-amendment-v1.md`). +- `dr-math-binding-probe/src/hhtl16.rs` reads a bound DR64 register through it. `row` gives the identity orientation and `column` the property orientation, and `rotate_yz` is an address map over the one stored relation, never a copy. Measured in D-DRCA-1. +- The capstone plan proposed the vertical zipper: `HHTL16ISA[16]` and `HHTL16PartOf[16]`, 16 × 8-bit each, with persisted-vs-view left open on EXO-50 (`d-qr-abi-classview-rails-capstone-v1.md` §2, §5). The operator has now named it the opt-in format. + +Zipped vertically, column `k` is `Morton8x8::from_xy(isa[k], partof[k])`: one exact 64k address. Column 1 is the node's identity and columns 2–16 are 15 exact addresses. That is 32 bytes and 16 Morton codes, and each column climbs its own 4-level nibble trie. + +```text +HHTL16ISA 1234567890123456 (x bytes) +HHTL16PartOf 1234567890123456 (y bytes) +column k = Morton8x8::from_xy(isa[k], partof[k]) +``` + +**Placement: the two Register128 rails** (operator pointer, read in `canonical_node.rs` and `register128.rs`). `ValueTenant::Register0` sits at row bytes 252..268 and `Register1` at 268..284 (D-LXC-29). Each is 16 raw content-blind bytes with **no classid inside**, which is unlike the Facet96 lanes (`Tekamolo`, `CausalWitness`), whose first four bytes are a classid. So column 1 can be a 2-byte identity without colliding with a classid. Meaning comes from the SPOG context the population was resolved under. The slab must declare `SlabReading::Register128`, and `ResolvedReading::bind_register128` binds it once, refusing any other slab. + +- `Register0` = `HHTL16ISA` (x bytes) +- `Register1` = `HHTL16PartOf` (y bytes) +- column `k` = `Morton8x8::from_xy(R0[k], R1[k])` + +The opt-in is the slab declaration, so a class that does not declare it keeps its other readings. + +**Classid per population, not per row (operator, 2026-10-30): for a monotonic corpus the classid goes into the metadata envelope.** What the code already gives (`hotplug.rs`, read in full for 200–470): + +- the slab's metadata envelope carries a `u8` reading tag (`SlabReading::from_tag`); +- `Activation::resolve_for_context(concept, slab)` is resolved once per population, never per row; +- `bind_register128` returns `RegisterLanes` that carry that concept: "that concept, not anything in the register bytes, is the registers' semantic identity". + +A population where every row has one class therefore pays zero classid bytes per row, and all 16 columns stay addresses. + +Two things to settle when this is built: + +- `SlabDeclaration` says of itself "Physical facts only — no concept, no classid, no ontology: the SPOG context supplies those". Putting the classid literally inside the declaration reverses that sentence, so it needs a decision. The alternative is a population-level concept beside the declaration, which is the shape `resolve_for_context` already takes. +- Monotonic means one class per population. Makor, rule, world and holding nodes are four classes, so they form four populations, each resolved once. + +**The Kripke probe is already DR64-shaped.** Its `Rows = [u64; 64]` registers (accessibility, holds, block) are the registers `hhtl16` reads. `cell(Morton8x8::from_xy(world, proposition))` reads one holding. `column` gives the worlds that hold a proposition, `row` gives the propositions a world holds, and `rotate_yz` switches between the two without copying. The HHTL16 codes of the rows above are the global identities that `LocalMap` maps onto the 64 local coordinates. + +| Mistaber node | column 1 (identity) | columns 2–16 (exact addresses) | overflow | +|---|---|---|---| +| makor citation `sa("yd:87:3")` | the seif | its siman, chelek and work | none | +| rule `r_…` | the rule | its world scope (one, by `scope/2`) and every makor it cites | more than 15: refused, counted | +| world | the world | every parent world (`ashk_ah`: mechaber and rema) | more than 15: refused, counted | +| holding | (proposition, world) | immediate rule, source rule, origin world, the source rule's makorot | more than 15: refused, counted | + +This replaces the earlier table, which kept a rule's extra makorot and `ashk_ah`'s second parent as edges outside the rails. In-row columns carry them. X3 changes from "worlds as value ids plus an edge DAG" to "worlds as identities whose parents are in-row addresses". The DR64 fixpoint still computes holdings; it reads parents from the rows instead of a separate register. + +**The vertical match is free in this corpus.** Mistaber lays out `dsl/corpus/yd_87/seif_3.hll`, so a rule's `part_of` chain (file → seif → siman) and its makor's DN chain name the same positions. Under the operator's format this is the ideal case. It is still two rails, never one composed relation. + +**Capacity: settled.** With each of the 16 columns a `(u8:u8)` pair, every column addresses 64k positions. All 3,701 YD seifim, every siman and every commentary seif katan get exact addresses. The earlier one-byte-per-level reading, and the "last two bytes as the leaf" step that followed it, are superseded by the reading above. A hilchot level remains optional, for basin structure only. + +X1 and P1 are amended accordingly: P1's 9-bit arm is replaced by a pair-address arm (3,701 distinct seif addresses, 0 refusals, 0 aliases; disable run: read one byte of each pair → aliases). + +**P11 (new, pre-registered, not run).** On F1 and the C-mammal goldens, give every rule, world and makor node both rails and check: + +- (a) `is_ancestor_of` on tenant 1 reproduces citation containment exactly (seif ⊂ siman ⊂ chelek); +- (b) tenant 2 gives each rule exactly one world, the one `scope/2` names; +- (c) `ashk_ah` carries both parents as in-row addresses, and the fixpoint reads them from the row; +- (d) holdings are unchanged (11/11 goldens). + +Disable runs: + +- compose the two rails, so a rule inherits its makor's chain: (a) or (b) must go red; +- drop `ashk_ah`'s second address: (c) and the goldens must go red. + +## Addendum: property inheritance and the syntax tenants (operator, 2026-10-30) + +The operator pointed at two more organs: the episodic-witness basins (24 × i4) for property inheritance over a mammal taxonomy, and the Markov context build (relative-pronoun anaphora pointers, 24 × i4 syntax resolution, the TEKAMOLO tenant). Checked against code: + +- `contract::causal_witness::CausalWitnessFacet` reads a 12-byte register as 24 signed i4 loci, each an offset in −8..+7 inside the `temporal.rs` window, with 0 meaning unbound. It is labelled EXPERIMENTAL, not in the §3 catalogue. There are 16 named loci; 8 are reserved. They include `Antecedent` (relative pronoun to its antecedent), `BasinAnchor` (the `part_of:is_a` basin), `SupportedBy` / `Supports`, `Quorum` and `Contradiction`. +- `deepnsm-v2::wave` resolves inside ±8 and returns `Escalate` when the offset overflows. +- `contract::tekamolo_facet::TekamoloFacet` reads the same 16-byte facet in `G4D3`: four 256:256:256 lanes (Temporal, Kausal, Modal, Lokal). All-zero means unaddressed. +- `cognitive-shader-driver/examples/ontology_agreement_probe.rs` already folds property claims as three quorums over a `NiblePath` hierarchy: local (the node and its siblings), up (ancestors) and down (descendants). Its fixture holds mammal > placental (dog, cat, whale, bat) and monotreme (platypus, echidna), with properties fur, eggs, flight and milk. Whale fur and platypus eggs are its named conflicts. + +**Two inheritances; keep them apart.** + +| | taxonomic (`is_a` rail) | Mistaber (Kripke worlds) | +|---|---|---| +| question | does whale inherit `terrestrial` from mammal? | does observer `reader` hold `lays_eggs(platypus)` from `obs1`? | +| axis | tenant 1, the class chain | accessibility register (edges) | +| default and exception | up/down quorum; `Contradiction` / BasinConflict (whale is not terrestrial, platypus lays eggs) | inherited unless `asserts`, `endorses` or `overridden` at the child | +| organ | `ontology_agreement_probe` quorums + witness loci | the DR64 fixpoint (#1873) | + +The C-mammal goldens already use both axes at once: the proposition's subject (`platypus`) is a class node, and the worlds (`obs1`, `obs2`, `reader`) are observers. Mistaber's own crosswalk refuses "taxonomy → worlds" as a category error. So the combination is a pair: (class node on the `is_a` rail, proposition) is held per world. It is never a world placed in the taxonomy. + +**The syntax tenants serve encoding, not solving.** TEKAMOLO lanes and `Antecedent` loci describe the source TEXT of a seif. They map onto two of Mistaber's four encoding-decision types: + +- event identification: which clause is legally salient, and what a relative pronoun refers to; +- feature selection: time, cause, manner and place conditions become rule-body features. + +They do not touch the fixpoint. + +**Limit found:** the TEKAMOLO heuristics are German only. `de/tekamolo.tsv` is the one lexicon in `deepnsm-v2` (closed search over its tracked files), and its own docs say German forms ground German text and nothing else. The Shulchan Arukh is Hebrew, and Sefaria's translation is English. Either lexicon must exist before the tenant can read a seif; otherwise every lane reads unaddressed. + +**Still open:** which register the operator's "24 × i4 flavours" names. The board left this open on 2026-09-01: `atoms::I4x32` matches the name, and the 24-nibble facet matches the count. This note uses `CausalWitnessFacet` because it is the 24 × i4 basin and anaphora reading in code. + +- **P12 (pre-registered, not run).** Put the C-mammal subjects on an `is_a` rail (mammal > placental > {whale, elephant, fox}; marsupial > {wombat, possum}; monotreme > platypus). Run the up/down quorum for `terrestrial` and `lays_eggs`. Expected: whale `terrestrial` → Contradiction; platypus `lays_eggs` → BasinConflict up, and corroborated locally once echidna is present. The Mistaber goldens must stay 11/11. Disable runs: + - read a world as a taxonomy ancestor: a golden goes red; + - drop the `Contradiction` locus: whale reads terrestrial. +- **P13.** Census first: how many SA YD seifim in the English translation contain a relative pronoun whose antecedent lies beyond ±8 tokens. That count tells whether `Escalate` or the window carries most of the anaphora before any lexicon is built. + +## Open points for the operator + +- **Undeclared worlds.** Should an undeclared world be refused? Upstream derives `holds(p,x)` for an undeclared child world (golden F6). A native refusal would be a declared divergence from the golden, not a pass. +- **Siman capacity.** Settled (operator, 2026-10-30): the last two bytes of each HHTL16 rail form a `(u8:u8)` 64k leaf. Still open: is a hilchot level wanted for basin structure, and where would its boundary data come from? +- **SupportLedger derived-from slot.** Contract change; owner and timing. +- **D-ARG-1..3.** Prerequisite for X10. Owner and order. + +## Not searched + +- Sefaria's actual hilchot boundary data for YD. +- Other SA sections (OC, EH, CM) and their capacities. +- Commentary seif-katan counts. +- The OASIS Akoma Ntoso spec itself. +- Any ontology beyond PROV-O, FRBR, CTS and Web Annotation. +- Mistaber's own HLL makor grammar beyond `sa("yd:N:M")`. + +## Closeout + +STATUS: done (map only; X1 corrected by the operator: 16 levels, codec9 9-bit levels; HHTL16 two-tenant mapping added, P11; taxonomy-vs-world inheritance split and syntax tenants, P12-P13) | OUTCOME: three-axis split (makor node / world value + DAG edges / holding derived); ten probes named; one ruled interim (attestor-keyed source) | OPEN: undeclared-world policy, hilchot data, SupportLedger derived-from owner, D-ARG-1..3 order. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 23dde95af..755adcead 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -511 entries, 2026-08-06 .. 2026-10-30. +512 entries, 2026-08-06 .. 2026-10-30. | date | entry id | finding | file | |---|---|---|---| @@ -38,6 +38,7 @@ exactly one of them, never both. | 2026-10-30 | `D-LITHO-1` | | [2026-10-30-d-litho-1-xlog-register-steps-and-bag-fixture.md](2026-10-30-d-litho-1-xlog-register-steps-and-bag-fixture.md) | | 2026-10-30 | `D-DT64-6-BS` | | [2026-10-30-d-dt64-6-bs-bind-store-crate.md](2026-10-30-d-dt64-6-bs-bind-store-crate.md) | | 2026-10-30 | `D-DRCA-3` | | [2026-10-30-d-drca-3-dr4-method-routing.md](2026-10-30-d-drca-3-dr4-method-routing.md) | +| 2026-10-30 | `coresearch-mistaber-hydration` | | [2026-10-30-coresearch-mistaber-hydration.md](2026-10-30-coresearch-mistaber-hydration.md) | | 2026-10-29 | `palette512-turbovec9-nsl-worksteal` | | [2026-10-29-palette512-turbovec9-nsl-worksteal.md](2026-10-29-palette512-turbovec9-nsl-worksteal.md) | | 2026-10-28 | `thought-layers-nan-skip` | | [2026-10-28-thought-layers-nan-skip.md](2026-10-28-thought-layers-nan-skip.md) | | 2026-10-28 | `lane-layout-from-classview` | | [2026-10-28-lane-layout-from-classview.md](2026-10-28-lane-layout-from-classview.md) | diff --git a/.claude/plans/d-mistaber-native-v1.md b/.claude/plans/d-mistaber-native-v1.md index bd144e92c..18671adde 100644 --- a/.claude/plans/d-mistaber-native-v1.md +++ b/.claude/plans/d-mistaber-native-v1.md @@ -74,7 +74,7 @@ A lens row is one (mode, source rule), or one (mode) with empty rule fields when ## 5. Evidence (D-MIST-NATIVE-0) -`cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml`: 11 tests. +`cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml`: 12 tests. Goldens: F1-modes, F1-reversed, F2-cycle, F5-gates, F6-undeclared-child, C-mammal-C2/C4/C6/C6i, E-xlog-plain/override. All are exact, compared as sorted lists, so a duplicate atom would also fail. @@ -101,3 +101,31 @@ No timing was taken, and none is claimed. `mistaber-rs` §7 defers mask folds (c ## 7. Not in scope A port of the HLL compiler or Clingo. Stable-model semantics. Any CE64 bit, any Epi5 code. Writes to `BrainyBlaze/mistaber`. + +## 8. Mistaber on DR64³ (2026-10-30, lab test, no new type) + +The probe's registers are DR64² in the D-DRDT sense: row = proposition (64), bit = world (64). They are read through the HHTL16 address `Morton8x8::from_xy(p, w)` (`dr-math-binding-probe::hhtl16::cell`). The lineage already lives on three logical 64 × 64 × 64 index spaces, each a stack of DR64² slices along a third axis: + +| cube | third axis | cell `(z, p, w)` | stored? | +|---|---|---|---| +| V | parent world | `holds_via(inherited(z), p, w)` = `holds[p]∋z ∧ children[z]∋w ∧ ¬block[p]∋w` | no; it is the uncontracted iteration space of `compose`, built on demand | +| O | origin world | `inheritance_source(p, w, z)` | yes, `Holdings::origins` | +| L | rule | `holds_via_rule` source rule `z` of `(p, w)` | yes, `Holdings::sources` | + +Contracting V or O over the third axis (OR over `z`) gives the `holds` register back: `direct ∪ ⋃_z V[z] = holds` and `⋃_z O[z] = holds`. L does not contract to `holds`, because a holding can have no rule (F1 `g` in `a`). Bag multiplicity is the count along the third axis of V × L. The Set projection is the contraction. + +**Test:** `tests::the_third_axis_contracts_back_to_holds`, over all 11 goldens. It also checks that every cell of all three cubes reads the same through its HHTL16 address. Anti-vacuity: at least one cell has two parents (the F1 diamond) and at least one has two origins. + +**Disable runs** (committed first, then each broken, red, restored): + +- drop `¬block` from `inherited_from`: red, `E-xlog-override V`, `left: 3, right: 1`; +- drop the last origin world: red, `F2-cycle O`, `left: 0, right: 4`. + +**Axis typing, a data point for NFR-OP-2.** The D-DR256 Amendment A working model reads DR #3 as Identity × Property, with the third axis indexing a relation ordinal for the Identity × Identity view. Mistaber needs two kinds of third axis: + +- two cubes (V, O) have an Identity third axis: a world; +- one cube (L) has a rule ordinal, closer to a method or relation ordinal. + +So "the third axis is a relation ordinal" covers L and not V or O. Closing NFR-OP-2 stays the DR owner's decision. + +**Size.** Dense, each cube is 32 KiB of bits, 96 KiB for the three. The probe stores only O and L, and only as many slices as there are worlds and rules. V is never stored, because every V slice is one `compose` row read. Nothing here allocates a cube. diff --git a/crates/mistaber-kripke-probe/src/lib.rs b/crates/mistaber-kripke-probe/src/lib.rs index 551d37755..c0cf365b6 100644 --- a/crates/mistaber-kripke-probe/src/lib.rs +++ b/crates/mistaber-kripke-probe/src/lib.rs @@ -563,6 +563,73 @@ impl Holdings<'_> { mod tests { use super::*; + fn all_goldens() -> Vec { + let dir = std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("goldens"); + let mut paths: Vec<_> = std::fs::read_dir(dir) + .unwrap() + .map(|e| e.unwrap().path()) + .filter(|p| p.extension().is_some_and(|x| x == "tsv")) + .collect(); + paths.sort(); + paths + .iter() + .map(|p| parse_golden(&std::fs::read_to_string(p).unwrap()).unwrap()) + .collect() + } + + /// The probe's lineage already lives on three 64 x 64 x 64 index spaces, + /// each a stack of 64 x 64 registers (row = proposition, bit = world) + /// along a third axis: + /// + /// - V[parent]: `holds_via(inherited(parent), p, w)`, built on demand; + /// - O[origin]: `inheritance_source(p, w, origin)`; + /// - L[rule]: the source rule of `holds_via_rule`. + /// + /// Contracting V or O over its third axis must give back the 64 x 64 + /// `holds` register, and each cell must read the same through its HHTL16 + /// address. + #[test] + fn the_third_axis_contracts_back_to_holds() { + use dr_math_binding_probe::hhtl16; + use lance_graph_contract::morton8x8::Morton8x8; + let (mut two_parents, mut two_origins) = (false, false); + for g in all_goldens() { + let kb = Kb::load(&g.facts).unwrap(); + let h = kb.solve(); + let nw = kb.worlds.0.len(); + let v: Vec = (0..nw) + .map(|par| std::array::from_fn(|p| h.inherited_from(par, p))) + .collect(); + for p in 0..SLOTS { + let via_parent = v.iter().fold(h.direct[p], |a, s| a | s[p]); + assert_eq!(via_parent, h.holds[p], "{} V", g.fixture_id); + let via_origin = h.origins.iter().fold(0, |a, s| a | s[p]); + assert_eq!(via_origin, h.holds[p], "{} O", g.fixture_id); + for w in 0..nw { + let parents = v.iter().filter(|s| s[p] >> w & 1 == 1).count(); + let origins = h.origins.iter().filter(|s| s[p] >> w & 1 == 1).count(); + two_parents |= parents >= 2; + two_origins |= origins >= 2; + } + } + for cube in [&v, &h.origins, &h.sources] { + for slice in cube.iter() { + for p in 0..kb.props.0.len() { + for w in 0..nw { + let code = Morton8x8::from_xy(p as u8, w as u8); + let bit = slice[p] >> w & 1 == 1; + assert_eq!(hhtl16::cell(slice, code), Ok(bit)); + } + } + } + } + } + // Anti-vacuity: the third axis carries more than one entry somewhere, + // so contraction is a real OR and not a copy of one slice. + assert!(two_parents, "no cell with two parents"); + assert!(two_origins, "no cell with two origins"); + } + #[test] fn lineage_never_leaves_the_held_cells() { // F5: r_orphan has a rule companion but no assertion, so p holds