Book XIX · opened 2026-09-19 · The practice, read against its manual
AXLE and the Manual
This corpus writes Lean daily, keeps an axiom gate, and has spent a month making rules about declarations resolving at the path cited. It holds three Lean books — the language's design thesis, the Mathlib tutorial, and the reference — and had opened none of them. This volume reads AXLE against them.
The gap this volume closes is not knowledge of mathematics. It is that a practice was built by inference from error messages, next to a shelf that explains it, for two years.
1 · The three books, and what each is for
| text | pp | what it answers |
|---|
| S. Ullrich, An Extensible Theorem Proving Frontend (Lean 4 thesis) | 255 | why elaboration, macros and the kernel are separated — the design, not the usage |
| J. Avigad & P. Massot, Mathematics in Lean, release v4.19.0 (11 Jun 2026) | 214 | how Mathlib is meant to be used, idiom by idiom |
| J. Avigad, L. de Moura & S. Kong, Theorem Proving in Lean | 206 | the reference: dependent types, tactics, axioms |
The third is the one that bears directly on this corpus's standing rules. The axiom gate reads #print axioms and accepts [propext, Classical.choice, Quot.sound]; the reference is where those three are introduced and where what an axiom declaration does to a development is set out. The gate was written correctly by inference. It has never been checked against the text that defines it.
2 · What the audit already has to work with
This volume does not start empty. The 2026-09-18 audit of the hub page produced findings that are properly Lean-practice findings and belong here:
- A theorem that assumes its conclusion kernel-checks. spiral_return_exists 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. This is the central lesson of the whole volume in one declaration.
- An axiom is accepted by being assumed, so the absence of sorry is not the verdict and #print axioms is. The hub said two axioms where the file has three.
- Two divergent files share the name Chain_updated.lean, one sorry-free and one not, and the page cited a third path that does not exist.
- 110 .lean names cited across the corpus resolve nowhere, per tools/lean_addresses.py.
- "AXLE compiles nothing" was carried in a handoff and had never been run; one lake env lean refuted it.
The shape of every item above
Each is a claim about a proof that was true of the words and false of the file, or true of the file and never checked. That is the failure mode a manual prevents and an error message does not — an error message tells you what broke, never what you were entitled to say.
3 · Chapters
| ch | title | state |
|---|
| 1 | What the Kernel Certifies — the lexical entry WP-94 left open, the field case, and the gate read against the reference | live |
| 2 | The Idioms AXLE Reinvented — corpus tactics and structures against Mathematics in Lean, chapter by chapter | planned |
| 3 | Elaborator, Macro, Kernel — Ullrich's separation, and which corpus complaints are about which layer | planned |
| 4 | Addresses — why 110 declaration names resolve nowhere, and the smallest rule that would have prevented it | planned |
4 · What this volume will not claim
- That AXLE's proofs are wrong. Those that check, check; the findings are about what was said about them.
- That reading the manual would have prevented the mathematics. It would have prevented the prose.
- Any count of theorems without a tier. R1 applies here more than anywhere: a count without a tier is not a count.