Komorebi P. • 10 October 2026 The paper repeatedly asks three different questions: does an object exist, where is a supplied object nonzero, and when does that object have the desired arithmetic meaning? This guide makes those distinctions tangible through examples that can be followed by hand.
| Question | What must be supplied |
|---|---|
| Existence | Is there a represented deformation problem, a nonzero carrier, or a compatible family to start with? |
| Support | At which prime ideals does the supplied module or complex survive? |
| Realization | Does the surviving eigensystem come from a classical automorphic object with the required attached representation? |
Three models, rather than one overloaded analogy
| Model | What it lets you see | Lessons |
|---|---|---|
| A formal thickening | Conditions on power series, infinitesimal points, obstructed lifts, and compatible precision levels. | Visual 3–Visual 5 |
| A presented module | Matrix rank, support, Fitting ideals, changes of coordinates, and nonreduced structure. | Visual 6–Visual 8 |
| A finite Artin algebra | Generalized eigenspaces, nilpotent directions, canonical packets, and empty packet modules. | Visual 12–Visual 14 |
The models are connected by the paper's theorems, but they are not the same ring. A polynomial coordinate plane is not a complete local spectrum, and a local branch is not an Artin product factor. Explicitly changing models prevents a picture from silently changing the hypotheses.
A route through the guide
Use the object atlas on Visual 2 when a symbol becomes unfamiliar. The local model starts on Visual 3; the matrix model on Visual 6. Lessons Visual 9–Visual 11 explain what quotients, patching, and derived fibers preserve. Lessons Visual 15–Visual 16 separate finite occupancy from genuine infinite compatibility. The exact arithmetic boundary is on Visual 17.
How to read a visual claim
Each lesson gives an explicit object, a calculation, and a source reference. Coordinate sketches display only the stated real points. Coefficient arrays and finite specialization diagrams describe the stated algebraic data exactly. Line thickness never stands for nilpotent multiplicity.
Read this as
These are explanations of the formal release, not additional assumptions or new Lean certificates. The accompanying scripts check the explicit finite calculations. They do not establish universal arithmetic existence.