WP-82 found the corpus quoting rung 33 thirty-one times and rung 28 zero times, and asked for the floor to be built first. The floor was in Downloads: Weibel, van Neerven, Connes–Marcolli, Deisenroth — 5,309 pages, uncited. The books were never missing. They had no address.
Rung 28: quoted zero times, founding text 576 pages, on the desk. Rung 33: quoted thirty-one times, founding text 705 pages, same desk. Neither had been opened. The inversion WP-82 measured is a distribution of citing; the reading was never done at either end.
A ladder is the wrong picture in one direction
It implies the low levels are done. They are not, and formalisation is what shows it: under a total-function kernel, natural subtraction truncates, division by zero is defined,
00 has a value, limits are filters, and “let X be a random variable” is a measurable-space instance with side conditions. Each of those was run rather than recalled —
Book17Core.lean (12 theorems, no imports) and
Book17Mathlib.lean (9 theorems, Mathlib v4.33.0-rc1).
[VERIFIED 2026-09-19]Two of those rows are sharper than the sentence above them.
Filter.Tendsto f l₁ l₂ unfolds definitionally to
Filter.map f l₁ ≤ l₂, so “limits are filters” is closed by
Iff.rfl — it is not an analogy. And a real random variable with no second moment does not make
variance undefined; it makes it
zero, and the zero is a theorem (
variance_of_not_memLp). A statistic that silently returns 0 for a variable whose variance does not exist is the kind of thing the ladder picture says is behind us.
This corpus's own case is checked:
GateScreen.lean generalised WP-39's T2(i) from one loss to
every layer-local map fixing zero. The squaring sat in the prose for two years as if it were part of the result. The proof never used it.
[VERIFIED 2026-09-15]