Merge pull request #948 from AdaWorldAPI/claude/jirak-math-theorems-harvest-rfii13

D-WXS-3b: the L4 lane — and a disable probe that can itself be vacuous

Author: AdaWorldAPI

.claude/board/EPIPHANIES.md

@@ -1,3 +1,138 @@
+## 2026-08-13 — E-A-TOTAL-FUNCTION-THAT-CANNOT-REFUSE-IS-A-CORRUPTION-PATH-1
+
+**Status:** FINDING `[G]` — two measured instances, one crate, one hour.
+Found by codex review on PR #948; the second by following the first to its
+class. **Confidence:** High. Mechanism measured, not inferred.
+
+**The shape.** `CalibratedFloor::quantize(f64) -> u8` is **total**: every input
+returns a valid-looking bucket. It has no way to say *"that was not a
+measurement."* Measured behaviour on non-finite input:
+
+| input | bucket | why |
+|---|---|---|
+| `NaN` | **0** | `f64::clamp` **propagates** `NaN` rather than clamping it, then Rust's float→int cast saturates and sends `NaN` to zero |
+| `-inf` | **0** | clamps to the low rim |
+| `+inf` | **255** | clamps to the high rim |
+
+Every one of those is a **legitimate** bucket. `0` and `255` are the ordinary
+saturation values; `bucket_center(0)` is a real number near `lo`. Nothing
+downstream can distinguish the result from a genuine reading.
+
+**Why this was live and not theoretical.** ARCO-ERA5 is sparse *by design*:
+`probes/weather-p1/README.md` §1 records `fill_value: NaN`, that several
+variables 404 at the arc's **own fixture timestep**, and that in Zarr v2 a
+missing chunk means all-`fill_value` — so **a 404 is valid store semantics, not
+a fetch failure**, and *"any ingest must treat 404 as data."* The 404-ing list
+at that timestep includes five variables the W1 field set actually packs.
+
+**Instance 1 — the store path** (`lane.rs::pack_facet`, codex P1). An absent
+field would have been written as plausible low-bucket measurements and read
+back through `bucket_center` as ordinary numbers. This is the reserved-slot
+rule — *"a reserved slot must not read back as a plausible number"* — defeated
+one level deeper, where the existing guard could not see it.
+
+**Instance 2 — the INSTRUMENT path, and it is worse**
+(`floor.rs::saturation_of`). That function scores *"an ARBITRARY external
+population"* by counting rim buckets — and non-finite input lands **on the
+rim**. An all-`NaN` population would have scored `1.0`: **"completely
+saturated" when the truth is "no data at all."** Those are opposite findings
+and the bare fraction could not tell them apart. It is bar B2's instrument, so
+the corruption would have propagated into a *measurement* rather than a stored
+value.
+
+> **The sharpening worth keeping: a corrupted stored value is bad; a corrupted
+> INSTRUMENT is worse.** A bad value is one wrong row. A bad instrument is
+> every conclusion drawn with it, each of which looks sound and carries no
+> trace of the defect. When a finding lands on a total function, check its
+> *measurement* call sites before its storage call sites.
+
+**The other half of the same mistake — do not silently drop.** Skipping
+non-finite values without reporting them is equally wrong: the caller never
+learns the population was partly or wholly absent. The fix therefore
+**reports**: `saturation_of` returns `SaturationScore { fraction, finite,
+non_finite }`, matching this crate's standing shape (`calibrate` and `decode`
+return `None` on a degenerate case rather than inventing a number) and the
+`D-WXS-12` rule that *the degenerate case must be reported, never folded as
+`0.0`*.
+
+**Where the guard belongs.** At the boundary where an external value enters
+the register — not inside the hot primitive. `quantize` keeps its signature
+(changing it ripples through every call site); `pack_facet` refuses, and
+`saturation_of` excludes-and-counts. `calibrate` was checked and is **clean**
+— it already filters `is_finite`, so the hole never reached calibration. Every
+`quantize` call site in the crate is now either guarded or provably finite.
+
+**Generalizable check, cheap to run:** for every total function that maps a
+wider domain onto a narrower one — quantisers, clamps, `as` casts,
+`unwrap_or`, saturating arithmetic — ask *what does an invalid input return,
+and is that return distinguishable from a valid one?* If the answer is "a
+valid-looking value", the function cannot refuse, and every call site is a
+corruption path until one of them does.
+
+**Cross-ref:** `E-VACUOUS-ASSERTION-IS-THE-HOUSE-STYLE-1`;
+`E-A-DISABLE-PROBE-CAN-ITSELF-BE-VACUOUS-1` (same session, the verification
+layer); `.claude/plans/weather-soa-bake-v1.md` §4 bar B2 (the instrument);
+`probes/weather-p1/README.md` §1 (the store semantics); PR #948.
+
+---
+
+## 2026-08-13 — E-A-DISABLE-PROBE-CAN-ITSELF-BE-VACUOUS-1
+
+**Status:** FINDING `[G]` — three measured instances in one session, all mine.
+**Confidence:** High. Method-level; no code claim.
+
+**The known rule it extends.** This workspace already holds *"an assertion
+implied by the code it tests is not a test"* (`CLAUDE.md` § falsifiability rule)
+and, in the sibling repo's words, *"turning a knob that does not bind is not a
+disable."* Both are stated about **tests**. This entry records that the same
+failure applies one level up — to the **verification probe** that is supposed to
+prove a test can fail — and that it is harder to spot there, because a broken
+probe and a passing suite look identical.
+
+**The three instances, same session, gating `crates/weather-poc`.**
+
+1. **Wrong symbol name.** A probe searched for `ManifestError::DuplicateSlot`;
+   the real variant is `SlotCollision`. The substitution script aborted, the
+   test run afterwards executed **unmodified code**, and reported `25 passed`.
+   Read casually, that is a passing disable-verification of a guard that was
+   never touched.
+2. **Dead code.** A probe inserted an `if` block computing `lo`/`hi` and
+   discarding both (`let _ = (lo, hi);`). It applied cleanly and changed
+   nothing. `25 passed` again.
+3. **Wrong target.** A probe changed `raw` to `raw.max(1)` intending to make
+   reserved slots decode — but the unpack loop only visits **manifest-resolved**
+   slots, so the edit could never reach a reserved one. `33 passed`.
+
+Instance 1 is the dangerous one: 2 and 3 at least ran, while 1 silently did not.
+
+**The signature that separates the two causes.** A disable run that stays green
+has two possible explanations — *the guard is absent* or *the probe never
+touched it* — and greenness alone does not distinguish them. What does: a
+correct disable kills **at least one** test, and usually a small, nameable set.
+
+> **A disable that kills ZERO tests is more likely a broken probe than a missing
+> guard.** Treat zero as "re-check the probe", never as "verified".
+
+Corollary, the mechanical fix now in use: **the probe must assert that it
+applied.** Every substitution asserts its pattern was found and the file
+actually changed, and fails loudly otherwise — so instance 1 becomes an error
+instead of a green run.
+
+**Why this is worth a board entry rather than a shrug.** The whole
+disable-the-fix discipline exists because a passing test proves nothing about
+whether it *could* fail. If the probe that establishes that is itself unchecked,
+the discipline has an unverified root and inherits exactly the confidence it was
+built to withdraw. Three instances in one session, by an operator applying the
+rule deliberately, is the measured argument that the root needs checking too.
+
+**Cross-ref:** `E-VACUOUS-ASSERTION-IS-THE-HOUSE-STYLE-1`,
+`E-A-CONTROL-THAT-CANNOT-LOSE-IS-NO-CONTROL-1`,
+`E-ANTI-EIGENVALUE-MACHINERY-CAN-ITSELF-BECOME-THE-EIGENVALUE-1` (the same
+one-level-up move, applied there to guards rather than probes);
+`CLAUDE.md` § The falsifiability rule.
+
+---
+
 ## 2026-08-12 — E-THE-REGIME-LADDER-MEASURED-RANGE-NOT-TURBULENCE-1
 
 **Status:** FINDING `[G]` — measured, same run, found by an operator

