# Model Measurements — the byte-LM + the Apeiron, on our own kernel

> **Empirical, not a proof, and dated.** The single results doc for the model lane: what our
> framework-native models did on real data, run on **our own** `proof/Runtime/Model.lean` +
> `proof/Substrate/Algebra/NeuralPrimitives.lean` — the second of which was moved under `Neural/` at <!-- CITATION-EXEMPT: moved at cc26679e then deleted at f58f3c5d, kept as the record -->
> `cc26679e` (2026-06-22) and deleted at `f58f3c5d` (2026-07-01), taking all fifteen theorems this
> document cites from it. Every number below is the record of a 2026-06 run, not a present-tense
> measurement; the Labels block says which harness still exists. The *catalogue/reading* (why
> there is no model zoo) lives in [`THE_HASHMAP_PATH.md`](THE_HASHMAP_PATH.md) §the model trinity;
> this doc holds the **numbers**. Two live threads on our code, plus the archived external-repo
> history that motivated them:
> 1. **The byte-LM suffix counter** (`Model.lean`) — beats a torch byte-Transformer on every metric.
> 2. **The Apeiron spectral collapse** (`Model.lean §5e` / `NeuralPrimitives §7`) — the cell's
>    second recovery operator, measured: the register is real, the next-byte lever small.
> 3. *(archived, external `peregrine-trainer`)* the rotor chord (4.19 bits/byte, superseded by §1)
>    and the closed-form STT wall (LER ~0.77, the monad blindness §2 acts on) — work we moved off.

---

# §1 — The byte-LM: the suffix counter beats PyTorch

> **Author:** Claude (Opus 4.8), 2026-06-13. **Empirical**, on `proof/Runtime/Model.lean`
> (zero-sorry, green). A framework-native byte LM that runs locally and serves as the Scribe's
> helper-face brain. Every number was *run* (`sang model tabulate`/`teach`/`chat`), held-out, and
> points at the artifact.

**What the model is (the subtraction).** The framework-native byte LM is the **Witten–Bell suffix
counter** already in `Model.lean`: the **B/U accumulator on the proven suffix filtration**
(`suffix_keys_form_a_filtration`, `THE_HASHMAP_PATH §the dual`). Nothing added — the hashmap path's
Map/Accumulator faces: **fold = counting** (`tabFoldText`, one forward pass, the `+` merge); **read =
Witten–Bell blend** (`wbDist`/`wbRefine`, weights derived from the table's own distinct-continuation
counts — the Dedup face; **zero free params, no SGD/Adam/backprop**); **generate = the spinor loop**
(`generate`, argmax at `T→0` or seeded categorical, O(k)/token, no `Y`, no KV cache).

**Result 1 — beats PyTorch on every metric at matched data.** Byte next-token on a pinned C4 slice
(`experiments/ml_baseline/PROTOCOL.md`), held-out 20K positions, identical per contestant. Three
counter reads on the SAME table (the merge is the only freedom): **WB** = Witten–Bell (B/U-additive
backoff); **KN** = absolute discounting (NB-subtraction face); **KNx** = full Kneser–Ney (lower orders
by *continuation count* = Set/NB face + continuation-unigram floor). Opponent: `gpt_opponent.py`, a
1.71M-param 2-layer causal byte-Transformer, AdamW, CPU.

Held-out **bits/byte** (lower better):

| train | WB | KN | **KNx** | torch GPT |
|---|---:|---:|---:|---:|
| 100k  | 3.179 | 2.802 | **2.496** | 2.942 |
| 500k  | 2.780 | 2.500 | **2.204** | 2.469 |
| 8M    | 2.198 | 2.097 | **1.890** | 2.034 |
| 18M   | 2.058 | 1.986 | **1.817** | 1.952 |

