Coherence · the volume turned on itself
Volume XIII was specified before it was written, and several of its chapters are about whether it should be written. This one is about what it has proved. Every number below is recomputed by book13/ch11-verify.py, which exits non-zero the day any of it stops being true.
1 · Rung 30 is asserted eleven times and nowhere else
Every page of this volume carries the masthead Rung 30 · Higher Category Theory. Eleven pages assert it. Outside Volume XIII, nothing in the corpus does.
| where | rung numbers it names |
|---|
| WP-82, the document this volume cites as its authority | 9, 28, 33 |
| docs/floor-ladder.tsv | 11, 12, 14, 16, 17, 20, 21, 28, 33 |
| tools/floor_texts.py, the overlay from WP-82 §3 | 28, 29, 33 |
| Volume XIII, eleven pages | 30 |
WP-82 orders the rungs by field and terminates at 33. It does not contain a rung 30, and neither does any ladder the corpus keeps. The number was assigned by this volume to itself, and then printed on every page as though it had been read off a table.
Why this is more than a typo
A rung number is an address. The whole apparatus the corpus built in September — the ladder file, tools/ladder_check.py, the rule that a volume's number must agree in three independent places — exists because a file in the wrong volume gets read by the next session and built on. A volume that numbers itself is outside that apparatus by construction: there is nothing for the check to compare against.
2 · The artifact is cited three times and is not in this repository
Three pages name AXLE/Vol13_Coherence.lean as the artifact behind the volume — chapter 3 twice, chapter 7 once, and the index once more in its status line. Copies of that file inside this repository: zero.
The file is real. It sits in the AXLE repository on the author's machine, and this chapter was written with it open. But a reader of the published site follows the citation and arrives nowhere, which is the condition R11 exists to forbid: a declaration resolves at the path cited, or it is not a citation. Crossing a repository boundary without saying so is the same failure as a wrong path, with better intentions.
The narrower version of the same problem
What this repository does hold is the report: tools/verify-audit/2026-09-09/Vol13_Coherence.axioms.txt and its gate verdict. A saved #print axioms report beside no file is a certificate for something the reader cannot inspect. It is strictly worse than no report, because it looks like evidence.
3 · The gate said eighteen. There are nine.
The saved report contains eighteen depends on axioms lines and nine distinct declarations. Every name appears twice. tools/axiom_gate.py counts lines, so its recorded verdict reads:
OK: 18 theorems, no sorryAx, no axiom outside the permitted set.
Chapter 3 of this same volume says nine axiom probes, twice. Both numbers describe one file. The larger one is an artefact of a doubled report and has been sitting in the audit trail since 2026-09-09.
What the gate is and is not
The gate was written to answer one question — is any axiom outside the permitted three, and is there a sorryAx — and on that question it was right. The theorem count is a second claim it makes in the same breath, and on a doubled file that claim is false while the first stays true. A green verdict is not a single fact.
4 · What the artifact proves, stated exactly
Nine declarations, of which one is a deliberate blank. Vol13.vacuity_control : True := trivial is a fixture, declared as such in the file: it exists so that the probe reports a contentless theorem in exactly the words it uses for a real one. That is good practice, and the volume deserves the credit. It also means the honest headline is eight theorems and one control.
The eight divide by level, and the division is the finding:
| level | what is proved | how it closes |
|---|
| 0 · endofunctions | the four bracketings of U ∘ F ∘ K ∘ C are equal | rfl |
| 1 · endofunctors | the same, for functor composition, and the 33-fold iterate regroups freely | rfl, Functor.assoc |
| 2 · a bicategory | the associator is invertible in both directions | Iso.hom_inv_id, Iso.inv_hom_id |
Levels 0 and 1 are honest and the file says plainly what they cost: composition is strict there, and — in the file's own words — rung 30 buys nothing at that level.
Level 2 does not say what the chapter title claims it settles
assoc₂_hom_inv and assoc₂_inv_hom prove that Mathlib's associator α_ is invertible. It is an Iso; the proofs are Iso.hom_inv_id and Iso.inv_hom_id. That holds for every isomorphism in every bicategory, for arbitrary 1-morphisms, by construction.
So the two theorems are true, kernel-checked, and carry no information about this chain. They are a restatement of the bicategory axioms with the letters C, K and F substituted in. Nothing in the file establishes that the operator chain lives in a bicategory rather than in the category of endofunctors — and the file itself says the series “has never claimed to be working at” level 2.
Chapter 3, titled the chapter that decides whether this volume needs to exist, records the verdict “strict at levels 0 and 1, weak at level 2” and marks itself Closed · kernel-checked. The weakness at level 2 is a property of the setting that was chosen, not a discovery about the chain. Choosing to work in a bicategory and then observing that bicategories have associators does not decide whether this volume needs to exist. It assumes it.
5 · The shape of the whole volume
Ten chapters. Chapter 3 decides whether the volume is needed; chapter 7 is the admissibility test the volume must pass before it is written; chapter 8 is what the volume will not have established, written before it is written. Three of ten are about the volume rather than about its subject, and they are the ones marked closed or specified.
WP-82 assigns rung 28 — K-theory and index theory — and rung 33 — noncommutative geometry — and observes the corpus citing the top of the ladder thirty-one times and the middle twice. Volume XIII was written before XI and XII on an argument recorded in book13/ch-mathlib-verify.py: Mathlib has no K-theory, so XI could not have a machine-checked core, while CategoryTheory/ is large enough that XIII's work would be instantiation rather than construction.
That argument has since been overtaken, and the script says so itself
The script's own NOT ESTABLISHED section states that a file count measures a library's size and not its fit to a purpose. It was right. And Volume XXVIII now has a machine-checked core —
book28/ShiftIndex.lean, four theorems, actual kernels and cokernels — built without any K-theory in Mathlib at all, because the index of a shift is linear algebra. The obstacle that decided this volume's place in the reading order was measured once and then inherited.
6 · The volume's own contents page skipped a chapter
Twelve chapter files sit in book13/. Until this chapter was written, the contents table listed ten rows, and row 10 pointed at ch-types-the-range-of-a-variable.html. ch10-what-a-check-establishes.html was not linked from its own volume at all — it had been on disk since 2026-09-17 and was reachable only from a Book X chapter and from the generated master index.
It is the best chapter in the volume. Every rule in it was extracted from a failure with a date attached, and the volume's front door did not mention it.
Fixed in the same commit that found it
The contents table now gives Ch 10 its row, this chapter Ch 11, and moves The Range of a Variable to row A, where a chapter outside the numbered sequence belongs. ch11-verify.py now checks that no book13/ch*.html is missing from the index, so the next one fails the script instead of waiting two days for a reader.
7 · What this chapter does not claim
- That the Lean file is wrong. It is careful, it is honest in its comments, and its vacuity control is better practice than most of the corpus.
- That higher category theory is the wrong subject for a volume. It is a real subject with real content, and none of it is here yet.
- That chapters about method are worthless. Chapter 10 earns its place: every rule in it came from a failure with a date on it. The objection is to a volume whose closed chapters are all method and whose subject is unstarted.
- That this chapter is exempt. It is checked by book13/ch11-verify.py, which recomputes all five findings and fails if the corpus moves under them.
8 · The six findings, as the script prints them
F1 pages asserting 'rung 30' : 11, of which outside book13: 0
rung numbers WP-82 names : [9, 28, 33]
F2 pages citing Vol13_Coherence.lean : 3
copies of it inside this repository: 0
F3 lines in the saved report : 18
DISTINCT declarations in it : 9
the gate's recorded verdict : OK: 18 theorems, ...
F4 #print axioms probes in the file: 9
declared vacuous (True := trivial): ['vacuity_control']
F5 level-2 theorems close by : Iso.hom_inv_id / Iso.inv_hom_id
F6 chapter files in book13/ : 12
not linked from book13/index.html: none (was: ch10)