The series rule is that an entry is written only when there is a recorded artifact behind it. This chapter is where Volume XIII either acquires one or admits it has not.
One Lean file, pinned to the Mathlib actually built in the geometry repository, elaborating with
zero errors, ending in #print axioms over every declaration the volume claims. The
permitted set is propext, Classical.choice, Quot.sound.
Anything reporting sorryAx is an admit and is named as one in the chapter that
depends on it.
sorry. When an identifier stops
resolving, a hypothesis can silently become sorry and
#print axioms reports exactly what it reported before.: True := trivial compiles, carries no
sorry, and reports only the three permitted axioms. A scan that does not fire on
its own fixtures cannot see it.Each detector used in this volume ships with cases it is required to reject. A gate that has never rejected anything is not known to work. This is not optional infrastructure; it is the reason two of the three failure modes above were ever found.
The chapter-3 file was written with a fixture: a declaration
vacuity_control : True := trivial, deliberately contentless, placed in the audit so
that the probe would have something it ought to be able to reject. It could not.
Read the last three lines together. assoc₂_hom_inv and assoc₂_inv_hom
carry the entire mathematical content of level 2 — the associator is invertible, so the bracketings
are isomorphic and not equal. vacuity_control says nothing at all. The reports are
byte-identical. DATA
| Declaration | Content | Axioms |
|---|---|---|
| chain₁_assoc | trivial — a rewrite by two lemmas | 3 |
| assoc₂_hom_inv | substantive — invertibility of the associator | 0 |
| vacuity_control | none | 0 |
Axiom count is not a proxy for content. In this file it is
anti-correlated: the trivial statements carry three axioms and the substantive ones carry
none. The three on the chain₁ family almost certainly enter through the ambient
Category and Functor machinery the statements reference, not through
anything their proofs do — checkable with
#print axioms CategoryTheory.Functor.assoc, and not yet checked here.
OPEN
#print axioms reports what a declaration rests on.
It never reports what a declaration says. A clean axiom report is a floor, not a
certificate, and no volume in this series may cite one as evidence that a theorem has content.
Reading the statement remains mandatory. This is the empirical version of the argument in
book8/ch-do-not-trust-verify.html.
One file exists and its report is printed above verbatim, with its fixture. The chapter closes when every other chapter of this volume has one — chapter 2 above all, which chapter 3 has now made load-bearing for the entire volume.