Use the example on the left to keep the relevant object in view while reading the exact statement on the right. The guide is explanatory; the main text supplies the theorem hypotheses and the proof contract.
| Guide | Question or calculation | Paper XII reference |
|---|---|---|
| V–3 | Quotient monomials before or after completed combination | Theorem 3.1; Corollary 3.2 |
| V–4 | A test point factors exactly when its local equations vanish | Proposition 3.3 |
| V–5 | Compatible precision data and the closed-kernel argument | Section 3; Section 10 |
| V–6–7 | Minors, fiber dimensions, support, and nilpotent structure | Theorems 6.3–6.4 |
| V–8 | Base change and transport of intrinsic Fitting ideals | Proposition 6.5; Theorem 7.1 |
| V–9 | A quotient loses a generic point without creating a projector | Propositions 3.4 and 7.3 |
| V–10 | Auxiliary freeness versus full deformation support | Theorems 6.7, 6.9, 6.11; Example 6.13 |
| V–11 | A two-term projective complex and its derived fibers | Definition 6.14; Theorem 6.16 |
| V–12–13 | Whole primary packets, localization, and scalar fibers | Theorems 7.4, 8.2; Corollaries 8.3–8.4 |
| V–14 | Sign-projector failure and augmentation recovery | Section 5; Remark 8.5; Section 11 |
| V–15–16 | Stable images, finite stabilization, and tail escape | Section 8, items 8.7–8.13 |
| V–17 | Compatible Hecke points and conditional realization | Theorem 12.6; Section 13 |
Three short proof-reading tests
Can a module have full support but fail to be faithful? Yes. On Visual 10, the module \(k\) over \(k[[x]]/(x^2)\) has a nonzero nilpotent annihilator and full support.
Do equal support sets force equal Fitting ideals? No. On Visual 7, \((xy)\) and \((x^2y)\) have the same vanishing set but different infinitesimal behavior.
Do nonzero finite levels force a nonzero inverse limit? No. On Visual 15, \(N^3=0\) forces every compatible sequence to vanish, although every level is \(k^3\).
Provenance and reproducibility
The source is Patching Support, Hecke Packets, and Conditional Automorphic Completion, Komorebi P., revised formalization v0.17.0. The theorem references above are internal references to that manuscript. The existing 49-claim revised formal contract and its inherited original-wording boundaries are unchanged.
The accompanying Python script performs 46 exact checks: exhaustive finite test-ring enumeration, symbolic minors and CRT identities, exact matrix calculations, and the identities behind the stable-core examples. All drawings are reproducible vector graphics. Further worked details appear on Visual 19–Visual 25; the inherited revised/original claim boundary is on Visual 26. The illustrative examples are not newly certified in Lean by this guide; its finite checks are reported separately from the source release. Infinite claims are supported by the arguments given here, not by extrapolating a finite image.