What this companion adds and what its checks mean
The guide preserves the earlier worked examples. TikZ generates every drawing from exact objects; there are no raster figures. Python checks finite enumerations, minors, projectors and matrices; the text argues uniform conclusions. These checks supply no new Lean certificate or census update. Supporting Markdown (.md) files accompany the source.
Read this as
The source's internal formal implications are distinguished from the arithmetic inputs: representability, residual occupancy, applicable patching, classicality, attached representations and compatible systems, Frobenius density, semisimplification and Brauer–Nesbitt. Universal companions and unrestricted reciprocity remain outside the proved scope.
Inherited labels and current mathematical judgments
The original-status labels record historical verification coverage. The current mathematical audit judges the actual statements. These are different questions:
| Original | Inherited label | Current statement-level judgment |
|---|---|---|
| 6.12 | unchecked | The reversed containment is false: in the node of V–9, \(M=R\) has full support, which is not contained in either single component. |
| 10.5 | partial | The unrestricted effectivity conclusion lacks the coefficient, continuity, integrality and frame hypotheses made explicit in the revision. |
Use each check for its actual subject
| Evidence | What its subject is |
|---|---|
| Inherited Lean record | The mapped revised statements under their supplied hypotheses. This guide neither replays that build nor changes the original-wording record. |
| Current exact Python checks | Forty-six illustrative assertions: 31 inherited checks and 15 added checks on the printed finite examples and identities. |
| Mathematical arguments | Uniform quotient, specialization and all-level conclusions, with their hypotheses retained in the text. A finite diagram is not an infinite proof. |
| PDF and rebuild checks | Topic alignment, bounds, vector-only assets, resolved references, and an isolated byte/text/page comparison. These are document checks. |
The supporting README.md gives portable rebuild commands. The source-coverage Markdown and JSON map all 49 internal claims to this guide's reading entries and exact manuscript labels. The audit records dependency versions, mathematical self-review and complete-page inspection. No finite calculation here verifies residual automorphic existence, classicality, attached compatible systems, or a universal arithmetic theorem.