.claude/board/STATUS_BOARD.md

@@ -12,9 +12,10 @@ with a control that can lose and a stay-silent twin.
 | D-WXS-1 | field manifest v1 — (facet, pair, byte) → (variable, level, unit, floor id), a committed data artifact, ClassView-side | 0 | **SHIPPED 2026-08-13** — `data/field_manifest_v1.tsv` (22 rows = F0 5 pairs + F1/F2 3 pairs each, reserved slots emit NO row) + `manifest.rs`, 13/13; collision guard **disable-verified** (removed → only `colliding_entries_are_rejected` fails, BOTH stay-silent twins stay green). Bar B0's end-to-end half (mutating an entry changes written bytes) DEFERRED — the bake does not exist yet | slot purity §2; bar B0 |
 | D-WXS-1a | variable census as a committed re-runnable probe (17 surface + 91 upper-air + 14 static = 122 fields; 92,044 six-hourly steps) | 0 | **SHIPPED 2026-08-13** — `era5_variable_census.py` + `.json`; `--selftest` PASS on all 10 constants, orchestrator-rerun independently; guard disable-verified (one constant broken → exit 1, correct message) | ends the chat-only-figure defect for the census |
 | D-WXS-2 | key codec `(lat,lon) ↔ NodeGuid` — HEEL 16° tile / HIP within-tile / TWIG dormant; ragged tiles; lon-wrap range-SET | 1 | **SHIPPED 2026-08-13** — `key.rs`, 5/5 green; exhaustive 1,038,240-cell round-trip + collision-free; both bar-B1 halves **disable-verified** by the orchestrator (zeroing the HIP lat byte kills 3 tests incl. collision + ragged; removing the seam split kills the wrap twin while the non-wrap twin stays green) | a 16° box becomes a HEEL-prefix scan; bar B1 |
