The entries follow Chapter 3's template, one head sense and what the word must not be taken to mean, plus two lines of history: where it went wrong, and how it is used now. Every count comes from the 831 published pages at commit 7a471e3. COMPUTED
Head sense. A place in a proof the author has not finished, marked so the checker and the reader both know it.
Not to be read as. a fact. It is also not interchangeable with gap, axiom, admit or assumption: five communities name one hole five ways, and the words differ in grammar.
Where it went wrong. WP-94 found the difference is countability. In the corpus sorry takes a bare numeral ("one sorry") 905 times; gap, the ordinary word for the same thing, only 26. A countable word is an item on a list you mean to shorten.
Usage now. Book XIX ch 1 carries the lexical entry. The gate reads the kernel's sorryAx, not the word.
Head sense. Where the second derivative vanishes too (V″ = 0): the special case.
Not to be read as. “double root” or “critical point”. Those are three different objects.
Where it went wrong. WP-61: a theorem called q* a “degenerate double root” when q* was neither a root nor degenerate. It was wrong twice, though the mathematics underneath survived. At q = 1, V″(1) = 6 ≠ 0: non-degeneracy is the whole content, and “degenerate” asserted its opposite.
Usage now. The error phrase is used on 0 published pages. It survives only where it is quoted, in WP-61 and in the June Huh chapter that reports it. “Non-degenerate critical point” appears on 8 pages.
Head sense. Kernel-audited: #print axioms reports only the three standard axioms for that named declaration.
Not to be read as. written (a theorem line exists) or sorry-free (no sorry in the body). A page that puts a written-count under “Proved” overclaims by two steps.
Where it went wrong. CLAUDE.md's three-column rule: written, sorry-free, kernel-audited. “Proved belongs to the third column only.”
Usage now. The pages say proved 789 times and Proved 225, against kernel-checked 232, kernel-audited 33 and sorry-free 89. The count shows that the rule is newer than most of the prose.
Head sense. Without error, at the stated point.
Not to be read as. “in the limit”. A value approached as z → ∞ is exact only there.
Where it went wrong. The transverse rate μmax = −2 holds as z → ∞, not at finite z. The corpus now writes the qualifier.
Usage now. 1,300 uses. The script counts them and does not audit each one.
Head sense. A claim that something does not exist, which needs a proof or an exhaustive search.
Not to be read as. “I did not find X by <method>”. That is the honest form of a one-search absence.
Where it went wrong. CLAUDE.md: false absences came from case-sensitive globs, files without extensions, and a repository described as holding only sketches when it held Lean.
Usage now. 322 uses of “there is no” against 4 of “did not find”. Many of the 322 are correct mathematics (“there is no rational root”). The count is a work list, not a verdict.
Head sense. The printer's page limit for the hardback edition.
Not to be read as. a resonance, a symbol, or “6 × 111”.
Where it went wrong. The series once glossed the number with a meaning it did not have. Pablo Nogueira Grossi corrected it on 2026-09-27: other editions can change the limit.
Usage now. It is a constraint of one printer and one edition, recorded as such in CLAUDE.md.
Head sense. The number of tracked .lean files.
Not to be read as. “110 names that resolve nowhere”, which was the plan's reading.
Where it went wrong. Book XIX ch 4: no run of that figure was ever recorded, and the tool's own header prints “110 corpus .lean files”. The number was read with the wrong noun.
Usage now. Corrected on the index. The measured figure is 98 names and 217 citations.
Head sense. An argument that establishes its conclusion, checkable step by step.
Not to be read as. “a rough indication of the lines along which a rigorous proof can be given”, which is how Syntactic Structures describes its own argument (SS p.23).
Where it went wrong. Chapter 1: Pullum shows that SS contains no proof that English is not finite-state, though it was cited as one for fifty years.
Usage now. Chapter 1 supplies the proof for brackets, in Lean.
Head sense. Unfolding, the last step of the dm³ chain C → K → F → U.
Not to be read as. Union (the Omega chain G–L–R–U), Universal or Unification. Those are other senses or other keys.
Where it went wrong. Chapter 4: 68 pages gloss U as unfolding, 10 as union, 3 as universal and 3 as unification. That is three senses by Chapter 3's test.
Usage now. Recorded in the Key Register. Which gloss the other senses should take is an editorial decision still open.
The counts also show that the repairs have not reached most of the prose. For every “did not find” there are about eighty “there is no”, and “proved” appears more than three times as often as “kernel-checked”. Not every use is wrong. But the lexicon turns each rule into something a reader or a script can check, which is what Chapter 5's readers are for. COMPUTED
See also WP-94, WP-61, Book XIX and Chapter 7, on how much meaning a word can carry.