9.5. Reverse index
The index below asks the coverage question in the opposite direction: not which Lean declarations correspond to a paper result, but which node accounts for each module of the pinned formalization. The development has 139 modules, three entry points and 136 under nine directories, and every one appears exactly once below, with the entries of the correspondence table that name it; each module name links to its source at the pinned commit. Modules marked †, and shown muted, contribute nothing to any of the three closed root theorems: the kernel-level dependency walk described at the end of this section reaches none of their declarations. A module marked (none) is named by no entry — both such modules are also unreachable, and each is superseded by a module the proof does use. A cluster node is later split by promoting rows of this index to nodes of their own.
The root modules state the theorem:
Module | Node |
|---|---|
| |
no node; a one-declaration reduction recorded with the root theorem | |
no node; the mathlib |
Analysis/ holds one module, the implicit function theorem step of
the Euclidean equivalence:
Module | Node |
|---|---|
Algebra/ holds the commutative algebra:
Module | Node |
|---|---|
| |
Combinatorics/ holds the sparsity theory and the flag states:
Module | Node |
|---|---|
(none) | |
| |
Graph/ holds one module:
Module | Node |
|---|---|
(none) |
Incidence/ holds the chart layer under Proposition 6.5:
Module | Node |
|---|---|
| |
| |
Interop/ holds one module, outside the proof:
Module | Node |
|---|---|
no node; the mathlib |
Linear/ holds the direction-stress theory of the deletion step:
Module | Node |
|---|---|
NullCellule/ holds the semismallness induction and the height theorem:
Module | Node |
|---|---|
| |
| |
Rigidity/ holds the real bar–joint model and the two ends of the argument:
Module | Node |
|---|---|
The daggers come from a measurement rather than a reading. The walk is a
short metaprogram,
scripts/reachable.lean
in this blueprint's repository: it takes the constants of the three closed
root theorems in the kernel environment and closes over every constant
appearing in the type or the value — proof terms included — of each
declaration it meets, then reports, per module of the formalization, which
declarations were reached. The three roots are the maximum-rank statement
and the two Euclidean statements the Asimow–Roth bridge derives from it;
walking only the first would report the whole bridge as dead.
Rerunning it against the pinned submodule reproduces the numbers here, and
scripts/coverage.py --reachable checks every dagger in this index against
its output. The walk reaches 1,458 of the development's 2,662
declarations, and the twelve daggered modules contribute none of theirs; every
module the walk does reach is named by some entry above, so nothing
load-bearing is unaccounted for. Of the four modules that develop
the construction theorem of the sparsity
chapter, only a few counting facts are reachable: from TightCompletion.lean
one equation lemma for a definition made elsewhere; from
TriangleSequence.lean two declarations about the four-element vertex set of
a K_4; from GraphExtension.lean eight facts about the edges one outside
vertex sends into a tight subgraph; and from Construction.lean its edge-set
vocabulary rather than its reduction theorems. The twelve daggered modules
divide into three groups. Two are superseded and named by no entry: the
multigraph interface, whose conversion the proof never calls, and the capacity
table, whose bounds the proof takes from PinRank.lean instead. Eight
are documented as parallel developments by the
Split–Klein and
assembly chapters: the literal build of the
ideal, the weight apparatus, and the two orbit modules. The last two are the
mathlib Graph compatibility export, which upstream offers to other
developments and no root theorem uses.