-| D-WXS-2a | **NEW — row-major vs Morton, pre-registered comparison.** The shipped key assigns one WHOLE byte per axis; OGAR's cascade doctrine specifies the axis bytes **nibble-interleaved** (Morton). §1.2 deviated from the canon it cites and did not say so — now recorded as plan §1.3a. The prefix-scan claim holds under both; what differs is neighbour locality (`lat ± 1` is 1440 cells away under row-major) and how many ranges a non-tile-aligned box needs | 1 | Queued | gates any downstream assumption of Morton locality — measured against the ζ stencil (D-WXS-9), metric stated before the run |
-| D-WXS-3 | shared canonical floor calibration (global 0.4–99.6 pct, frozen per epoch, stamped in dataset metadata) | 1 | **SHIPPED 2026-08-13** — `floor.rs`, 7/7; bar B2 **disable-verified** (widening the "narrow" control floor kills only the control, twin stays green); version-stamp mismatch detected, ±½-bucket round-trip asserted | bar B2 |
-| D-WXS-4 | the bake: one timestep → 1,038,240 NodeRows → ONE Lance version | 1 | Queued | bar B3; the missing path |
+| D-WXS-2a | **NEW — row-major vs Morton, pre-registered comparison.** The shipped key assigns one WHOLE byte per axis; OGAR's cascade doctrine specifies the axis bytes **nibble-interleaved** (Morton). §1.2 deviated from the canon it cites and did not say so — now recorded as plan §1.3a. The prefix-scan claim holds under both; what differs is neighbour locality (`lat ± 1` is 1440 cells away under row-major) and how many ranges a non-tile-aligned box needs | 1 | **Bar PRE-REGISTERED 2026-08-13** (plan §1.3b, committed before the run). Half A (pure key-space: range count + neighbour locality; arms SHIPPED/MORTON/CONTROL-BAD) is runnable NOW. Half B (the ζ stencil) is gated on D-WXS-9 → D-WXS-0 | gates any downstream assumption of Morton locality — measured against the ζ stencil (D-WXS-9), metric stated before the run |
+| D-WXS-3 | shared canonical floor calibration (global 0.4–99.6 pct, frozen per epoch, stamped in dataset metadata) | 1 | **SHIPPED 2026-08-13** — `floor.rs`; bar B2 **disable-verified** (widening the "narrow" control floor kills only the control, twin stays green); version-stamp mismatch detected, ±½-bucket round-trip asserted. **AMENDED same day** (`E-A-TOTAL-FUNCTION-THAT-CANNOT-REFUSE-IS-A-CORRUPTION-PATH-1`): `saturation_of` folded non-finite input into the metric — `quantize` sends `NaN`/`-inf`→0 and `+inf`→255, all **rim** buckets, so an all-`NaN` population scored **1.0** ("fully saturated") where the truth is "no data at all". Now returns `SaturationScore {fraction, finite, non_finite}` — reported, never folded and never silently dropped. `calibrate` checked **CLEAN** (already filters `is_finite`) | bar B2 — this is the bar's own INSTRUMENT, so the defect would have corrupted a measurement, not a value |
+| D-WXS-3b | **NEW — the L4 lane (pack/unpack ONE 16-byte facet).** The plan gave the lane a worker in §6.2 but **no D-id in §4's ladder** — it jumped D-WXS-3 → D-WXS-4. Added here as the pack/unpack half the bake will call | 1 | **SHIPPED 2026-08-13** — `lane.rs`, 33/33 crate-wide; 4 disables verified by the orchestrator (lo/hi swap → the swap test; hard-coded slot → 3 tests incl. manifest-load-bearing; version guard bypassed → the version test; unmapped slots emitting values → the reserved-slot test). The lane names no ERA5 variable in its own source — the caller's closure owns that **AMENDED same day (codex P1, PR #948):** `pack_facet` accepted non-finite readings; `quantize` maps them to valid-looking buckets, so a missing ARCO-ERA5 chunk (all-`NaN` — **valid store semantics**, and five W1 variables 404 at the arc's own fixture timestep) would have been stored as plausible low-bucket measurements. Now `LaneError::NonFiniteValue`, covering `±inf` too since they land on the rim. Disable-verified | precursor to bar B3; §2.6 slot purity as code |
+| D-WXS-4 | the bake: one timestep → 1,038,240 NodeRows → ONE Lance version | 1 | Queued — **blocked behind D-WXS-0** (must refuse to write without a minted classid) | bar B3; the missing path |
 | D-WXS-5 | statics bake — separate classid, separate dataset, exactly ONE version | 1 | Queued | bar B4; avoids ~1.3 PB of rewritten constants |
 | D-WXS-6 | version-range read (`QueryReference::at(v,rung)` + `deinterlace`) + version-count scaling measurement | 2 | Queued | bar B5; KILL if growth is superlinear at 92,044 versions |
 | D-WXS-7 | **D-WXA-5 re-homed and RE-SPECIFIED** — ρ(code_dist, field_dist) via `jc::reliability::spearman` over whole-grid pairs. (a) ρ ≥ 0.9996 (the bar a real pair FAILED at 0.999556); (b) shuffled-codebook control < 0.98 (measured losable at 0.003–0.159); (c) 16/64/256-level ladder must be MONOTONE before any verdict | 3 | Queued | ⚠ poc-v2's ρ ≥ 0.98 is at risk of being vacuous — D-CZ-1 §6.4 measured real-arm ρ spread 3e-6…4.7e-5 |

.claude/plans/weather-soa-bake-v1.md

@@ -198,6 +198,69 @@ test:** `box_ranges` treats `lon_lo == lon_hi` as *wrap the whole circle*, not a
 *empty box*. Neither reading is forced by the spec. It needs a test pinning the
 chosen one, or an API that makes the ambiguity unrepresentable.
 
+### §1.3b `D-WXS-2a` — the row-major-vs-Morton bar, PRE-REGISTERED 2026-08-13 (written and committed BEFORE the run)
+
+§1.3a leaves the layout a *stated deviation, not a ruling*. This section is the
+bar that resolves it. **Split in two, because only one half is runnable today:**
+
+- **Half A — pure key-space. Runnable now**, needs no ERA5 data, no classid,
+  no bake. This is what is pre-registered here.
+- **Half B — the ζ stencil under each layout.** Gated on `D-WXS-9`, itself gated
+  on the bake and therefore on `D-WXS-0`. Not pre-registered here; it inherits
+  this section's metrics when it runs.
+
+**First, a correction to §1.3a's own wording.** §1.3a called the shipped layout
+"row-major". That is imprecise. The key orders bytes
+`[lat_tile, lon_tile, lat_hip, lon_hip]`, so lexicographic order is
+**tile-row-major, then row-major *within* a tile** — a two-level blocked order,
+which already has better locality than a flat row-major over 721×1440 would.
+Recording this before measuring, so the comparison is against what is actually
+shipped rather than against the looser word.
+
+#### The two metrics (both computed over key-order index, not raw bytes)
+
+1. **Range count** — the number of maximal contiguous runs in key order needed
+   to cover **exactly** a given box, with **no false positives** (a scan that
+   over-reads and filters is a different, weaker thing and does not count).
+2. **Neighbour locality** — the median `|key_index(a) − key_index(b)|` over the
+   4-neighbourhood (`lat ± 1`, `lon ± 1`, longitude wrapping), across a
+   deterministic sample of cells.
+
+#### Arms
+
+| arm | layout |
+|---|---|
+| **SHIPPED** | `[lat_tile, lon_tile, lat_hip, lon_hip]` — what `key.rs` emits today |
+| **MORTON** | the OGAR-canon reading: the two axis bytes of a tier nibble-interleaved |
+| **CONTROL-BAD** | a deliberately locality-destroying order (axis bytes byte-reversed, i.e. `lon_hip` most significant) |
+
+#### The bar, with both halves and a kill
+
+- **Primary:** MORTON beats SHIPPED on **both** metrics, over a box set that
+  includes tile-aligned, non-tile-aligned, seam-crossing and pole-adjacent
+  boxes. "Beats" is stated before the run as: strictly fewer ranges on the
+  **median** non-tile-aligned box, **and** strictly smaller median neighbour
+  distance.
+- **Control that can lose:** **CONTROL-BAD must be worse than both** on both
+  metrics. If a deliberately bad order scores like the good ones, the metric is
+  not measuring locality and no verdict may be read off it.
+- **Stay-silent twin (non-trivial):** on a **tile-aligned** box, SHIPPED and
+  MORTON must produce **exactly one range each** — identical. This is §1.2's
+  actual load-bearing claim, and it must show **no difference** where the plan
+  claims none. A comparison that reports MORTON better *everywhere*, including
+  here, is measuring something other than what it says.
+- **KILL:** if MORTON does **not** win on both metrics, the deviation is
+  **harmless for this workload**, §1.3a downgrades from "stated deviation owing a
+  decision" to a recorded note, and `D-WXS-2a` closes without a code change.
+  A negative result here is a real result and is the cheaper outcome — it retires
+  an open question rather than opening a migration.
+
+**Discipline note.** Half A cannot settle the *whole* question, because the
+stencil (half B) is where locality is actually spent. Half A can only show
+whether a difference exists **in key space at all**. If half A kills, half B is
+moot; if half A confirms, half B still has to run before any migration. Stated
+now so a green half A is not later read as a mandate.
+
 ### §1.4 classid — a mint decision, NOT taken here
 
 `0x0F = Geo` already exists in the OGAR domain table; free domains are `0x03–0x06`