Ch 1 · What the Kernel Certifies

Every system that checks proofs mechanically must provide a way to write down a step you have not done; without one, no large proof could be started. The escape hatch is universal. Its name is not — and the names are not translations of one another.

1 · The five words

community	word	what it admits
Lean / Mathlib	sorry	a step the author intends to return to
Isabelle/HOL	sorry, oops	the same, plus abandoning a goal — not attested in the source now held
Coq / Rocq	Admitted	a whole lemma closed by fiat — admit not separately attested
proof-carrying code	axiom, trust	a fact the checker will not verify and must be believed
aerospace certification	axiom, trust	patterns with the row above, not as a fifth word — see §5

WP-94 §1. The Lean and proof-carrying-code rows are checked against primary sources; Isabelle, Coq and avionics are marked OPEN there and remain so here.

2 · Countability is the tell

WP-94's census over 3,207,496 running words found the difference is grammatical, not doctrinal. Cited, not recomputed:

WP-94 §2, the numeral column sorry takes a bare numeral 905 times — a word for a thing you count without a measure phrase, because counting is what you do to items on a list you intend to shorten. gap, the ordinary English word for the same object, takes a numeral 26 times and prefers a determiner. axiom runs the other way: it appears in the plural more often than the singular, because an axiom is not an item on a worklist but a member of a set you are trying to keep small.

That is the whole entry. sorry is a worklist noun; axiom is a set noun. A worklist can be emptied while the set is not. Nothing about the two words licenses reading a count of one as a statement about the other.

3 · The field case, two weeks later

On 2026-09-18 a live page of this corpus printed “0 sorry in Chain_updated.lean” in a section headed What has been proved. The file has no sorry and the claim is true. It also carries three axioms — inner_basin_is_asymmetric, outer_basin_unbounded, poincare_collatz — and the page said two and never named the third.

The grammar predicted the error An empty worklist was published as though it were an empty set. That is not a slip of attention; it is the substitution WP-94 said the two words do not support, made in the direction the countability data predicts — from the word you can count down to zero, to the word you cannot.

The same page displayed spiral_return_exists as proved. It takes h_second_circuit : G.iter 128 x₀ ≠ x₀ and closes with exact h_second_circuit. The kernel certifies the implication; the prose claimed the antecedent. A theorem that assumes its conclusion kernel-checks.

4 · What the reference actually says, and what it does not

The corpus's axiom gate reads #print axioms and accepts [propext, Classical.choice, Quot.sound]. Located in Theorem Proving in Lean:

term	where
propext	ch. 12 Axioms and Computation; §12.3 Function Extensionality — 6 pages
Quot.sound	§12.4 Quotients — 2 pages
noncomputable	ch. 12 — 5 pages
sorry	15 pages · and 53 printed pages of Mathematics in Lean, first p. 11
#print axioms	absent from the reference entirely
Classical.choice	not found under this spelling; the axiom is discussed in ch. 12, the identifier is not

TPiL carries no page numbers this reader can locate — 3 of 206 — so it is addressed by chapter and section, which is how the book is cited anyway.

The gate is named after a command its own reference never mentions Chapter 12 defines the three axioms the gate accepts and explains why admitting them costs computability. The command that reports them appears nowhere in the book. The gate was assembled from the axioms' definitions plus tooling knowledge the reference does not carry — which is what building a practice next to an unopened shelf produces: correct, and unable to say why.

5 · The three open rows, checked

WP-94 marked its Isabelle, Coq and avionics rows OPEN — “stated from working familiarity and not checked against a corpus here” — and named them as the rows the eventual paper must earn. Primary sources for all three arrived on 2026-09-19 and were checked the same hour. Two rows narrow. One fails.

row	source	result
Isabelle	Paulson, The Foundation of a Generic Theorem Prover, 37 pp	sorry 0 · oops 0 · axiom 79 · assumption 42
Coq	Huet, Kahn & Paulin-Mohring, The Coq Proof Assistant: A Tutorial, v8.0, 27 April 2004, 47 pp	Admitted 1, p. 17 · Axiom 7 · Hypothesis 27 · Parameter 2
aerospace	Denney, Fischer & Schumann, Using Automated Theorem Provers to Certify Auto-Generated Aerospace Software, NASA Ames, 13 pp	assumption 0 · assume 0 · axiom 12 · trust 2

Isabelle — a checked negative, not a confirmation

The word is absent from Isabelle's foundational paper, whose vocabulary for an unfinished step is axiom and assumption. That is consistent with sorry arriving later, with Isar, but this source cannot establish a date and no dated source is held. WP-94 §4's diachronic pivot — whether Isabelle's sorry predates Lean's — therefore stays OPEN. What has changed is that it is now open against evidence rather than against nothing.

Coq — the row overstated its own vocabulary

WP-94 gives Coq “admit a step closed by fiat; Admitted for the whole lemma.” This tutorial attests Admitted once, and the standalone admit tactic not at all — the single lowercase match is the substring inside Admitted, which is a trap worth naming because it inflates exactly this kind of count. The tutorial is also one source and not the manual, so this narrows the claim rather than refuting it. Correction to WP-94 §1: the Coq row should read Admitted, with admit unattested here.

The fifth row may not be a fifth community

WP-94's fifth row is “avionics assurance · assumption · a condition the argument is conditional on.” In the aerospace-certification source now held, assumption occurs zero times and assume zero. What the paper uses is axiom (12) and trust (2) — the proof-carrying-code vocabulary of row four.

So on this evidence the table has four words and not five, and the fifth row was a guess about a community rather than a reading of one. It may still be right for the assurance-case literature proper — DO-178C, goal-structuring notation — where “assumption” is a term of art. None of that is held. Until it is, the fifth row is withdrawn, not corrected. [OPEN]

That is the shape of the whole volume in one pass: three rows that had been stated from familiarity, checked against sources within an hour of their arriving, producing one narrowing, one withdrawal, and one honest negative. None of it required new mathematics. All of it required opening the file.

6 · The entry, stated

sorry counts. Its absence is a claim about a worklist and about nothing else.
axiom does not count; it belongs to a set. Its members must be named, because a number is not a description of a set.
#print axioms is the verdict, and it reports the second, not the first.
A theorem's hypotheses are part of what it says. The kernel certifies an implication; only a reader certifies that the antecedent holds of anything.

7 · Open

(i) The assurance-case literature proper — DO-178C, goal-structuring notation — where “assumption” is a term of art. Not held; the fifth row waits on it. [OPEN]
(ii) Whether Isabelle's sorry predates Lean's. No dated source is held; the foundational paper does not carry the word. [OPEN]
(iii) Classical.choice under its identifier spelling. [OPEN]

8 · References

WP-94 · One Hole, Five Words — the census and the countability finding, cited not recomputed.
Avigad, de Moura & Kong, Theorem Proving in Lean · Avigad & Massot, Mathematics in Lean v4.19.0 · Paulson, The Foundation of a Generic Theorem Prover · Huet, Kahn & Paulin-Mohring, The Coq Proof Assistant: A Tutorial v8.0 · Denney, Fischer & Schumann, NASA Ames. sha256 for each in docs/floor-texts.tsv.
tools/book19_ch01_verify.py — exit 0, 2026-09-19.