**Top-1 / train wall-clock** (KNx vs torch): 100k 50.1% vs 39.9% (0.3 s vs 22 s); 8M 60.5% vs 56.4%
(~65 s vs 1704 s); 18M 61.5% vs 58.3% (~190 s vs 3785 s). The counter at the full-KN read **wins
bits/byte, top-1, and training speed simultaneously at every matched-data scale** (gzip −9 = 3.390,
xz −9 = 3.293, both beaten from 100k up), carrying exact merge-of-shards / unfold / bit-reproducible
heads at no price.

```
cd proof && lake build sang
.lake/build/bin/sang model tabulate \
  ../experiments/ml_baseline/data/train_scale_8000000.tsv \
  ../experiments/ml_baseline/data/heldout.tsv --order 8 --kn --knx
```



## Limitations recorded by the original document

## Labels (Axiom XIII)

* **Proved (riding):** the suffix orders are a filtration, not an n-gram heuristic
  (`Model.suffix_keys_form_a_filtration`); the streaming read is exact
  (`Collapse.streaming_exact`); the ridge head is the objective's minimizer and its Gram is an
  order-free monoid over a positive-definite drag (`TrainingCollapse.ridgeHead_minimizes_objective`,
  `TrainingCollapse.gram_stack`, `TrainingCollapse.drag_posDef`); the depth-1 flat lift is the family
  `Web.sweep_depth_is_radius` says loses; the monad/Apeiron axis is
  `SpectralWorld.monad_recovery_compact` / `SpectralWorld.logos_recovery_noncompact`, with
  `RoutesToChaos.cover_escapes_polynomials` the reason no finite collapse reaches the residual. This
  document declares nothing.
* **Anchor:** every table. Each is a reading of one run onto the model, never a
  theorem. No machine is stated for §1, §2 or §4 — "CPU" (§1 Result 1), "16 CPU cores" (§4), "32
  cores" (§2 wall-clock) is all there is, and a bits/byte or a wall-clock from one unnamed box and
  one pinned slice transfers nowhere.
