Part II, Volume XIII. Rung 30 of the ladder. The volume does not import a new subject — it names one the series has been using since its first page. G = U∘F∘K∘C is a composite, composition is a 1-morphism, and the question of whether two routes through the chain agree on the nose or only up to something is a 2-morphism. The coherence data has never been written down.
WP-81 places Volume XI (K-theory) first in reading order and it remains there. In construction order it cannot be first: Mathlib contains zero K-theory files, so Volume XI has no machine-checked core available and would fail the series' own admissibility rule. The measurement behind that is WP-82 · The Missing Floor, and the author chapter for the construction Volume XI is named after is Book 7 · Alexander Grothendieck — which also measures the corpus’ one index candidate and finds it is not invariant.
Rung 30 is the opposite case. CategoryTheory/ is the second largest area in
Mathlib — 1089 .lean files, behind
Algebra/ at 1341 and ahead of Analysis/ at 792 — with
44 under Bicategory/, 108 under
Monoidal/, 68 under AlgebraicTopology/SimplicialSet/
and 6 under AlgebraicTopology/Quasicategory/. Every result this
volume needs is already formalised; the work is instantiation, not construction.
Provenance. Re-measured 2026-09-12 against the Mathlib checked
out in the geometry repository, which has not moved since 2026-07-13 (toolchain
v4.32.0) — so this is the same tree the 2026-08-29 measurement
read. That earlier reading gave 1113 / 48 / 112, and called
CategoryTheory/ the deepest area in Mathlib; the file counts and the superlative are
both corrected here. The two numbers that carry the argument are unchanged and both still hold:
Bicategory/ and Quasicategory/ exist and are populated, and Mathlib
still contains zero K-theory files. The counts are checked mechanically by
book13/ch-mathlib-verify.py, which fails if the tree and this page
disagree.
Book 8, Chapter 13 sets out a 2 × 2 taxonomy and calls the fourth cell holology, the logic of the whole as a whole. Until 11 September 2026 that chapter held the cell had no consolidated tradition because it had no settled name. It does have one: topos theory has named that ground four ways over sixty years, and the chapter now says so.
What survives the correction lands here. Topos theory is explicitly plural — many toposes, many internal logics — so it says which universes are possible and not which one obtains. Holology wants the second, which inside the machinery is a selection principle: a Lawvere–Tierney topology j : Ω → Ω singled out and the others forbidden. That is a statement in category theory, it is checkable, and if it is ever to be made under a kernel it has to be made in this volume and not in that one. It is not made here either, and Chapter 2 is upstream of it: an operator chain whose objects are unnamed cannot select anything. See Book 8 · Ch 13 · §5.
Chapter 3 closed by showing the chain associates definitionally at levels 0 and 1: chain1_assoc_rfl discharges it by rfl, and weakness exists only at level 2, where Mathlib's bicategory associator is an isomorphism and never an equation. That verdict makes Chapter 2 load-bearing for the whole volume: if C, K, F, U are plain functions on a type — AXLE's PhaseVector := Fin 12 → ℝ with applyG : PhaseVector → PhaseVector — then rung 30 buys the series nothing and Volume XIII closes as a one-section negative result, which Chapter 2's stub says is to be published, not routed around.
A fourth outcome was added to Chapter 2 on 2026-08-29, and it changes the shape of that question. applyG is a fact about a Lean file, not about the world. The LAW3M brief states the empirical object as an ODE on (ℝ³, α = dz − r²dθ) with a computed basin boundary at r* = 0.77594058 — a flow, not a function. If the operators are phases of that flow, composition is time addition and associates on the nose; the path-dependence lives in the basin, and the weakness, if any, lives at the fold, where the flow stops being a diffeomorphism.
Two artifacts decide it and neither is Lean: re-run certify_rstar.py against the brief, and run the two-route assembly of 216 spheres and record whether the outcomes are equal or merely isomorphic. The [K, F] ≠ 0 tension stated in Chapter 2 must be settled before any of it reaches Chapter 4.
| # | Chapter | Status |
|---|---|---|
| 1 | The Chain Was Never a Diagram Three years of arrows, and no statement of what category they live in | STUB |
| 2 | What Category Is It On? Naming the objects before naming the arrows · fourth outcome added 2026-08-29: the operators may not be endofunctors at all but phases of a flow, in which case composition is time addition and associates strictly | STUB |
| 3 | On the Nose, or Up to Something The chapter that decides whether this volume needs to exist | CLOSED |
| 4 | The Associator and the Pentagon If composition is weak, the coherence is not optional | STUB |
| 5 | Thirty-Three Compositions What the iterated composite accumulates when composition is weak | STUB |
| 6 | When Coherence Does Not Stop at Two The rung's actual infinity, and how it differs from every other infinity in this series | STUB |
| 7 | What the Kernel Can Check The admissibility test this volume has to pass before it is written | PARTIAL |
| 8 | Known Limits What this volume will not have established, written before it is written | STUB |
| 9 | What a Model Carries Equality, isomorphism, interpretation — and which of the three Beltrami’s 1868 dictionary actually is. Open: no kernel-checked core; its candidate core routes to Volume XI. | OPEN |
| 10 | What a Check Establishes Four rules, each extracted from a failure with a date on it — this chapter existed on disk from 2026-09-17 and was not linked here until 2026-09-19 | partial |
| 11 | What This Volume Has Actually Proved Six findings, each recomputed by ch11-verify.py: a rung number this volume assigned itself, an artifact that is not in this repository, a gate that counted a doubled report, and two level-2 theorems that hold in every bicategory | audit |
| A | The Range of a Variable A type is a range and a vicious circle is a range containing the quantifier. Stated that way it is mechanically testable: tools/self_reference.py over all 57 verify scripts — 0 vicious, 8 guarded, 48 narrow — and it found WP-82’s rung table counting the paper that prints it, 12 of 12 rows in one column and 0 of 12 in the other. Fixed by stratifying the range. | PARTIAL |
Most chapters here are stubs: a statement of what the chapter must establish and what would close it. Six are. Chapter 10, added 2026-09-17, is a partial result with a working instrument behind it and no type hierarchy constructed, and it says so. Chapter 3 is closed and has a kernel-checked artifact behind it; Chapter 7 is a partial result; Chapter 9 is open and says so, having no kernel-checked core and a candidate core that routes out of this volume into Volume XI. Under the rule that an entry is written only when there is a recorded artifact behind it, only Chapter 3 is an entry. A volume named after a rung does not occupy it. Chapter 3 may collapse the volume to a single page, and chapter 2 may end it before chapter 3; both outcomes are results and are to be published as such.
Nothing in the corpus uses higher-categorical vocabulary — measured across ten spellings on
2026-08-29, the counts are effectively zero. What the corpus has instead is three years of
unbracketed four-fold composites and a central object, G^[33], whose bracketing has
never been specified. There are on the order of 1017 ways to bracket a 33-fold
composite. Mac Lane's coherence theorem is the reason that need not matter — and the series has
been relying on it without stating it.