The final theorem is a composition of proved implications with explicitly supplied data. Use a single coherent Frobenius normalization in every polynomial comparison. These are not competing labels: an implication may be internally proved while its arithmetic premises remain external.
| Gate | What must be supplied | What the formal deduction gives |
|---|---|---|
| Residual | Residual automorphic occupancy and a represented deformation problem. | The rings, universal representation, and starting carrier are available as inputs. |
| Patching | An applicable patching package: full patched support, quotient, and control isomorphism. | Full support descends to the finite-level module or perfect complex. |
| Comparison | A ring map \(f:R\to T\) with the stated support comparison, or the suitable isomorphism and carrier identification. | Support is transported at compatible points. |
| Fiber | A Hecke point \(y:T\to E'\) over the same field, with \(y\circ f=x\). | A nonzero scalar fiber and an actual eigensystem; in the derived case, one survives in a cohomological degree. |
| Realization | Classicality for that eigensystem, an attached representation, continuity, equality of the universal specialization and attached Frobenius polynomials on a dense union of conjugacy classes, and semisimplification/Brauer–Nesbitt inputs. | The specialization is identified after semisimplification with the attached representation. |
Support alone does not supply a point over the same field
The inclusion \({\mathbb Q}\to{\mathbb Q}(i)\) preserves full support of the nonzero scalar-extended carrier. But no \({\mathbb Q}\)-algebra map \({\mathbb Q}(i)\to{\mathbb Q}\) exists: the image of \(i\) would be a rational number \(a\) with \(a^2=-1\). Thus one cannot infer the required Hecke point \(y\) merely from a support statement.
Propagation needs two existing families and the same automorphic object
After producing an automorphic object \(\pi\), retain that same \(\pi\). The propagation statement assumes both the original compatible family and the family attached to \(\pi\) already exist, with the common Frobenius polynomial data and the stated comparison hypotheses. It then identifies corresponding members. It does not construct a missing family.
Read this as
The algebra locates and transports supplied nonzero data. Arithmetic inputs establish occurrence, classicality, and attachment. A visualization must not turn one of those inputs into an automatic consequence.