* **Retired:** superseded — the header names `proof/Substrate/Algebra/NeuralPrimitives.lean` as the <!-- CITATION-EXEMPT: moved at cc26679e then deleted at f58f3c5d, kept as the record -->
  proof anchor for §1 and §2. **Correction to the record (2026-08-06):** this bullet said the module
  was "deleted in `cc26679e`". `cc26679e` (2026-06-22, "Restructure complete: Substrate/Algebra's 184
  files into 12 topic folders") *renamed* it — `R099` to `proof/Substrate/Algebra/Neural/`. The
  deletion is `f58f3c5d` (2026-07-01, "refactor: delete NeuralPrimitives.lean, inline its live
  dependents"). One module, two commits, and the same one `THE_INFERENCE_TRINITY.md` and
  `SEED_SPEC.md` cite under the post-move path. **Every theorem the body cites from it resolves to no
  declaration** — with its line in the `f58f3c5d^` blob: `spectral_collapse_is_spinor_fixed_point:250`, <!-- CITATION-EXEMPT: deleted at f58f3c5d, kept as the record -->
  `spectral_collapse_is_compact_not_logos:317`, `lpc_is_ridge_minimizer:676`, <!-- CITATION-EXEMPT: deleted at f58f3c5d, kept as the record -->
  `nonlinear_read_is_depth_two_boost_ridge:772`, `causalScan_incremental:1654`, <!-- CITATION-EXEMPT: deleted at f58f3c5d, kept as the record -->
  `causalScan_apply_is_full_eval:1677`, `causalScan_infinite_is_closed_form:1687`, <!-- CITATION-EXEMPT: deleted at f58f3c5d, kept as the record -->
  `band_lossless_on_local:1721`, `simKey_scale_invariant:1822`, `recall_inserted:1846`, <!-- CITATION-EXEMPT: deleted at f58f3c5d, kept as the record -->
  `recall_content_addressed:1854`, `literal_counter_is_exact_key:1877`, `autocorr2d_is_dot:1956`, <!-- CITATION-EXEMPT: deleted at f58f3c5d, kept as the record -->
  `image_lpc_is_ridge_minimizer:1972`, `shift2d:1947` <!-- CITATION-EXEMPT: deleted at f58f3c5d, kept as the record -->
  (`grep -rn` over `proof/**/*.lean` minus `.lake`, 2026-08-06). Current corpus, same date:
  `scripts/check-roots.py` reads 604 proof modules, 599 roots, 605 index rows, 3398 canonical warrant
  bullets; `data/audit/CERTIFICATE.json` records 7607 authored statements over 598 modules, 0 holes.
* **Retired:** superseded — §1's reproduce lines. `sang model tabulate` now accepts only `[--order k]
  [--save out]` (`proof/Runtime/Model.lean:2226`); `--kn`, `--knx`, `--spectral`, `--orbit`,
  `--solve` are not parsed. KNx is the unconditional read (`foldCounterScore` → `knxDist`), and the
  WB and KN arms are gone with `wbDist`, `wbRefine` and `tabPredict`, which declare nowhere in the
  corpus. **The WB | KN | KNx table cannot be produced by the current binary at all.** §1 Result
  10/11's `--whiten` is now the inverted `--no-whiten` (whitening is the default,
  `proof/Runtime/Model.lean:2137`).
* **Anchor:** §4 in full. `sang model forward` was removed on 2026-06-17 in
  `d0a53e85` ("Yeet the gemv kernels, the C, and the dense transformer forward wholesale"), together
  with `linearPar`, `qlinearPar` and the `--quant` arm. **GATE A's 5.307687 vs PyTorch 5.307615, and
  the in-memory `--aware` floor +0.0946 vs bnb NF4 +0.1408, have no harness in this tree.** What
  survives is the storage half: `seal` / `qrun` still dispatch (`proof/Runtime/Model.lean:1985`,
  `:1988`) over `rmsNormB` / `attnB` / `ropeB` / `sealEntry` / `runEntry` in
  `proof/Runtime/SeedForward.lean`.
* **Anchor:** §2 Results 1–3. `couplingRows`, `specCover` and `specKey` declare
  nowhere; `specApply` and `specTopModes` survive in `proof/Runtime/SpectralFold.lean` under `sang
  fold`, not `Model.lean §5e`, and no `--spectral` flag exists. The spectral-floor tables are a
  record of a run, not a reproducible one.
* **Anchor:** §1 Results 6, 7, 8 (both of them) and 9 — the length sweep, the depth
  sweep, the routing table and the NIAH table. Their harnesses are `/tmp/lensweep/sweep.py`, <!-- CITATION-EXEMPT: /tmp is untracked in the sanguine repo, kept as the record -->
  `/tmp/route/gen.py`, `/tmp/route/niah.py` and `/tmp/route/gen_wide.py`. `/tmp` is not a repository; <!-- CITATION-EXEMPT: /tmp is untracked in the sanguine repo, kept as the record -->
  the scripts are absent and were never tracked, so those four lines now read "Ran under", not
  "Reproduce".
* **Open:** the pinned inputs. `experiments/ml_baseline/PROTOCOL.md`, `gen_data.py` and
  `gpt_opponent.py` exist; `experiments/ml_baseline/data/` does not, and the source
  `data/boundary/c4_text_massive/…` is gitignored (`.gitignore`) and absent, as are the audio corpora
  behind §2 Results 5–7 and the Claude Code logs behind §1's second Result 8. `experiments/audio/`
  (`run.sh`, `README.md`, the three preps) is intact. Re-running means re-downloading per
  `data/MANIFEST.md:160–197`, and a fresh download is not the pinned slice.
* **Open:** two distinct sections are both numbered "Result 8" in §1 — the inference trinity's third
  face, and the sovereign seed on our own logs — and §4 is printed before §3.