A reading map
On this page · Permalink · Source line 2
This volume develops the algebraic steps in conditional automorphic completion. Read its support and packet theorems as deductions for the rings, modules, complexes, and arithmetic inputs that are actually supplied. They do not create missing residual occupancy or missing classicality.
The companion visual guide gives 27 worked lessons. The Lean and evidence guide exposes the production sources, the 49-claim crosswalk, and the hypotheses of the formal interfaces. The links below are reading routes, not additional theorem certificates.
What the verification record means
On this page · Permalink · Source line 17
The inherited formal record covers all 49 revised internal claims. The original-wording ledger remains separate: 41 complete, seven partial, and one unchecked. This release preserves those historical statuses rather than promoting amended statements into proofs of their stronger predecessors.
No fresh Lean compilation is claimed here. Current checks concern source preservation, inherited evidence authenticity, bounded computations, references, and publication quality. Representability, applicable patching, classicality, attached representations, Frobenius density, and the comparison inputs retain their stated external status.
The final theorem requires a compatible Hecke point over the stated field. The propagation step compares two already existing families associated with the same automorphic object. Paper XI's general realization conjecture is not an input to this paper.