Realization Calculus

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Included manuscript sections

• Paper_XII_Traditional_Final.bib
• core-monograph-layout.tex
• reading_route.tex

Read the typeset paper

1 % Final traditional edition. Raw manuscript snapshots are preserved in source_preserved/.
2 \pdfinfoomitdate=1
3 \pdfsuppressptexinfo=15
4 \pdftrailerid{}
5 \documentclass[11pt]{amsart}
6 \usepackage[margin=1.05in]{geometry}
7 
8 \usepackage[T1]{fontenc}
9 \usepackage{lmodern}
10 \usepackage[nopatch=footnote]{microtype}
11 \usepackage{amssymb,mathtools}
12 \usepackage{amscd}
13 \usepackage{bm}
14 \usepackage{aliascnt}
15 \usepackage{enumitem}
16 \usepackage{graphicx}
17 \usepackage{booktabs}
18 \usepackage{array}
19 \usepackage{longtable}
20 \usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref}
21 \usepackage[nameinlink,noabbrev]{cleveref}
22 
23 \allowdisplaybreaks
24 \hyphenpenalty=10000
25 \exhyphenpenalty=10000
26 \tolerance=2600
27 \emergencystretch=4em
28 
29 
30 
31 \setlist[enumerate]{topsep=4pt,itemsep=2pt}
32 \setlist[itemize]{topsep=4pt,itemsep=2pt}
33 
34 \newtheorem{theorem}{Theorem}[section]
35 \newaliascnt{proposition}{theorem}
36 \newtheorem{proposition}[proposition]{Proposition}
37 \aliascntresetthe{proposition}
38 \newaliascnt{lemma}{theorem}
39 \newtheorem{lemma}[lemma]{Lemma}
40 \aliascntresetthe{lemma}
41 \newaliascnt{corollary}{theorem}
42 \newtheorem{corollary}[corollary]{Corollary}
43 \aliascntresetthe{corollary}
44 \theoremstyle{definition}
45 \newaliascnt{definition}{theorem}
46 \newtheorem{definition}[definition]{Definition}
47 \aliascntresetthe{definition}
48 \newaliascnt{example}{theorem}
49 \newtheorem{example}[example]{Example}
50 \aliascntresetthe{example}
51 \newaliascnt{standardfact}{theorem}
52 \newtheorem{standardfact}[standardfact]{Standard Fact}
53 \aliascntresetthe{standardfact}
54 \theoremstyle{remark}
55 \newaliascnt{remark}{theorem}
56 \newtheorem{remark}[remark]{Remark}
57 \aliascntresetthe{remark}
58 
59 \crefname{theorem}{theorem}{theorems}
60 \crefname{proposition}{proposition}{propositions}
61 \crefname{lemma}{lemma}{lemmas}
62 \crefname{corollary}{corollary}{corollaries}
63 \crefname{definition}{definition}{definitions}
64 \crefname{example}{example}{examples}
65 \crefname{standardfact}{standard fact}{standard facts}
66 \crefname{remark}{remark}{remarks}
67 
68 \newcommand{\OO}{\mathcal O}
69 \newcommand{\FF}{\mathbb F}
70 \newcommand{\QQ}{\mathbb Q}
71 \newcommand{\ZZ}{\mathbb Z}
72 \newcommand{\CC}{\mathbb C}
73 \newcommand{\NN}{\mathbb N}
74 \newcommand{\EE}{\mathbb E}
75 \newcommand{\TT}{\mathbb T}
76 \newcommand{\Spec}{\operatorname{Spec}}
77 \newcommand{\Spf}{\operatorname{Spf}}
78 \newcommand{\Supp}{\operatorname{Supp}}
79 \newcommand{\Ann}{\operatorname{Ann}}
80 \newcommand{\Fitt}{\operatorname{Fitt}}
81 \newcommand{\Hom}{\operatorname{Hom}}
82 \newcommand{\End}{\operatorname{End}}
83 \newcommand{\Ext}{\operatorname{Ext}}
84 \newcommand{\Tor}{\operatorname{Tor}}
85 \newcommand{\coker}{\operatorname{coker}}
86 \newcommand{\im}{\operatorname{im}}
87 \newcommand{\rank}{\operatorname{rank}}
88 \newcommand{\Tr}{\operatorname{Tr}}
89 \newcommand{\Frob}{\operatorname{Frob}}
90 \newcommand{\Gal}{\operatorname{Gal}}
91 \newcommand{\GL}{\operatorname{GL}}
92 \newcommand{\ad}{\operatorname{ad}}
93 \newcommand{\Max}{\operatorname{Max}}
94 \newcommand{\Perf}{\operatorname{Perf}}
95 \newcommand{\nil}{\operatorname{Nil}}
96 \newcommand{\rad}{\operatorname{rad}}
97 \newcommand{\length}{\operatorname{length}}
98 \newcommand{\id}{\operatorname{id}}
99 \newcommand{\e}{\mathrm e}
100 \newcommand{\one}{\bm 1}
101 \newcommand{\norm}[1]{\left\lVert#1\right\rVert}
102 \newcommand{\abs}[1]{\left\lvert#1\right\rvert}
103 \newcommand{\calA}{\mathcal A}
104 \newcommand{\calC}{\mathcal C}
105 \newcommand{\calD}{\mathcal D}
106 \newcommand{\calF}{\mathcal F}
107 \newcommand{\calH}{\mathcal H}
108 \newcommand{\calM}{\mathcal M}
109 \newcommand{\calP}{\mathcal P}
110 \newcommand{\calR}{\mathcal R}
111 \newcommand{\calS}{\mathcal S}
112 \newcommand{\calT}{\mathcal T}
113 \newcommand{\calV}{\mathcal V}
114 \newcommand{\calW}{\mathcal W}
115 \newcommand{\frakC}{\mathfrak C}
116 \newcommand{\frakF}{\mathfrak F}
117 \newcommand{\frakm}{\mathfrak m}
118 \newcommand{\frakp}{\mathfrak p}
119 \newcommand{\fraka}{\mathfrak a}
120 \newcommand{\wideotimes}{\mathbin{\widehat\otimes}}
121 
122 \graphicspath{{figures/}}
123 
124 \title[Patching support and automorphic completion]{Patching Support, Hecke Packets, and Conditional Automorphic Completion}
125 \author[Komorebi P.]{Komorebi P.}
126 \subjclass[2020]{11F80, 11F70, 13C14, 13D09, 11R34}
127 \keywords{automorphy lifting, Taylor Wiles patching, module support, Hecke algebra, compatible system, adequate image}
128 \date{}
129 
130 \pdfstringdefDisableCommands{\let\unskip\relax}
131 \hypersetup{
132   pdftitle={Patching Support, Hecke Packets, and Conditional Automorphic Completion},
133   pdfauthor={Komorebi P.},
134   pdfsubject={Global deformation conditions, patching support, Hecke packets, compatible systems, and conditional automorphic realization}
135 }
136 
137 
138 % Operation Komorebi: shared publication profile.
139 \usepackage{komorebi-publication}
140 \renewcommand{\KomorebiTitle}{Patching Support and Hecke Packets}
141 \renewcommand{\KomorebiSubtitle}{Conditional automorphic completion}
142 \renewcommand{\KomorebiSeries}{Chapter XII}
143 \renewcommand{\KomorebiKind}{Monograph}
144 \renewcommand{\KomorebiEdition}{}
145 \renewcommand{\KomorebiShortTitle}{Paper XII / Conditional automorphic completion}
146 \renewcommand{\KomorebiTitleSize}{31}
147 \renewcommand{\KomorebiTitleLeading}{36}
148 \renewcommand{\KomorebiProfile}{classical}
149 \renewcommand{\KomorebiOrientation}{portrait}
150 \KomorebiSetup
151 \makeatletter
152 \providecommand\@dotsep{4.5}
153 \renewcommand\l@section{\@dottedtocline{1}{0pt}{2.8em}}
154 \renewcommand\numberline[1]{\hb@xt@\@tempdima{#1\hfil}}
155 \makeatother
156 \input{core-monograph-layout.tex}
157 \begin{document}
158 \KomorebiCover
159 \input{reading_route.tex}
160 
161 \begin{abstract}
162 Let \(\bar\rho\) be a residual Galois representation and let \(R\) be a global deformation ring with declared local conditions. We separate the global automorphy problem into residual occupancy, deformation support, Hecke occupancy, and arithmetic realization. Local conditions are encoded by quotient rings rather than by idempotents, since irreducible components of a local deformation ring need not be clopen. For an ordinary or derived patching datum, full support descends through the augmentation quotient. Near faithfulness is shown to be equivalent to full support for finite modules over Noetherian rings. An isomorphism \(R\cong\TT\) transports support, Fitting ideals, and point fibers, but a quotient map can erase an entire component. Finite Hecke algebras are resolved into canonical Artin packets, so simultaneous generalized eigenspaces are available without assuming semisimplicity. Nested packets in one finite carrier stabilize. For changing finite carriers, nonzero stable cores give compatible inverse limit vectors. These results give a pointwise criterion: a characteristic zero deformation point in automorphic support produces a Hecke eigensystem. With attached Galois representations, local global compatibility, and classicality, the point is automorphic. A fixed compatible system then propagates the conclusion to every coefficient place. For finite coefficient quotients, compatible conjugacy classes admit compatible continuous representatives. Declared polynomial quotient conditions survive their adic reconstruction. These completion statements require explicit finite occupancy, continuity, and integral Frobenius data. Universal companion existence and unrestricted reciprocity are not proved.
163 \end{abstract}
164 \makeatletter\@setabstract\makeatother
165 \thispagestyle{plain}
166 
167 \section*{The realization boundary}
168 Theorem~\ref{thm:five_gate_completion} brings the five realization requirements into one statement. The diagrams throughout the chapter distinguish supplied arithmetic data from algebraic deductions. The formal companion maps each claim to its source and describes the scope of the recorded verification.
169 
170 Formal evidence is mapped to all forty-nine revised internal claims. The original formulations have a separate record: forty-one complete, seven partial and one unchecked. The stronger original formulations and the revised statements are different contracts. The completed tensor and point-factorization results are algebraic deductions for supplied deformation data. Representability, residual occupancy, applicable patching and classicality theorems, attached Galois representations, Frobenius density, semisimplification, and the general Brauer--Nesbitt theorem remain external arithmetic or algebraic inputs. Neither Chapter XI's general Conjecture~66 nor universal companion existence is assumed.
171 
172 \section{Introduction}\label{sec:introduction}
173 
174 Automorphy lifting joins several kinds of mathematics that are easy to conflate. A residual representation must first occur in an automorphic carrier. The chosen characteristic zero representation must lie on a deformation problem controlled by local conditions. A patching argument must show that the automorphic module reaches the relevant part of the deformation space. A comparison such as \(R\cong\TT\) must identify the arithmetic and Hecke coordinates. Finally, the resulting Hecke point must be classical and must carry the expected Galois representation with the required local compatibility.
175 
176 None of these steps is merely a change of notation. A deeper lift above one residual representation cannot create a missing residual companion. Freeness over an auxiliary group algebra does not imply that every component of a deformation ring is occupied. An isomorphism of rings transports support that already exists, but it does not create a nonzero automorphic vector. A nonzero class in completed or torsion cohomology need not be classical without a theorem that says so.
177 
178 The Taylor Wiles method and its later forms solve these problems in many important settings \cite{Wiles1995,TaylorWiles1995,Diamond1997,Kisin2009,Gee2022}. Higher dimensional and derived versions use a broader range of local deformation rings, residual image conditions, torsion classes, and cohomological carriers \cite{ClozelHarrisTaylor2008,BarnetLambGeeGeraghtyTaylor2014,CalegariGeraghty2018,Thorne2012,MiagkovThorne2023,Scholze2015,CaraianiScholze2017,NewtonThorne2016}. The present chapter does not replace those theorems. It isolates the algebraic support statements that explain exactly what a patching package supplies once its arithmetic hypotheses have been verified.
179 
180 The first correction concerns local packets. A local deformation ring is usually complete and local. Its irreducible components are rarely open and closed. They cannot generally be represented by central idempotents. The correct object is a quotient ring defining a local condition, together with the support of a module or complex on the resulting spectrum. Central idempotents reappear later, where they belong, inside finite Artin Hecke algebras and finite dimensional characteristic zero carriers.
181 
182 The second correction concerns patching. The useful global conclusion is full support, often expressed as near faithfulness. For a finite module over a Noetherian ring, near faithfulness is equivalent to full support. Full support descends through the quotient that removes the auxiliary variables. This statement is elementary, but it is the exact bridge from a patched module to componentwise occupancy at finite level. The same conclusion holds for perfect complexes through derived support.
183 
184 The third correction concerns Hecke packets. Semisimplicity is not required to isolate a maximal Hecke packet. Every finite commutative algebra over a field is a product of Artin local algebras. Its canonical central idempotents project onto simultaneous generalized eigenspaces. Trace is only a secondary criterion in characteristic zero. Support and localization are the primary notions.
185 
186 The last part assembles these statements into a conditional theorem. A characteristic zero point of \(R\) is automorphic when it lies in the support of the automorphic carrier, the comparison with the Hecke algebra is available, and the corresponding Hecke fiber satisfies the declared realization theorem. If the point belongs to a fixed strictly compatible system, equality of Frobenius polynomials propagates the automorphic identification to every coefficient place by Chebotarev density and Brauer Nesbitt \cite{BrauerNesbitt1941,Neukirch1999,Gee2022}.
187 
188 \begin{figure}[t]
189 \centering
190 \includegraphics[width=.98\textwidth]{01_global_gates.pdf}
191 \caption{The global argument has several logically separate gates.}
192 \label{fig:global_gates}
193 \end{figure}
194 
195 Local quotient conditions are developed in \cref{sec:local_conditions}. Adequacy and residual occupancy appear in \cref{sec:adequacy}. Auxiliary group algebras are treated in \cref{sec:auxiliary}. Ordinary and derived patching support appear in \cref{sec:patching_support}. The effect of \(R\cong\TT\) is isolated in \cref{sec:rt}. Finite Hecke packets and infinite occupancy are developed in \cref{sec:hecke_packets}. Pointwise automorphy and compatible systems appear in \cref{sec:pointwise,sec:compatible}. The coefficient prime two is discussed in \cref{sec:two}. The final conditional theorem is stated in \cref{sec:completion}.
196 
197 \section{Global deformation data and exact boundaries}\label{sec:global_data}
198 
199 Throughout, \(S\) is a finite set of places. Frobenius elements are geometric Frobenius elements. All Hecke polynomials, attached representations, and common algebraic spines use that same convention and the normalization specified by the declared realization theorem.
200 
201 
202 Let \(F\) be a number field. Fix a prime \(p\), a finite extension \(E/\QQ_p\), its valuation ring \(\OO\), uniformizer \(\varpi\), and residue field \(k\). Let
203 \[
204 \bar\rho:G_{F,S}\longrightarrow\GL_n(k)
205 \]
206 be a continuous residual representation, where \(S\) is a finite set of places containing every place at which the deformation problem is allowed to ramify.
207 
208 \begin{definition}[Global deformation datum]\label{def:global_datum}
209 A global deformation datum consists of the following objects.
210 \begin{enumerate}
211 \item A residual representation \(\bar\rho\).
212 \item For every \(v\in S\), a framed local deformation ring \(R_v^\square\).
213 \item A quotient \(R_v^{\tau_v}\) representing the chosen local condition whenever such a quotient is known to exist.
214 \item A global deformation ring \(R^\square\) with a continuous local map
215 \[
216 R^{\mathrm{loc}}:=\wideotimes_{v\in S,\OO}R_v^\square
217 \longrightarrow R^\square.
218 \]
219 \item The induced global ring with local conditions
220 \[
221 R^{\tau}:=R^\square\wideotimes_{R^{\mathrm{loc}}}R^{\mathrm{loc},\tau},
222 \qquad
223 R^{\mathrm{loc},\tau}:=\wideotimes_{v\in S,\OO}R_v^{\tau_v}.
224 \]
225 \end{enumerate}
226 \end{definition}
227 
228 Representability of deformation functors and the construction of local condition quotients require hypotheses. The standard foundations are due to Mazur and Schlessinger, with many later refinements for local conditions and pseudorepresentations \cite{Mazur1989,Schlessinger1968,BellaicheChenevier2009}.
229 
230 \begin{standardfact}[Represented deformation problem]\label{fact:represented_deformation}
231 Under the usual finiteness and Schur type hypotheses, framed lifts of \(\bar\rho\) are represented by complete Noetherian local \(\OO\) algebras. A declared local deformation condition is represented by a quotient when the corresponding subfunctor is representable. Tangent and obstruction spaces are described by the appropriate first and second cohomology groups.
232 \end{standardfact}
233 
234 \begin{standardfact}[Automorphy lifting package]\label{fact:automorphy_package}
235 Published automorphy lifting theorems begin with residual automorphic occupancy and impose hypotheses on the residual image, local deformation conditions, regularity, and the global deformation problem. They then use ordinary or derived patching to compare a deformation ring with a Hecke algebra and to prove automorphy for characteristic zero points in the supported locus. The precise assumptions depend on the theorem being used \cite{ClozelHarrisTaylor2008,BarnetLambGeeGeraghtyTaylor2014,CalegariGeraghty2018,Thorne2012,MiagkovThorne2023,AllenEtAl2023}.
236 \end{standardfact}
237 
238 The chapter treats \cref{fact:represented_deformation,fact:automorphy_package} as external inputs. Its results begin after the relevant rings, modules, complexes, and comparison maps have been supplied.
239 
240 \begin{definition}[Residual automorphic occupancy]\label{def:residual_occupancy}
241 The residual datum \((\bar\rho,\tau)\) is automorphically occupied when a nonzero localized automorphic or cohomological Hecke carrier realizes the residual representation and the declared local conditions.
242 \end{definition}
243 
244 This is a depth zero hypothesis. A positive depth deformation argument above another residual root cannot produce it.
245 
246 \begin{figure}[t]
247 \centering
248 \includegraphics[width=.94\textwidth]{18_claim_boundary.pdf}
249 \caption{The chapter proves formal support and occupancy theorems. It does not prove the universal existence statements shown on the right.}
250 \label{fig:claim_boundary_intro}
251 \end{figure}
252 
253 \section{Local conditions are quotient packets}\label{sec:local_conditions}
254 
255 The completed tensor product combines the local deformation conditions. The first theorem records the exact quotient law.
256 
257 \begin{theorem}[Completed tensor quotient]\label{thm:tensor_quotient}
258 Let \(R_1,\ldots,R_s\) be complete Noetherian local \(\OO\) algebras with common residue field \(k\). Let \(I_i\subseteq R_i\) be closed ideals. Put
259 \[
260 R^{\mathrm{loc}}=R_1\wideotimes_{\OO}\cdots\wideotimes_{\OO}R_s
261 \]
262 and let \(J\) be the closed ideal generated by the images of the \(I_i\). Then there is a canonical isomorphism
263 \[
264 \boxed{
265 (R_1/I_1)\wideotimes_{\OO}\cdots\wideotimes_{\OO}(R_s/I_s)
266 \cong
267 R^{\mathrm{loc}}/J.
268 }
269 \]
270 \end{theorem}
271 
272 \begin{proof}
273 Write \(S=\bigotimes_{i=1}^{s}R_i\) for the ordinary tensor product. Its ideal of definition is
274 \[
275 \fraka=\frakm_{\OO}S+\sum_i\frakm_{R_i}S,
276 \qquad L=\sum_i I_iS.
277 \]
278 The scalar term retains the base adic topology when the family is empty. The ordinary quotient theorem gives a canonical algebra isomorphism
279 \[
280 S/L\cong\bigotimes_{i=1}^{s}(R_i/I_i),
281 \]
282 carrying the image of \(\fraka\) to the defining ideal on the right. The quotient topology on \(S/L\) is precisely this image ideal topology.
283 
284 Here completion means the actual Hausdorff completion for the additive uniformity of the indicated adic topology. For every adic ring \(S\) and ideal \(L\), there is a canonical bicontinuous ring isomorphism
285 \[
286 \widehat S\big/\overline{L\widehat S}\cong\widehat{S/L}.
287 \]
288 Indeed, the completed quotient map kills the closed extended ideal. In the other direction, the quotient map from \(S/L\) to \(\widehat S/\overline{L\widehat S}\) extends to its completion. The latter quotient is complete: the adic uniformity has a countable base, and the quotient of a complete countably based additive group is complete. Its closed defining subgroup makes it Hausdorff. The two composites agree with the identity on dense quotient representatives, so continuity proves both inverse laws.
289 
290 Applying this comparison to the displayed ordinary tensor isomorphism proves the claim. The closed extended ideal is exactly \(J\), since extension commutes with the finite sum of the factor ideals. The maps preserve coefficients and each canonical factor map. The common residue field identifies \(S/\fraka\) with \(k\). Finite generation of \(\fraka\), supplied by the Noetherian factor hypotheses, identifies the completed topology with its maximal ideal topology. Proper quotients retain locality. If a condition is the unit ideal, the ring comparison remains valid with the zero ring, without treating it as a local ring with residue field \(k\).
291 \end{proof}
292 
293 \begin{corollary}[Simultaneous local conditions]\label{cor:simultaneous_local}
294 A continuous point of \(R^{\mathrm{loc}}\) with Hausdorff target factors continuously through \(R^{\mathrm{loc}}/J\) if and only if its restriction to every \(R_i\) factors continuously through \(R_i/I_i\). Each factor is unique. If the original point is local, its quotient factor is local.
295 \end{corollary}
296 
297 \begin{proof}
298 Let \(f:R^{\mathrm{loc}}\to A\) be the point. Since \(A\) is Hausdorff and \(f\) is continuous, \(\ker f\) is closed. Thus it contains the closed ideal \(J\) if and only if it contains the algebraic ideal generated by the images of the \(I_i\). This is equivalent to every local restriction killing \(I_i\). The universal property of the actual ideal quotient gives the factors, and the quotient topology gives their continuity. Surjectivity of the quotient map gives uniqueness. If \(f\) reflects units, lift an element of the quotient to the original ring to see that its factor also reflects units.
299 \end{proof}
300 
301 \begin{proposition}[Global base change for local conditions]\label{prop:global_local_basechange}
302 In the global deformation datum of \cref{def:global_datum}, let \(R^\square\) be a complete Noetherian local \(\OO\) algebra receiving a continuous local \(\OO\) algebra map from \(R^{\mathrm{loc}}\). Then
303 \[
304 R^{\tau}
305 =
306 R^\square\wideotimes_{R^{\mathrm{loc}}}R^{\mathrm{loc},\tau}
307 \]
308 represents the base change of the global deformation problem to the simultaneous local conditions. A continuous local \(\OO\) algebra point of \(R^\square\) with complete Hausdorff coefficient target factors uniquely and continuously through \(R^{\tau}\) exactly when all of its local restrictions satisfy the declared quotient conditions.
309 \end{proposition}
310 
311 \begin{proof}
312 Put \(A=R^{\mathrm{loc}}\), \(B=R^\square\), and let \(J\subseteq A\) be the closed local condition ideal. By \cref{thm:tensor_quotient}, the independently constructed ring \(R^{\mathrm{loc},\tau}\) is canonically \(A/J\). The ordinary tensor identity
313 \[
314 B\otimes_A(A/J)\cong B/JB
315 \]
316 carries the defining ideal of the tensor to the image of \(\frakm_B\). Here the structural map is local by the stated global deformation datum, so it carries \(\frakm_A\) into \(\frakm_B\). Completing, and applying the completion and quotient comparison from the preceding proof, gives a bicontinuous isomorphism
317 \[
318 R^\tau\cong B/\overline{JB}.
319 \]
320 The construction commutes with the canonical map from \(B\), which is therefore surjective. It is also unchanged by transporting the tensor factor from \(A/J\) to the actual completed tensor of the local quotients. The transported ideal is exactly its natural defining ideal.
321 
322 For a continuous algebra point \(x:B\to C\) with complete Hausdorff target, the kernel of \(x\) is closed. Consequently \(x\) has a unique continuous factor through \(R^\tau\) if and only if it kills \(JB\), equivalently if its restriction to \(A\) kills \(J\). By \cref{cor:simultaneous_local}, this is exactly the requirement that all local restrictions satisfy their quotient conditions. The factor is an algebra map because its composite with the canonical global map is \(x\). If \(x\) is local, surjectivity of that map shows that its factor reflects units and is local. Uniqueness also proves naturality under coefficient preserving maps of targets. This identifies the represented base change. It does not supply representability of a new arithmetic deformation problem.
323 \end{proof}
324 
325 The local coefficient points in \cref{prop:global_local_basechange} are test rings in the represented deformation category. Later field valued points \(x:R\to E'\) are algebraic or generic specializations, and continuity of \(\rho_x\) is imposed separately. Such a field specialization need not be a local ring map: under \(\OO\to E\), a uniformizer becomes a unit.
326 
327 \begin{proposition}[Idempotents in a local ring]\label{prop:local_idempotent}
328 If \(R\) is a commutative local ring, then its only idempotents are zero and one.
329 \end{proposition}
330 
331 \begin{proof}
332 Let \(e^2=e\). Since \(e+(1-e)=1\), at least one of \(e\) and \(1-e\) is a unit. If \(e\) is a unit, then \(e=1\). If \(1-e\) is a unit, then \(e=0\).
333 \end{proof}
334 
335 \begin{remark}\label{rem:components_not_idempotents}
336 An irreducible component of \(\Spec R\) for a local deformation ring need not be open and closed. It therefore need not be selected by an idempotent. Components and local conditions should be described by quotient ideals and module support. Idempotent packet formulas are reserved for finite Artin algebras or other settings with an actual product decomposition.
337 \end{remark}
338 
339 \begin{figure}[t]
340 \centering
341 \includegraphics[width=.9\textwidth]{02_local_quotient_packets.pdf}
342 \caption{Local conditions are imposed by quotient rings. Components are support loci unless a genuine product decomposition exists.}
343 \label{fig:local_quotients}
344 \end{figure}
345 
346 \section{Adequacy and the residual input}\label{sec:adequacy}
347 
348 Adequacy is one of the residual image hypotheses used in several automorphy lifting theorems. The definition and its role are external to the support arguments below \cite{GuralnickHerzigTaylorThorne2012,Thorne2012,MiagkovThorne2023}.
349 
350 \begin{standardfact}[Adequate image]\label{fact:adequacy}
351 Let \(G\subseteq\GL(V)\) act absolutely irreducibly over a finite field \(k\) of characteristic \(p\). Under the standard definition, adequacy imposes vanishing conditions on \(H^1(G,k)\) and \(H^1(G,\ad^0V)\), a scalar condition, and a generalized eigenspace detection condition for every irreducible submodule of \(\ad^0V\).
352 \end{standardfact}
353 
354 The following small example makes the projector detection condition explicit. It is a certificate for one finite representation, not a new adequacy criterion.
355 
356 Let \(G=S_3\), let \(k=\FF_7\), and let \(V\) be the standard two dimensional representation. In the basis
357 \[
358 v_1=(1,-1,0),
359 \qquad
360 v_2=(0,1,-1),
361 \]
362 a transposition and a three cycle act by
363 \[
364 s=
365 \begin{pmatrix}
366 6&1\\
367 0&1
368 \end{pmatrix},
369 \qquad
370 t=
371 \begin{pmatrix}
372 0&6\\
373 1&6
374 \end{pmatrix}.
375 \]
376 
377 \begin{theorem}[Finite adequacy certificate]\label{thm:s3_adequacy}
378 The standard representation of \(S_3\) over \(\FF_7\) is adequate. More precisely,
379 \[
380 H^0(S_3,\ad^0V)=0,
381 \qquad
382 H^1(S_3,\FF_7)=0,
383 \qquad
384 H^1(S_3,\ad^0V)=0,
385 \]
386 and
387 \[
388 \ad^0V\cong\operatorname{sgn}\oplus V.
389 \]
390 The sign summand is detected by an eigenprojector of a three cycle, and the standard summand is detected by an eigenprojector of a transposition.
391 \end{theorem}
392 
393 \begin{proof}
394 The coordinate map
395 \[
396 (a,b)\longmapsto(a,-a+b,-b)
397 \]
398 identifies the displayed matrices with the permutation action on the sum zero subspace of \(\FF_7^3\). This action is faithful. The four matrices \(1,s,t,st\) span \(M_2\) over every field of characteristic seven: the determinant of their coordinate matrix is \(4\ne0\). A subspace stable under the group is therefore stable under every endomorphism, so the representation is absolutely irreducible. The characteristic polynomials of the identity, transpositions, and three cycles are respectively
399 \[
400 (X-1)^2,\qquad (X-1)(X+1),\qquad (X-2)(X-4).
401 \]
402 Thus all eigenvalues already lie in \(\FF_7\).
403 
404 A trace zero matrix fixed by conjugation by both \(s\) and \(t\) is zero, as follows by comparing its four entries. This proves \(H^0(S_3,\ad^0V)=0\). For any \(\FF_7[S_3]\) module \(M\) and one cocycle \(f\), put
405 \[
406 u=-6^{-1}\sum_{h\in S_3}f(h).
407 \]
408 Summing \(f(gh)=g f(h)+f(g)\) over \(h\) gives \(gu-u=f(g)\). Hence every one cocycle is a coboundary and \(H^1(S_3,M)=0\), giving both asserted first cohomology vanishings.
409 
410 Write
411 \[
412 W(a,b,c)=\begin{pmatrix}a&b\\c&-a\end{pmatrix},
413 \qquad
414 Z=W(2,3,4),\quad A=W(1,1,2),\quad B=W(1,5,6).
415 \]
416 The three coordinate columns have determinant \(3\ne0\). Under conjugation,
417 \[
418 sZ=-Z,\quad tZ=Z,\qquad
419 sA=-A,\quad sB=A+B,\quad tA=B,\quad tB=-A-B.
420 \]
421 Consequently \((z,(a,b))\mapsto zZ+aA+bB\) is an equivariant isomorphism from \(\operatorname{sgn}\oplus V\) to \(\ad^0V\).
422 
423 The sign witness is \(W_{\mathrm{sgn}}=Z\), while
424 \(W_{\mathrm{std}}=W(6,4,3)=3A+3B\) belongs to the standard summand. The corresponding projectors and trace pairings are
425 \[
426 P_{t,2}=\begin{pmatrix}2&4\\3&6\end{pmatrix},
427 \qquad \Tr(P_{t,2}W_{\mathrm{sgn}})=3\ne0,
428 \]
429 \[
430 P_{s,1}=\begin{pmatrix}0&4\\0&1\end{pmatrix},
431 \qquad \Tr(P_{s,1}W_{\mathrm{std}})=6\ne0.
432 \]
433 For an operator \(D\) with \((D-\alpha I)(D-\beta I)=0\) and \(\alpha\ne\beta\), the canonical projector is
434 \[
435 P_{D,\alpha}=(\alpha-\beta)^{-1}(D-\beta I).
436 \]
437 Its image equals \(\ker((D-\alpha I)^n)\) for every \(n\ge1\), and it kills \(\ker((D-\beta I)^n)\). This identifies the displayed matrices with the generalized eigenspace projectors required in the adequacy definition.
438 
439 For detection on every irreducible submodule, one can check the stronger assertion that canonical projectors detect every nonzero matrix. In addition to the two projectors above, use
440 \[
441 P_{s,-1}=\begin{pmatrix}1&3\\0&0\end{pmatrix},
442 \qquad
443 P_{tst^{-1},1}=\begin{pmatrix}1&0\\4&0\end{pmatrix}.
444 \]
445 The four trace pairings with these matrices have trivial common kernel in \(M_2(\FF_7)\), by row reduction. Every irreducible adjoint submodule contains a nonzero matrix, so some canonical projector has nonzero trace pairing on that submodule. This verifies the last adequacy clause and completes the certificate.
446 \end{proof}
447 
448 \begin{figure}[t]
449 \centering
450 \includegraphics[width=.86\textwidth]{03_adequacy_packets.pdf}
451 \caption{The two irreducible adjoint packets are detected by different generalized eigenspace projectors.}
452 \label{fig:adequacy_packets}
453 \end{figure}
454 
455 \begin{remark}\label{rem:adequacy_boundary}
456 The theorem verifies adequacy for one finite image. A global automorphy lifting argument must verify the published residual image hypothesis for its actual representation. The calculation does not replace that step, and it does not provide a uniform coefficient prime two theorem.
457 \end{remark}
458 
459 \section{Auxiliary group algebras and augmentation}\label{sec:auxiliary}
460 
461 Let \(\Delta\) be a finite abelian \(p\) group and let
462 \[
463 \Lambda=\OO[\Delta].
464 \]
465 The augmentation map is
466 \[
467 \epsilon:\Lambda\longrightarrow\OO,
468 \qquad
469 \sum_{g\in\Delta}a_gg\longmapsto\sum_{g\in\Delta}a_g.
470 \]
471 Its kernel is the augmentation ideal \(\fraka\).
472 
473 \begin{proposition}[Functorial group algebra transfer]\label{prop:group_algebra_transfer}
474 A group homomorphism \(q:\Delta'\to\Delta\) induces an \(\OO\) algebra homomorphism
475 \[
476 q_*:\OO[\Delta']\longrightarrow\OO[\Delta].
477 \]
478 If \(q\) is surjective, then \(q_*\) is surjective. Augmentation commutes with the transfer:
479 \[
480 \epsilon_\Delta q_*=\epsilon_{\Delta'}.
481 \]
482 \end{proposition}
483 
484 \begin{proof}
485 Extend \(q\) linearly from the group basis. Multiplicativity follows from \(q(gh)=q(g)q(h)\). Surjectivity follows because every basis element of \(\OO[\Delta]\) has a preimage. Both augmentation maps send every group element to one, which gives the final identity.
486 \end{proof}
487 
488 \begin{theorem}[Residual augmentation algebra]\label{thm:residual_augmentation_algebra}
489 Suppose
490 \[
491 \Delta\cong
492 \prod_{i=1}^{r}C_{p^{n_i}}.
493 \]
494 Choose generators \(\gamma_i\), and let \(X_i=\gamma_i-1\). Then
495 \[
496 \boxed{
497 k[\Delta]
498 \cong
499 k[X_1,\ldots,X_r]
500 \big/
501 (X_1^{p^{n_1}},\ldots,X_r^{p^{n_r}}).
502 }
503 \]
504 The augmentation ideal is generated by the \(X_i\), and \(k[\Delta]\) is local.
505 \end{theorem}
506 
507 \begin{proof}
508 In characteristic \(p\),
509 \[
510 (1+X_i)^{p^{n_i}}-1=X_i^{p^{n_i}}.
511 \]
512 Thus the assignment \(X_i\mapsto\gamma_i-1\) gives a surjective homomorphism from the displayed truncated polynomial ring to \(k[\Delta]\). Both sides have dimension \(\prod_ip^{n_i}=\abs{\Delta}\) over \(k\), so the map is an isomorphism. The quotient by the ideal generated by the \(X_i\) is \(k\). Since each \(X_i\) is nilpotent, that ideal is the unique maximal ideal.
513 \end{proof}
514 
515 \begin{corollary}[No residual character splitting]\label{cor:no_residual_character_splitting}
516 The residual group algebra \(k[\Delta]\) has no nontrivial idempotents. In particular, character projectors do not split a finite \(p\) group algebra in residue characteristic \(p\).
517 \end{corollary}
518 
519 \begin{proof}
520 The first assertion follows from locality in \cref{thm:residual_augmentation_algebra}. For the general finite \(p\) group assertion, let \(e\in k[G]\) be idempotent and write \(\epsilon:k[G]\to k\) for augmentation. Suppose \(\epsilon(e)=0\) and \(e\ne0\). The \(\FF_p\) span \(W\) of the left translates \(ge\) is a nonzero finite dimensional \(\FF_p\) vector space, stable under \(G\). Its cardinality is divisible by \(p\). The orbit counting formula implies that its fixed point set also has cardinality divisible by \(p\). Since zero is fixed, there is a nonzero fixed vector \(v\in W\).
521 
522 A vector in the regular representation fixed by all left translations has constant coefficients. Consequently \(ve=\epsilon(e)v=0\). On the other hand, \(e^2=e\) implies \(we=w\) for every \(w\in W\), hence \(ve=v\), a contradiction. Thus every idempotent of augmentation zero is zero. Since \(\epsilon(e)^2=\epsilon(e)\) in the field \(k\), either \(\epsilon(e)=0\) or \(\epsilon(e)=1\). In the latter case, apply the preceding argument to \(1-e\).
523 \end{proof}
524 
525 For \(M\otimes_{\Lambda,\epsilon}\OO\), we use a right \(\Lambda\) module \(M\). The left module convention is \(\OO\otimes_{\Lambda,\epsilon}M\). Throughout, \(\fraka M\) denotes the augmentation relation submodule: it is generated by \(ma\) for right modules and by \(am\) for left modules, with \(a\in\fraka\). This convention also applies to nonabelian groups in \cref{cor:dyadic_coinvariant_recovery}. For abelian groups, both tensor orders agree over the commutative group algebra.
526 
527 \begin{theorem}[Coinvariant recovery]\label{thm:coinvariant_recovery}
528 Let \(M\) be a free \(\Lambda\) module of rank \(d\). Then
529 \[
530 \boxed{
531 M/\fraka M
532 \cong
533 M\otimes_{\Lambda,\epsilon}\OO
534 \cong
535 \OO^d.
536 }
537 \]
538 The statement is valid for every coefficient prime, including two.
539 \end{theorem}
540 
541 \begin{proof}
542 Choose a \(\Lambda\) basis of \(M\). Tensoring the resulting isomorphism \(M\cong\Lambda^d\) along augmentation gives \(\OO^d\). Tensoring by \(\Lambda/\fraka\) is the same as quotienting by \(\fraka M\).
543 \end{proof}
544 
545 \begin{standardfact}[Iwasawa limit]\label{fact:iwasawa_limit}
546 For \(\Delta_m=(\ZZ/p^m\ZZ)^r\), the inverse limit of \(\OO[\Delta_m]\) is the Iwasawa algebra
547 \[
548 \OO[[\ZZ_p^r]]\cong\OO[[X_1,\ldots,X_r]],
549 \]
550 where \(X_i\) corresponds to a chosen topological generator minus one \cite{RibesZalesskii2010}.
551 \end{standardfact}
552 
553 \begin{figure}[t]
554 \centering
555 \includegraphics[width=.94\textwidth]{04_auxiliary_group_tower.pdf}
556 \caption{Auxiliary group algebras refine through quotient maps, while augmentation recovers the coarse level.}
557 \label{fig:auxiliary_tower}
558 \end{figure}
559 
560 \begin{figure}[t]
561 \centering
562 \includegraphics[width=.88\textwidth]{05_augmentation_algebra.pdf}
563 \caption{The residual auxiliary algebra is a local truncated polynomial algebra at every coefficient prime.}
564 \label{fig:augmentation_algebra}
565 \end{figure}
566 
567 The augmentation formalism is uniform in \(p\). The difficult coefficient two questions lie elsewhere. Residual image hypotheses, local deformation geometry, and classicality may change at two even though coinvariant recovery remains exact.
568 
569 
570 \section{Ordinary and derived patching support}\label{sec:patching_support}
571 
572 The algebraic conclusion supplied by a patching argument is most naturally stated through support. This section isolates the commutative algebra needed to descend that conclusion from a patched object to finite level.
573 
574 \begin{definition}[Support and near faithfulness]\label{def:support_near_faithful}
575 Let \(R\) be a commutative ring and let \(M\) be an \(R\) module. Its support is
576 \[
577 \Supp_R(M)
578 =
579 \{\frakp\in\Spec R:M_{\frakp}\neq0\}.
580 \]
581 If \(R\) is Noetherian and \(M\) is finite, then \(M\) is \emph{nearly faithful} when \(\Ann_R(M)\) is a nilpotent ideal.
582 \end{definition}
583 
584 \begin{theorem}[Finite module support]\label{thm:finite_module_support}
585 Let \(R\) be a commutative ring and let \(M\) be a finite \(R\) module. Then
586 \[
587 \boxed{
588 \Supp_R(M)
589 =
590 V\bigl(\Ann_R(M)\bigr).
591 }
592 \]
593 \end{theorem}
594 
595 \begin{proof}
596 Let \(\frakp\in\Spec R\). If \(\Ann_R(M)\not\subseteq\frakp\), choose
597 \(a\in\Ann_R(M)\setminus\frakp\). The element \(a\) becomes a unit in
598 \(R_{\frakp}\), so \(M_{\frakp}=0\).
599 
600 Conversely, suppose \(M_{\frakp}=0\). Choose generators
601 \(m_1,\ldots,m_d\) of \(M\). For each \(i\), there is an element
602 \(s_i\notin\frakp\) such that \(s_im_i=0\). The product
603 \(s=s_1\cdots s_d\) lies outside \(\frakp\) and annihilates every generator.
604 Thus \(s\in\Ann_R(M)\setminus\frakp\). This proves the equality.
605 \end{proof}
606 
607 \begin{theorem}[Fitting support criterion]\label{thm:fitting_support}
608 Let \(R\) be Noetherian and let \(M\) be a finite \(R\) module. Then
609 \[
610 \boxed{
611 \Supp_R(M)
612 =
613 V\bigl(\Fitt_0^R(M)\bigr).
614 }
615 \]
616 \end{theorem}
617 
618 \begin{proof}
619 If \(M=0\), the statement follows from the usual convention \(\Fitt_0(0)=R\). Assume \(M\neq0\), and choose a finite presentation
620 \[
621 R^m\xrightarrow{A}R^n\longrightarrow M\longrightarrow0
622 \]
623 with \(n\geq1\).
624 The zeroth Fitting ideal is generated by the \(n\) by \(n\) minors of \(A\). After localization at a prime \(\frakp\), the module \(M_{\frakp}\) vanishes exactly when \(A_{\frakp}\) is surjective. A map onto the free module \(R_{\frakp}^n\) is surjective exactly when one maximal minor is a unit. Thus \(M_{\frakp}=0\) exactly when \(\Fitt_0^R(M)\not\subseteq\frakp\).
625 \end{proof}
626 
627 \begin{theorem}[Higher Fitting strata]\label{thm:higher_fitting_strata}
628 Let \(R\) be Noetherian and let \(M\) be finite. For \(r\geq1\), put
629 \[
630 \mu_{\frakp}(M)
631 =
632 \dim_{\kappa(\frakp)}
633 \left(M\otimes_R\kappa(\frakp)\right).
634 \]
635 Then
636 \[
637 \boxed{
638 \left\{
639 \frakp\in\Spec R:
640 \mu_{\frakp}(M)\geq r
641 \right\}
642 =
643 V\bigl(\Fitt_{r-1}^R(M)\bigr).
644 }
645 \]
646 \end{theorem}
647 
648 \begin{proof}
649 Use a finite presentation with target rank \(n\). If \(r>n\), every fiber has dimension at most \(n\), so the left-hand locus is empty. The convention \(\Fitt_{r-1}(M)=R\) for \(r-1\geq n\) makes the right-hand locus empty as well. It remains to consider \(1\leq r\leq n\). At \(\frakp\), the fiber dimension is
650 \[
651 n-\rank A(\frakp).
652 \]
653 It is at least \(r\) exactly when the rank is at most \(n-r\), which is equivalent to the vanishing of every minor of size \(n-r+1\). Those minors generate \(\Fitt_{r-1}^R(M)\).
654 \end{proof}
655 
656 \begin{proposition}[Fitting ideals and base change]\label{prop:fitting_base_change}
657 Let \(R\to S\) be a ring map and let \(M\) be a finitely presented \(R\) module. Then for every \(j\geq0\),
658 \[
659 \boxed{
660 \Fitt_j^S(M\otimes_RS)
661 =
662 \Fitt_j^R(M)S.
663 }
664 \]
665 \end{proposition}
666 
667 \begin{proof}
668 Base change carries a finite presentation matrix for \(M\) to a presentation matrix for \(M\otimes_RS\). Every defining minor is carried to the corresponding minor over \(S\).
669 \end{proof}
670 
671 \begin{remark}
672 Support records nonvanishing. The higher Fitting strata record lower bounds on the number of generators in each fiber. They should not be confused with automorphic multiplicity formulas, which require additional representation theoretic input.
673 \end{remark}
674 
675 \begin{theorem}[Near faithfulness is full support]\label{thm:near_faithful_full_support}
676 Let \(R\) be Noetherian and let \(M\) be a finite \(R\) module. The following conditions are equivalent.
677 \begin{enumerate}
678 \item \(M\) is nearly faithful.
679 \item \(\Supp_R(M)=\Spec R\).
680 \item \(\Ann_R(M)\subseteq\nil(R)\).
681 \end{enumerate}
682 If \(R\) is reduced, these conditions are equivalent to faithfulness.
683 \end{theorem}
684 
685 \begin{proof}
686 By \cref{thm:finite_module_support}, full support is equivalent to
687 \[
688 V\bigl(\Ann_R(M)\bigr)=\Spec R.
689 \]
690 This holds exactly when \(\Ann_R(M)\) is contained in every prime ideal, hence in the nilradical. Because \(R\) is Noetherian, the ideal \(\Ann_R(M)\) is finitely generated. An ideal generated by finitely many nilpotent elements is nilpotent. This proves the equivalence of the first three conditions. If \(R\) is reduced, its nilradical is zero.
691 \end{proof}
692 
693 \begin{corollary}[Support on every irreducible component]\label{cor:every_component_support}
694 Under the hypotheses of \cref{thm:near_faithful_full_support}, a nearly faithful module is nonzero at the generic point of every irreducible component of \(\Spec R\).
695 \end{corollary}
696 
697 \begin{proof}
698 Every generic point is a prime of \(R\), and full support contains every prime.
699 \end{proof}
700 
701 \begin{theorem}[Support after a quotient]\label{thm:quotient_support}
702 Let \(R\) be Noetherian, let \(I\subseteq R\) be an ideal, and let \(M\) be a finite \(R\) module. Under the canonical identification
703 \[
704 \Spec(R/I)\cong V(I)\subseteq\Spec R,
705 \]
706 one has
707 \[
708 \boxed{
709 \Supp_{R/I}(M/IM)
710 =
711 \Supp_R(M)\cap V(I).
712 }
713 \]
714 \end{theorem}
715 
716 \begin{proof}
717 Let \(\frakp\supseteq I\). Localizing gives
718 \[
719 (M/IM)_{\frakp}
720 \cong
721 M_{\frakp}/I_{\frakp}M_{\frakp}.
722 \]
723 If \(M_{\frakp}=0\), the quotient is zero. If \(M_{\frakp}\neq0\), then
724 \(I_{\frakp}\) lies in the maximal ideal of the local ring \(R_{\frakp}\). Nakayama's lemma shows that
725 \(M_{\frakp}/I_{\frakp}M_{\frakp}\neq0\). The stated equality follows.
726 \end{proof}
727 
728 \begin{definition}[Ordinary patching datum]\label{def:ordinary_patching_datum}
729 An ordinary patching datum consists of a Noetherian ring \(R_\infty\), an ideal
730 \(\fraka\subseteq R_\infty\), a finite \(R_\infty\) module \(M_\infty\), and identifications
731 \[
732 R\cong R_\infty/\fraka,
733 \qquad
734 M\cong M_\infty/\fraka M_\infty.
735 \]
736 In automorphy lifting applications, \(R_\infty\) is a patched deformation ring and \(M_\infty\) is a patched automorphic module. The definition itself contains no automorphy assertion.
737 \end{definition}
738 
739 \begin{theorem}[Ordinary patching support descent]\label{thm:ordinary_support_descent}
740 Let \((R_\infty,\fraka,M_\infty,R,M)\) be an ordinary patching datum. If
741 \[
742 \Supp_{R_\infty}(M_\infty)=\Spec R_\infty,
743 \]
744 then
745 \[
746 \boxed{
747 \Supp_R(M)=\Spec R.
748 }
749 \]
750 Equivalently, if \(M_\infty\) is nearly faithful, then \(M\) is nearly faithful. If \(R\) is reduced, then \(M\) is faithful.
751 \end{theorem}
752 
753 \begin{proof}
754 Apply \cref{thm:quotient_support} with \(I=\fraka\). The support of the quotient is
755 \[
756 \Spec R_\infty\cap V(\fraka)=V(\fraka),
757 \]
758 which identifies with \(\Spec R\). The remaining statements follow from
759 \cref{thm:near_faithful_full_support}.
760 \end{proof}
761 
762 \begin{corollary}[Componentwise finite level occupancy]\label{cor:componentwise_occupancy}
763 In the setting of \cref{thm:ordinary_support_descent}, every irreducible component of
764 \(\Spec R\) is contained in the support of \(M\). In particular, no component of the finite level deformation ring is erased by the quotient from the patched level.
765 \end{corollary}
766 
767 \begin{proof}
768 The module \(M\) has full support by \cref{thm:ordinary_support_descent}.
769 \end{proof}
770 
771 \begin{example}[Freeness over auxiliary variables is not enough]\label{ex:freeness_not_support}
772 Let \(k\) be a field, let \(S=k[[t]]\), and put
773 \[
774 R=S[[x]]/(x(x-t)).
775 \]
776 The ring \(R\) is reduced and has two irreducible components. Let
777 \[
778 M=R/(x)\cong S.
779 \]
780 Then \(M\) is free of rank one over \(S\), but
781 \[
782 \Supp_R(M)=V(x)
783 \]
784 is only one component of \(\Spec R\). Thus freeness over the auxiliary power series ring does not imply full support over the deformation ring.
785 \end{example}
786 
787 \begin{proof}
788 The two nonassociate prime factors \(x\) and \(x-t\) occur with multiplicity one, so the principal quotient is reduced. The displayed isomorphism makes \(M\) free over \(S\). Its annihilator as an \(R\) module is \((x)\), hence
789 \[
790 \Supp_R(M)=V(x)
791 \]
792 by \cref{thm:finite_module_support}. The generic point \((x-t)\) of the other component does not contain \(x\), so it is not in the support.
793 \end{proof}
794 
795 \begin{figure}[t]
796 \centering
797 \includegraphics[width=.94\textwidth]{06_patching_support_descent.pdf}
798 \caption{Full support at the patched level descends through the augmentation quotient.}
799 \label{fig:patching_support_descent}
800 \end{figure}
801 
802 \begin{figure}[t]
803 \centering
804 \includegraphics[width=.86\textwidth]{07_freeness_counterexample.pdf}
805 \caption{A module can be free over the auxiliary ring while occupying only one deformation component.}
806 \label{fig:freeness_counterexample}
807 \end{figure}
808 
809 Derived patching replaces one module by a perfect complex. The correct support is detected after derived specialization.
810 
811 \begin{definition}[Derived support]\label{def:derived_support}
812 Let \(R\) be a commutative ring and let \(C\) be a perfect complex of \(R\) modules. Its derived support is
813 \[
814 \Supp_R(C)
815 =
816 \left\{
817 \frakp\in\Spec R:
818 C\mathbin{\mathop{\otimes}\limits_R^{\mathbf L}}\kappa(\frakp)
819 \not\simeq0
820 \right\}.
821 \]
822 \end{definition}
823 
824 \begin{standardfact}[Cohomological description of derived support]\label{fact:derived_support_cohomology}
825 If \(R\) is Noetherian and \(C\) is perfect, then
826 \[
827 \Supp_R(C)
828 =
829 \bigcup_i\Supp_R H^i(C).
830 \]
831 In particular, derived support is closed and is empty exactly when \(C\simeq0\) \cite{Weibel1994,Eisenbud1995}.
832 \end{standardfact}
833 
834 \begin{theorem}[Derived quotient support]\label{thm:derived_quotient_support}
835 Let \(R\) be a commutative ring, let \(I\subseteq R\) be an ideal, and let \(C\) be a perfect complex over \(R\). Under
836 \(\Spec(R/I)\cong V(I)\), one has
837 \[
838 \boxed{
839 \Supp_{R/I}
840 \left(
841 C\mathbin{\mathop{\otimes}\limits_R^{\mathbf L}}R/I
842 \right)
843 =
844 \Supp_R(C)\cap V(I).
845 }
846 \]
847 \end{theorem}
848 
849 \begin{proof}
850 Choose a bounded complex \(P\) of finite projective \(R\) modules representing \(C\). Scalar extension to a commutative \(R\) algebra \(S\) is computed degree by degree as \(S\otimes_RP\). The canonical symmetry of tensor products gives the displayed order \(C\otimes_R^{\mathbf L}S\). Scalar extension preserves the bounds, finite generation, and projectivity of the terms. A derived isomorphism between two such projective models lifts to a homotopy equivalence, which scalar extension preserves. The resulting derived object and its residue field fibers are therefore independent of the chosen model.
851 
852 Let \(q\in\Spec(R/I)\), and let \(\frakp\) be its inverse image in \(R\). The composite point \(R\to R/I\to\kappa(q)\) has kernel \(\frakp\), so it factors through a field embedding \(\kappa(\frakp)\to\kappa(q)\). The ordinary tensor associator in every degree gives an isomorphism of complexes
853 \[
854 \kappa(q)\otimes_{R/I}\bigl((R/I)\otimes_RP\bigr)
855 \cong\kappa(q)\otimes_RP
856 \cong\kappa(q)\otimes_{\kappa(\frakp)}
857 \bigl(\kappa(\frakp)\otimes_RP\bigr).
858 \]
859 Extension of fields is faithfully flat. It preserves and reflects exactness in each degree, hence also acyclicity. The left-hand complex is thus nonzero in the derived category exactly when the residue field fiber of \(C\) at \(\frakp\) is nonzero. This proves the support identity on corresponding primes. The image of \(\Spec(R/I)\to\Spec R\) is exactly \(V(I)\), giving the stated ambient spectrum equality, including the case \(I=R\).
860 \end{proof}
861 
862 \begin{definition}[Derived patching datum]\label{def:derived_patching_datum}
863 A derived patching datum consists of a Noetherian ring \(R_\infty\), an ideal
864 \(\fraka\), a perfect complex \(C_\infty\) over \(R_\infty\), and identifications
865 \[
866 R\cong R_\infty/\fraka,
867 \qquad
868 C\simeq
869 C_\infty
870 \mathbin{\mathop{\otimes}\limits_{R_\infty}^{\mathbf L}}R.
871 \]
872 \end{definition}
873 
874 \begin{theorem}[Derived patching support descent]\label{thm:derived_support_descent}
875 Let \((R_\infty,\fraka,C_\infty,R,C)\) be a derived patching datum. If
876 \[
877 \Supp_{R_\infty}(C_\infty)=\Spec R_\infty,
878 \]
879 then
880 \[
881 \boxed{
882 \Supp_R(C)=\Spec R.
883 }
884 \]
885 For every point \(x:R\to E'\) to a field, the derived fiber
886 \[
887 C\mathbin{\mathop{\otimes}\limits_{R,x}^{\mathbf L}}E'
888 \]
889 is nonzero.
890 \end{theorem}
891 
892 \begin{proof}
893 Apply \cref{thm:derived_quotient_support} to the patched complex and use the actual ring identification \(R\cong R_\infty/\fraka\). Full patched support restricts to \(V(\fraka)\), which corresponds to all of \(\Spec R\). The supplied derived isomorphism with \(C\) preserves this support by the projective model argument in that theorem.
894 
895 For a field valued point \(x:R\to E'\), put \(\frakp=\ker x\). The point factors as \(R\to\kappa(\frakp)\to E'\), where the second map is a field embedding. Tensor association on a projective model identifies the fiber at \(x\) with the extension to \(E'\) of the fiber at \(\frakp\). The latter is nonzero by full support. Faithful flatness of the field extension reflects exactness in every degree, so the fiber at \(x\) is nonzero as well. This applies to every field valued point, with no closed point restriction.
896 \end{proof}
897 
898 \begin{corollary}[A nonzero cohomological degree survives]\label{cor:derived_degree_survives}
899 Under the hypotheses of \cref{thm:derived_support_descent}, for every field valued point \(x:R\to E'\), there is an integer \(i\) such that
900 \[
901 H^i
902 \left(
903 C\mathbin{\mathop{\otimes}\limits_{R,x}^{\mathbf L}}E'
904 \right)
905 \neq0.
906 \]
907 \end{corollary}
908 
909 \begin{proof}
910 The derived fiber is nonzero by \cref{thm:derived_support_descent}. If every cohomology object vanished, a cochain model of that fiber would be acyclic. Its image in the derived category would then be zero, a contradiction. Hence some integer degree has nonzero cohomology.
911 \end{proof}
912 
913 \begin{remark}
914 The support theorem does not decide the cohomological degree in which the point occurs. It also does not prove that the surviving class is classical. Those are separate arithmetic inputs.
915 \end{remark}
916 
917 \section{Transport through an isomorphism \texorpdfstring{\(R\cong\TT\)}{R equals T}}\label{sec:rt}
918 
919 An isomorphism between a deformation ring and a Hecke algebra is an exact coordinate change. It transports support and finite presentation data, but it does not create a supported module.
920 
921 \begin{theorem}[Support and Fitting transport]\label{thm:rt_support_transport}
922 Let \(\varphi:R\to\TT\) be an isomorphism of Noetherian rings. Let \(M\) be a finite \(\TT\) module, viewed as an \(R\) module through \(\varphi\). Then the homeomorphism
923 \[
924 \varphi^*:\Spec\TT\longrightarrow\Spec R
925 \]
926 satisfies
927 \[
928 \boxed{
929 \varphi^*\bigl(\Supp_{\TT}(M)\bigr)
930 =
931 \Supp_R(M).
932 }
933 \]
934 For every \(j\geq0\),
935 \[
936 \boxed{
937 \varphi
938 \left(
939 \Fitt_j^R(M)
940 \right)
941 =
942 \Fitt_j^{\TT}(M).
943 }
944 \]
945 \end{theorem}
946 
947 \begin{proof}
948 Localization commutes with transport along an isomorphism, so a localization of \(M\) vanishes on one side exactly when the corresponding localization vanishes on the other. This proves the support identity. A finite presentation matrix over \(R\) is carried entry by entry to a presentation matrix over \(\TT\). The minors generating each Fitting ideal are therefore carried to the corresponding minors.
949 \end{proof}
950 
951 \begin{corollary}[Full support is invariant under \texorpdfstring{\(R\cong\TT\)}{R equals T}]\label{cor:rt_full_support}
952 In the setting of \cref{thm:rt_support_transport}, \(M\) has full \(R\) support if and only if it has full \(\TT\) support.
953 \end{corollary}
954 
955 \begin{proof}
956 Apply the support homeomorphism in \cref{thm:rt_support_transport}.
957 \end{proof}
958 
959 \begin{proposition}[A quotient can erase a component]\label{prop:quotient_erases_component}
960 Let
961 \[
962 R=k[[x,y]]/(xy)
963 \]
964 and let
965 \[
966 \TT=R/(x)\cong k[[y]].
967 \]
968 Viewed as an \(R\) module, \(\TT\) has support \(V(x)\), which misses the generic point \((y)\) of the other irreducible component. Thus a surjection \(R\twoheadrightarrow\TT\) does not by itself imply full component occupancy.
969 \end{proposition}
970 
971 \begin{proof}
972 The annihilator of the \(R\) module \(\TT\) is \((x)\). Hence its support is \(V(x)\) by \cref{thm:finite_module_support}. The prime \((y)\) does not contain \(x\), so it is not in this support.
973 \end{proof}
974 
975 \begin{theorem}[Field fiber criterion]\label{thm:field_fiber_criterion}
976 Let \(R\) be a commutative ring, let \(M\) be a finite \(R\) module, and let
977 \(x:R\to E'\) be a homomorphism to a field. Put \(\frakp=\ker x\). Then
978 \[
979 \boxed{
980 M\otimes_{R,x}E'\neq0
981 \quad\Longleftrightarrow\quad
982 \frakp\in\Supp_R(M).
983 }
984 \]
985 \end{theorem}
986 
987 \begin{proof}
988 The map \(x\) factors through the local ring \(R_{\frakp}\) and then through an embedding of the residue field \(\kappa(\frakp)\) into \(E'\). Since \(M\) is finite, Nakayama's lemma gives
989 \[
990 M_{\frakp}\neq0
991 \quad\Longleftrightarrow\quad
992 M\otimes_R\kappa(\frakp)\neq0.
993 \]
994 Extension of scalars from \(\kappa(\frakp)\) to \(E'\) preserves nonzero vector spaces.
995 \end{proof}
996 
997 \begin{corollary}[Supported deformation points give nonzero Hecke fibers]\label{cor:supported_hecke_fiber}
998 Let \(R\cong\TT\), and let \(M\) be a finite Hecke module. If a point
999 \(x:R\to E'\) lies in \(\Supp_R(M)\), then the corresponding Hecke fiber
1000 \[
1001 M\otimes_{\TT,x}E'
1002 \]
1003 is nonzero.
1004 \end{corollary}
1005 
1006 \begin{proof}
1007 Transport the support through \cref{thm:rt_support_transport}, then apply
1008 \cref{thm:field_fiber_criterion}.
1009 \end{proof}
1010 
1011 \begin{figure}[t]
1012 \centering
1013 \includegraphics[width=.94\textwidth]{08_rt_support_transport.pdf}
1014 \caption{An isomorphism transports occupied support exactly. A quotient can remove a component.}
1015 \label{fig:rt_support_transport}
1016 \end{figure}
1017 
1018 \section{Finite Hecke packets and infinite occupancy}\label{sec:hecke_packets}
1019 
1020 Finite Hecke carriers admit canonical packets even when the Hecke action is not semisimple. The packets come from the Artin local factors of the finite commutative Hecke algebra.
1021 
1022 \begin{standardfact}[Artin decomposition]\label{fact:artin_decomposition}
1023 Let \(E'\) be a field and let \(\TT\) be a finite dimensional commutative
1024 \(E'\) algebra. Then
1025 \[
1026 \boxed{
1027 \TT
1028 \cong
1029 \prod_{\frakm\in\Max\TT}\TT_{\frakm}.
1030 }
1031 \]
1032 Each factor is an Artin local algebra. Equivalently, there is a unique complete family of central idempotents \((e_{\frakm})\) such that
1033 \[
1034 e_{\frakm}e_{\mathfrak n}=0
1035 \quad(\frakm\neq\mathfrak n),
1036 \qquad
1037 \sum_{\frakm}e_{\frakm}=1,
1038 \]
1039 and \(e_{\frakm}\TT\cong\TT_{\frakm}\) \cite{AtiyahMacdonald1969,Matsumura1989}.
1040 \end{standardfact}
1041 
1042 \begin{theorem}[Canonical Hecke packet decomposition]\label{thm:canonical_hecke_packets}
1043 Let \(\TT\) be a finite dimensional commutative algebra over a field \(E'\), and let \(V\) be a finite \(\TT\) module. Then
1044 \[
1045 \boxed{
1046 V
1047 =
1048 \bigoplus_{\frakm\in\Max\TT}e_{\frakm}V.
1049 }
1050 \]
1051 For every maximal ideal \(\frakm\), the canonical map gives
1052 \[
1053 \boxed{
1054 e_{\frakm}V\cong V_{\frakm}.}
1055 \]
1056 The packet \(e_{\frakm}V\) is nonzero exactly when \(\frakm\in\Supp_{\TT}(V)\).
1057 \end{theorem}
1058 
1059 \begin{proof}
1060 The idempotent relations in \cref{fact:artin_decomposition} give the direct sum decomposition. Localization at \(\frakm\) kills every factor except the \(\frakm\) factor, where \(e_{\frakm}\) becomes one. Thus the localization map identifies \(e_{\frakm}V\) with \(V_{\frakm}\). The final statement is the definition of support.
1061 \end{proof}
1062 
1063 \begin{corollary}[Simultaneous generalized eigenspaces]\label{cor:simultaneous_generalized_eigenspaces}
1064 Assume that \(E'\) is algebraically closed and that \(\TT\) is generated by commuting operators \(T_1,\ldots,T_d\) on \(V\). For a maximal ideal
1065 \[
1066 \frakm
1067 =
1068 (T_1-\lambda_1,\ldots,T_d-\lambda_d),
1069 \]
1070 there is an integer \(N\geq1\) such that
1071 \[
1072 \boxed{
1073 e_{\frakm}V
1074 =
1075 \left\{
1076 v\in V:
1077 (T_i-\lambda_i)^Nv=0
1078 \text{ for every }i
1079 \right\}.
1080 }
1081 \]
1082 Thus the canonical Artin packet is the simultaneous generalized eigenspace.
1083 \end{corollary}
1084 
1085 \begin{proof}
1086 The maximal ideal of the Artin local algebra \(\TT_{\frakm}\) is nilpotent. Hence a common power of every \(T_i-\lambda_i\) kills the local packet. On every other local factor, at least one \(T_i-\lambda_i\) is a unit, so no nonzero vector can satisfy all the displayed nilpotence conditions.
1087 
1088 Conversely, suppose every \((T_i-\lambda_i)^N\) kills \(v\). Every monomial of total degree greater than \(d(N-1)\) contains one factor to exponent at least \(N\). Therefore a power of \(\frakm\) kills \(v\), which places \(v\) in the \(\frakm\) primary packet.
1089 \end{proof}
1090 
1091 \begin{corollary}[Rank and trace detection in characteristic zero]\label{cor:rank_trace_detection}
1092 Assume that \(E'\) has characteristic zero. For every maximal Hecke packet,
1093 \[
1094 \boxed{
1095 \Tr_{E'}(e_{\frakm}|V)
1096 =
1097 \rank_{E'}(e_{\frakm}|V)
1098 =
1099 \dim_{E'}e_{\frakm}V.
1100 }
1101 \]
1102 In particular, the packet is occupied exactly when its projector has positive rank, equivalently nonzero trace.
1103 \end{corollary}
1104 
1105 \begin{proof}
1106 An idempotent linear map has minimal polynomial dividing \(X(X-1)\), which has distinct roots. It is diagonalizable with eigenvalues zero and one. Its trace and rank both equal the multiplicity of the eigenvalue one. A positive integer is nonzero in characteristic zero.
1107 \end{proof}
1108 
1109 \begin{remark}
1110 The trace criterion can fail in positive characteristic when the packet dimension is divisible by the characteristic. The rank and localization criteria remain valid.
1111 \end{remark}
1112 
1113 \begin{figure}[t]
1114 \centering
1115 \includegraphics[width=.92\textwidth]{09_hecke_artin_packets.pdf}
1116 \caption{A finite commutative Hecke algebra splits into canonical Artin local packets.}
1117 \label{fig:hecke_artin_packets}
1118 \end{figure}
1119 
1120 \begin{figure}[t]
1121 \centering
1122 \includegraphics[width=.9\textwidth]{10_generalized_eigenspaces.pdf}
1123 \caption{An Artin packet is a simultaneous generalized eigenspace, not necessarily an ordinary eigenspace.}
1124 \label{fig:generalized_eigenspaces}
1125 \end{figure}
1126 
1127 \begin{example}[A nonsemisimple Hecke packet]\label{ex:nonsemisimple_hecke_packet}
1128 Let
1129 \[
1130 \TT
1131 =
1132 E'[u]/(u^2)
1133 \times
1134 E'[v]/(v^3)
1135 \]
1136 and let \(V=\TT\) be the regular module. The two canonical central idempotents split
1137 \[
1138 V=V_u\oplus V_v
1139 \]
1140 with dimensions two and three. Multiplication by \(u\) is nilpotent on \(V_u\), and multiplication by \(v\) is nilpotent on \(V_v\). Neither local factor is semisimple, but the two maximal Hecke packets are isolated exactly by the Artin idempotents.
1141 \end{example}
1142 
1143 \begin{proof}
1144 The product decomposition gives the two central idempotents \((1,0)\) and \((0,1)\). Their ranges are the two local factors. The classes of \(u\) and \(v\) are nilpotent of orders two and three, respectively.
1145 \end{proof}
1146 
1147 The next two theorems distinguish a fixed finite carrier from a sequence of changing carriers.
1148 
1149 \begin{theorem}[Nested packets in one finite carrier]\label{thm:nested_finite_carrier}
1150 Let \(V\) be a finite dimensional vector space. Let \(e_1,e_2,\ldots\) be idempotents such that
1151 \[
1152 e_{m+1}e_m=e_me_{m+1}=e_{m+1}
1153 \]
1154 for every \(m\). If \(e_mV\neq0\) for every \(m\), then the descending chain stabilizes and
1155 \[
1156 \boxed{
1157 \bigcap_{m\geq1}e_mV
1158 \neq0.
1159 }
1160 \]
1161 \end{theorem}
1162 
1163 \begin{proof}
1164 The displayed relations give
1165 \[
1166 e_{m+1}V\subseteq e_mV.
1167 \]
1168 The nonnegative dimensions form a nonincreasing sequence of positive integers, so they eventually become constant. Once two consecutive dimensions agree, the corresponding inclusion is equality. Thus the ranges stabilize at a nonzero subspace, which is their intersection.
1169 \end{proof}
1170 
1171 \begin{corollary}[Finite witness of incompatibility]\label{cor:finite_witness_incompatibility}
1172 Under the hypotheses of \cref{thm:nested_finite_carrier}, if
1173 \[
1174 \bigcap_{m\geq1}e_mV=0,
1175 \]
1176 then \(e_mV=0\) for some finite \(m\).
1177 \end{corollary}
1178 
1179 \begin{proof}
1180 This is the contrapositive of \cref{thm:nested_finite_carrier}.
1181 \end{proof}
1182 
1183 \begin{figure}[t]
1184 \centering
1185 \includegraphics[width=.9\textwidth]{11_finite_occupancy_staircase.pdf}
1186 \caption{Nested nonzero packets in one finite carrier stabilize after finitely many steps.}
1187 \label{fig:finite_occupancy_staircase}
1188 \end{figure}
1189 
1190 \begin{definition}[Stable core]\label{def:stable_core}
1191 Let
1192 \[
1193 V_1\longleftarrow V_2\longleftarrow V_3\longleftarrow\cdots
1194 \]
1195 be an inverse system of finite dimensional vector spaces. For \(n\geq m\), write
1196 \(f_{n,m}:V_n\to V_m\). The stable core at level \(m\) is
1197 \[
1198 Y_m
1199 =
1200 \bigcap_{n\geq m}\im(f_{n,m}).
1201 \]
1202 \end{definition}
1203 
1204 \begin{lemma}[Surjectivity on stable cores]\label{lem:stable_core_surjectivity}
1205 For every \(m\), the transition map \(V_{m+1}\to V_m\) induces a surjection
1206 \[
1207 \boxed{
1208 Y_{m+1}\twoheadrightarrow Y_m.
1209 }
1210 \]
1211 \end{lemma}
1212 
1213 \begin{proof}
1214 Fix \(y\in Y_m\). For \(n\geq m+1\), let
1215 \[
1216 A_n
1217 =
1218 \left\{
1219 z\in\im(f_{n,m+1}):
1220 f_{m+1,m}(z)=y
1221 \right\}.
1222 \]
1223 Each \(A_n\) is a nonempty affine subspace of \(V_{m+1}\), and the sequence
1224 \((A_n)\) is descending. A descending sequence of affine subspaces in a finite dimensional vector space stabilizes whenever every term is nonempty. Choose an element in its stable value. It lies in \(Y_{m+1}\) and maps to \(y\).
1225 \end{proof}
1226 
1227 \begin{theorem}[Nonzero stable core criterion]\label{thm:nonzero_stable_core}
1228 Let \((V_m)\) be an inverse system of finite dimensional vector spaces. If
1229 \[
1230 Y_m\neq0
1231 \]
1232 for every \(m\), then
1233 \[
1234 \boxed{
1235 \varprojlim_mV_m
1236 \neq0.
1237 }
1238 \]
1239 More precisely, the inverse limit contains a compatible sequence whose first coordinate is any prescribed nonzero element of \(Y_1\).
1240 \end{theorem}
1241 
1242 \begin{proof}
1243 Choose \(0\neq y_1\in Y_1\). By \cref{lem:stable_core_surjectivity}, choose recursively
1244 \(y_{m+1}\in Y_{m+1}\) mapping to \(y_m\). Every \(y_m\) is nonzero because it maps to the nonzero vector \(y_1\). The sequence \((y_m)\) is a nonzero element of the inverse limit.
1245 \end{proof}
1246 
1247 \begin{corollary}[Surjective systems]\label{cor:surjective_inverse_system}
1248 If every transition map \(V_{m+1}\to V_m\) is surjective and every \(V_m\) is nonzero, then the inverse limit is nonzero.
1249 \end{corollary}
1250 
1251 \begin{proof}
1252 Surjectivity gives \(Y_m=V_m\). Apply \cref{thm:nonzero_stable_core}.
1253 \end{proof}
1254 
1255 \begin{example}[Tail escape in an infinite carrier]\label{ex:tail_escape}
1256 Let \(V=\ell^2(\NN)\), and let \(P_m\) be the orthogonal projection onto the closed span of
1257 \[
1258 e_m,e_{m+1},e_{m+2},\ldots.
1259 \]
1260 Every range \(P_mV\) is nonzero and the ranges are nested, but
1261 \[
1262 \boxed{
1263 \bigcap_{m\geq1}P_mV=0.
1264 }
1265 \]
1266 Thus the finite carrier hypothesis in \cref{thm:nested_finite_carrier} cannot be removed.
1267 \end{example}
1268 
1269 \begin{proof}
1270 A vector in every tail range has its first \(m-1\) coordinates equal to zero for every \(m\). All of its coordinates vanish.
1271 \end{proof}
1272 
1273 \begin{figure}[t]
1274 \centering
1275 \includegraphics[width=.9\textwidth]{12_stable_core_inverse_limit.pdf}
1276 \caption{Changing finite carriers require a nonzero stable core, not only nonzero individual levels.}
1277 \label{fig:stable_core_inverse_limit}
1278 \end{figure}
1279 
1280 \begin{figure}[t]
1281 \centering
1282 \includegraphics[width=.88\textwidth]{13_tail_escape.pdf}
1283 \caption{Nested nonzero ranges can escape to infinity in an infinite dimensional carrier.}
1284 \label{fig:tail_escape}
1285 \end{figure}
1286 
1287 \section{Pointwise automorphy from support}\label{sec:pointwise}
1288 
1289 Support produces a nonzero Hecke fiber. A realization theorem is still required to turn that fiber into a classical automorphic representation and to identify its Galois representation.
1290 
1291 \begin{definition}[Automorphic Hecke datum]\label{def:automorphic_hecke_datum}
1292 An automorphic Hecke datum consists of the following objects.
1293 \begin{enumerate}
1294 \item A commutative \(\OO\) algebra \(\TT\).
1295 \item A finite \(\TT\) module \(H\), or a perfect \(\TT\) complex \(C\), obtained from an automorphic or cohomological carrier.
1296 \item For every unramified place \(v\) outside a finite set, a polynomial
1297 \[
1298 P_v(X)\in\TT[X].
1299 \]
1300 \item A declared characteristic zero locus on which a nonzero field fiber is known to be classical and is known to carry an attached Galois representation whose Frobenius polynomial at \(v\) is the specialization of \(P_v(X)\).
1301 \end{enumerate}
1302 \end{definition}
1303 
1304 \begin{standardfact}[Chebotarev and Brauer Nesbitt identification]\label{fact:chebotarev_brauer_nesbitt}
1305 Let \(E'\) be a Hausdorff topological field of characteristic zero, with continuous ring operations. Let
1306 \[
1307 \rho_1,\rho_2:G_{F,S}\longrightarrow\GL_n(E')
1308 \]
1309 be continuous semisimple representations. If their characteristic polynomials agree at every Frobenius element outside a density zero exceptional set, then
1310 \[
1311 \boxed{\rho_1\cong\rho_2.}
1312 \]
1313 This follows from Chebotarev density and the Brauer Nesbitt theorem
1314 \cite{BrauerNesbitt1941,Neukirch1999,Gee2022}.
1315 \end{standardfact}
1316 
1317 \begin{theorem}[Support gives a Hecke eigensystem]\label{thm:support_gives_hecke_system}
1318 Let \(R\cong\TT\), let \(H\) be a finite \(\TT\) module, and let
1319 \(x:R\to E'\) be a field valued point. If
1320 \[
1321 \ker x\in\Supp_R(H),
1322 \]
1323 then
1324 \[
1325 \boxed{
1326 H_x:=H\otimes_{\TT,x}E'\neq0.
1327 }
1328 \]
1329 Every element of \(\TT\) acts on \(H_x\) through the scalar prescribed by \(x\).
1330 \end{theorem}
1331 
1332 \begin{proof}
1333 Nonvanishing follows from \cref{cor:supported_hecke_fiber}. The tensor product relation
1334 \[
1335 th\otimes1=h\otimes x(t)
1336 \]
1337 shows that \(t\in\TT\) acts through \(x(t)\).
1338 \end{proof}
1339 
1340 \begin{theorem}[Pointwise Galois realization]\label{thm:pointwise_galois_realization}
1341 Let \(E'\) be a Hausdorff topological field of characteristic zero, with continuous ring operations. Require both \(\rho_x=x\circ\rho_R\) and the attached representation below to be continuous. Assume the following data.
1342 \begin{enumerate}
1343 \item A represented deformation ring \(R\) with universal representation
1344 \[
1345 \rho_R:G_{F,S}\longrightarrow\GL_n(R).
1346 \]
1347 \item An isomorphism \(R\cong\TT\).
1348 \item An automorphic Hecke datum \((\TT,H,(P_v))\).
1349 \item A characteristic zero point \(x:R\to E'\) lying in \(\Supp_R(H)\).
1350 \item A classical automorphic representation \(\pi_x\) occurring in the fiber \(H_x\), together with a semisimple attached representation
1351 \[
1352 \rho_{\pi_x}:G_{F,S}\longrightarrow\GL_n(E')
1353 \]
1354 whose unramified characteristic polynomial is \(x(P_v(X))\).
1355 \item Equality
1356 \[
1357 \det\left(X-\rho_x(\Frob_v)\right)=x(P_v(X))
1358 \]
1359 for \(\rho_x=x\circ\rho_R\) at every unramified place in a Chebotarev dense set.
1360 \end{enumerate}
1361 Then
1362 \[
1363 \boxed{
1364 \rho_x^{\mathrm{ss}}
1365 \cong
1366 \rho_{\pi_x}.
1367 }
1368 \]
1369 If \(\rho_x\) is irreducible, then \(\rho_x\cong\rho_{\pi_x}\).
1370 \end{theorem}
1371 
1372 \begin{proof}
1373 The coefficients of the characteristic polynomials of \(\rho_x\) and \(\rho_{\pi_x}\) are continuous and constant on conjugacy classes. Their equality on the declared dense union of Frobenius conjugacy classes therefore extends to every element of \(G_{F,S}\), by Hausdorffness. A semisimplification has the same characteristic polynomials as the original representation. The algebraic Brauer Nesbitt input in \cref{fact:chebotarev_brauer_nesbitt} thus gives \(\rho_x^{\mathrm{ss}}\cong\rho_{\pi_x}\). If \(\rho_x\) is irreducible, it is already semisimple.
1374 \end{proof}
1375 
1376 \begin{corollary}[Full support gives pointwise automorphy on the realized locus]\label{cor:full_support_pointwise_automorphy}
1377 In the setting of \cref{thm:pointwise_galois_realization}, suppose
1378 \[
1379 \Supp_R(H)=\Spec R.
1380 \]
1381 For every characteristic zero point \(x:R\to E'\) with \(\ker x\in U\subseteq\Spec R\), assume the coefficient topology and continuity hypotheses of \cref{thm:pointwise_galois_realization} and the declared classicality and Galois realization input. Then every such point is automorphic in the precise sense of \cref{thm:pointwise_galois_realization}.
1382 \end{corollary}
1383 
1384 \begin{proof}
1385 Every point of \(U\) lies in the support, so \cref{thm:support_gives_hecke_system} gives a nonzero Hecke fiber. Apply the declared realization input and then \cref{thm:pointwise_galois_realization}.
1386 \end{proof}
1387 
1388 \begin{theorem}[Derived pointwise realization]\label{thm:derived_pointwise_realization}
1389 Let \(e:R\cong\TT\), and let \(C\) be a perfect automorphic Hecke complex with full derived support. Choose a bounded finite projective model for \(C\), supported in degrees \([a,b]\). For every characteristic zero point \(x:R\to E'\), write \(y=x\circ e^{-1}\). Then some integer \(i\in[a,b]\) has
1390 \[
1391 H^i\left(C\mathbin{\mathop{\otimes}\limits_{\TT,y}^{\mathbf L}}E'\right)\neq0.
1392 \]
1393 Every \(t\in\TT\) acts on this cohomology through \(y(t)\).
1394 
1395 For the realization conclusion, give \(E'\) a Hausdorff topological field structure. Supply a universal representation \(\rho_R\), a continuous specialization \(\rho_x=x\circ\rho_R\), and a semisimplification of \(\rho_x\). Suppose its characteristic polynomials on a Chebotarev dense set are \(y(P_v(X))\). Let the declared classicality range contain \([a,b]\). Assume that every nonzero Hecke eigensystem in that range is realized by a classical automorphic representation occurring in that degree, with a continuous semisimple attached representation whose characteristic polynomials on the same dense set are \(y(P_v(X))\). With the standard Chebotarev density and Brauer Nesbitt inputs of \cref{fact:chebotarev_brauer_nesbitt}, the specialization \(\rho_x\) is automorphic after semisimplification. If \(\rho_x\) is irreducible, it is itself isomorphic to the attached representation.
1396 \end{theorem}
1397 
1398 \begin{proof}
1399 Full derived support gives a nonzero fiber at \(y\). Scalar extension of the chosen projective model preserves its degree bounds. Its cohomology therefore vanishes below \(a\) and above \(b\). Since vanishing in every degree is equivalent to being zero in the derived category, some degree \(i\in[a,b]\) has nonzero cohomology. Choose a nonzero vector in that cohomology module.
1400 
1401 Multiplication by \(t\in\TT\) is a cochain endomorphism of the original model. In the scalar extension the tensor relation identifies this endomorphism with \(y(t)\) times the identity. Passing to the derived category and then to cohomology preserves this equality. Thus the chosen vector is a common Hecke eigenvector with character \(y\).
1402 
1403 The interval inclusion puts this eigensystem in the declared classicality range. Apply the realization input to obtain an occurring automorphic representation and its continuous semisimple attached representation. Its Frobenius characteristic polynomials agree with those of \(\rho_x\) on the prescribed dense set. Continuity extends the equality to every group element. The supplied semisimplification preserves these polynomials, so the general Brauer Nesbitt input gives an invertible linear intertwiner. If \(\rho_x\) is irreducible, it is already semisimple and the same comparison applies directly.
1404 \end{proof}
1405 
1406 \begin{remark}
1407 Derived support does not identify the cohomological degree, Hodge type, or classical weight of the surviving eigensystem. Those properties must come from the external local and global realization theorem.
1408 \end{remark}
1409 
1410 \begin{figure}[t]
1411 \centering
1412 \includegraphics[width=.94\textwidth]{16_pointwise_automorphy.pdf}
1413 \caption{Support gives a nonzero Hecke fiber. Classicality and Galois realization complete the pointwise argument.}
1414 \label{fig:pointwise_automorphy}
1415 \end{figure}
1416 
1417 \section{Compatible systems and companion completion}\label{sec:compatible}
1418 
1419 Pointwise automorphy at one coefficient place and existence of companions at other coefficient places are different statements. They meet only after a common algebraic Frobenius spine has been fixed.
1420 
1421 \begin{definition}[Algebraic Frobenius spine]\label{def:frobenius_spine}
1422 An algebraic Frobenius spine consists of a number field \(L\), a finite set of places \(S\) of \(F\), and polynomials
1423 \[
1424 P_v(X)\in L[X]
1425 \]
1426 for every finite place \(v\notin S\), together with any additional local labels required by the declared compatibility problem.
1427 \end{definition}
1428 
1429 \begin{definition}[Finite companion forest]\label{def:companion_forest}
1430 Fix a coefficient place \(\lambda\) of \(L\). A finite companion forest for the spine is an inverse system of finite sets
1431 \[
1432 X_{\lambda,1}
1433 \longleftarrow
1434 X_{\lambda,2}
1435 \longleftarrow
1436 X_{\lambda,3}
1437 \longleftarrow\cdots
1438 \]
1439 whose points are admissible realizations modulo \(\lambda^m\), with edges given by reduction. A complete realization is admissible for this forest when all its finite reductions belong to the displayed levels; the empty level obstruction below concerns this declared admissibility problem.
1440 \end{definition}
1441 
1442 \begin{theorem}[Companion branch criterion]\label{thm:companion_branch_criterion}
1443 Suppose every level \(X_{\lambda,m}\) is finite and nonempty, and every point reduces along the displayed forest to the fixed residual root. Then
1444 \[
1445 \boxed{
1446 \varprojlim_mX_{\lambda,m}
1447 \neq\varnothing.
1448 }
1449 \]
1450 \end{theorem}
1451 
1452 \begin{proof}
1453 The disjoint union of the levels is an infinite rooted tree. It is locally finite because every level is finite. It contains a vertex at every depth. König's infinity lemma gives an infinite branch \cite{Diestel2017}. That branch is a point of the inverse limit.
1454 \end{proof}
1455 
1456 \begin{corollary}[Empty finite companion obstruction]\label{cor:empty_companion_obstruction}
1457 If \(X_{\lambda,m}=\varnothing\) for some \(m\), then no complete \(\lambda\) adic realization admissible for this forest exists.
1458 \end{corollary}
1459 
1460 \begin{proof}
1461 A complete realization would reduce to a point at every finite level.
1462 \end{proof}
1463 
1464 Finite forests alone give compatible classes. To obtain actual continuous representations, we use the following explicit coefficient and admissibility data. They also delimit the meaning of completion in the next theorem.
1465 
1466 Fix a topological group \(\Gamma\), a finite matrix index set \(D\), and a set \(\Lambda\) of coefficient indices. For each \(\lambda\), let \(\OO_\lambda\) be a commutative ring, complete and separated for a finitely generated ideal \(I_\lambda\), with finite residue ring \(\OO_\lambda/I_\lambda\). Give \(\OO_\lambda\) its ideal adic topology and every quotient its discrete topology. Let
1467 \[
1468 i_\lambda:\OO_\lambda\longrightarrow K_\lambda,
1469 \qquad e_\lambda:L\longrightarrow K_\lambda
1470 \]
1471 be supplied ring homomorphisms, where \(L\) and \(K_\lambda\) are fields, \(K_\lambda\) has a declared topology, and \(i_\lambda\) is continuous.
1472 
1473 For every positive integer \(n\), let \(X_{\lambda,n}\) be a finite nonempty set of conjugacy classes of actual continuous representations
1474 \[
1475 \Gamma\longrightarrow\GL_D(\OO_\lambda/I_\lambda^n).
1476 \]
1477 Conjugacy means change of basis by an invertible matrix over that quotient. Assume reduction preserves these sets and that \(X_{\lambda,1}\) consists of the declared residual class. Each admissible class must have a continuous representative. The auxiliary level zero is the unique class over the trivial quotient and imposes no extra occupancy hypothesis.
1478 
1479 Choose elements \(\gamma_v\in\Gamma\) on a sample set \(\Omega\), with declared good subsets \(\Omega_\lambda\subseteq\Omega\). In the arithmetic application these are the chosen Frobenius elements at the permitted places. For each \(v\in\Omega_\lambda\), supply an integral polynomial \(P_{\lambda,v}\in\OO_\lambda[X]\) such that
1480 \[
1481 i_\lambda(P_{\lambda,v})=e_\lambda(P_v)\quad\text{in }K_\lambda[X].
1482 \]
1483 Here and below a ring homomorphism applied to a polynomial acts on its coefficients. Assume every representative of every class in \(X_{\lambda,n}\) has characteristic polynomial \(P_{\lambda,v}\bmod I_\lambda^n\) at \(\gamma_v\). Also supply a subgroup \(H_\lambda\leq\Gamma\) on which all these finite representations are trivial. This is an inertia condition when \(H_\lambda\) is the specified inertia subgroup.
1484 
1485 Finally, put
1486 \[
1487 B_\lambda=\OO_\lambda[x_{g,a,b}:g\in\Gamma,\ a,b\in D].
1488 \]
1489 For each declared local condition index \(u\), supply an ideal \(J_{\lambda,u}\subseteq B_\lambda\). Evaluation at a representation sends \(x_{g,a,b}\) to its \((a,b)\) matrix entry at \(g\). Assume that evaluation at every admissible finite representative kills \(J_{\lambda,u}\), with polynomial coefficients reduced modulo \(I_\lambda^n\). For this class based theorem, the equations must hold in every admissible frame. A condition imposed only in one chosen frame needs a separate compatible frame argument. No arbitrary arithmetic condition is identified with such an ideal without a separate argument.
1490 
1491 \begin{theorem}[Conditional simultaneous companion completion]\label{thm:simultaneous_companion_completion}
1492 Under the coefficient and finite admissibility hypotheses above, one can choose continuous representations
1493 \[
1494 \rho_\lambda:\Gamma\longrightarrow\GL_D(\OO_\lambda)
1495 \qquad(\lambda\in\Lambda)
1496 \]
1497 whose reduction class belongs to \(X_{\lambda,n}\) for every positive \(n\). They retain the declared residual class. After applying \(i_\lambda\), they are continuous, trivial on \(H_\lambda\), and satisfy
1498 \[
1499 \det\!\left(X- i_\lambda(\rho_\lambda(\gamma_v))\right)
1500 =e_\lambda(P_v),\qquad v\in\Omega_\lambda.
1501 \]
1502 Their integral evaluation points factor through every actual quotient \(B_\lambda/J_{\lambda,u}\).
1503 \end{theorem}
1504 
1505 \begin{proof}
1506 The finitely generated ideal and finite residue ring give finite coefficient quotients at every precision. An individual conjugacy class has finitely many frames because the group of invertible basis matrices over each quotient is finite. Thus the finitely many admissible classes give a finite nonempty set of actual continuous representations at each positive level. Continuity is invariant under conjugation. Reduction gives total maps between these sets. Compactness, as in \cref{thm:companion_branch_criterion}, selects strictly compatible representatives. This step neither assumes transition surjectivity nor lifts a prescribed conjugating matrix.
1507 
1508 Completeness and separatedness identify \(\GL_D(\OO_\lambda)\) with the compatible inverse limit of the quotient matrix groups. Lift entries and inverse entries to construct this identification. The two reduction and reconstruction identities hold entrywise. Finite quotient continuity implies continuity for the ideal adic topology, including the matrix inverse, so the reconstructed representation is continuous.
1509 
1510 Each coefficient of its characteristic polynomial agrees with the prescribed integral coefficient modulo every positive power of \(I_\lambda\). Separatedness gives equality of the full polynomials. The same argument applied to the matrix entries of \(\rho_\lambda(g)-1\) gives triviality on \(H_\lambda\). Continuous coefficient change and the matching equations for \(P_{\lambda,v}\) give the asserted common spine over the local fields.
1511 
1512 For \(p\in J_{\lambda,u}\), evaluation commutes with reduction. Its value is zero modulo every positive power of \(I_\lambda\), hence is zero integrally by separatedness. Therefore the evaluation homomorphism kills the whole ideal and factors uniquely through \(B_\lambda/J_{\lambda,u}\). Choose a realization for each \(\lambda\).
1513 \end{proof}
1514 
1515 The quotient conclusion is a proved effectivity statement for the declared polynomial relations. For local conditions presented by continuous maps from represented local rings, \cref{cor:simultaneous_local} also accounts for the closed ideal generated by their defining ideals. Neither statement constructs a deformation ring for a condition that has not been shown representable. Hodge conditions, Weil--Deligne conditions, integral lifts of arbitrary Frobenius polynomials, and the finite occupancy hypotheses still require their own arithmetic inputs. The theorem retains a residual conjugacy class, not a prescribed residual matrix frame, and asserts no uniqueness up to integral conjugacy.
1516 
1517 \begin{standardfact}[Strict compatibility and one member determination]\label{fact:strict_compatibility}
1518 A strictly compatible semisimple system is determined at every coefficient place by its common unramified characteristic polynomials. If an automorphic representation gives a compatible system with the same polynomials, then Chebotarev density and Brauer Nesbitt identify the two systems member by member after semisimplification
1519 \cite{Serre1977,BarnetLambGeeGeraghtyTaylor2014}.
1520 \end{standardfact}
1521 
1522 \begin{theorem}[One member propagation in a fixed system]\label{thm:one_member_propagation}
1523 Let
1524 \[
1525 \{\rho_\lambda\}_{\lambda\in\Lambda}
1526 \]
1527 be a semisimple strictly compatible system with Frobenius spine \((P_v)\). Suppose that for one coefficient place \(\lambda_0\), the representation \(\rho_{\lambda_0}\) is identified with the Galois representation attached to an automorphic representation \(\pi\). Assume that the compatible system attached to \(\pi\) has the same polynomials \(P_v(X)\). Then for every \(\lambda\in\Lambda\),
1528 \[
1529 \boxed{
1530 \rho_\lambda
1531 \cong
1532 \rho_{\pi,\lambda}^{\mathrm{ss}}.
1533 }
1534 \]
1535 \end{theorem}
1536 
1537 \begin{proof}
1538 For every \(\lambda\), the two semisimple representations have the same unramified characteristic polynomials at all places outside one finite set. Apply \cref{fact:chebotarev_brauer_nesbitt}.
1539 \end{proof}
1540 
1541 \begin{remark}
1542 The theorem propagates automorphy inside a compatible system that already exists. It does not construct a missing coefficient place member and does not prove universal companion existence.
1543 \end{remark}
1544 
1545 \begin{proposition}[Finite Frobenius separator]\label{prop:finite_frobenius_separator}
1546 Let \(t_1,\ldots,t_r\) be linearly independent functions on a set \(\Omega\) with values in a field \(E'\). Then there are points
1547 \(\omega_1,\ldots,\omega_r\in\Omega\) such that the matrix
1548 \[
1549 \left(t_i(\omega_j)\right)_{j,i}
1550 \]
1551 is invertible. In particular, when the trace functions of finitely many compatible constituents are linearly independent on the unramified Frobenius set, finitely many Frobenius traces recover their multiplicities in any known semisimple carrier.
1552 \end{proposition}
1553 
1554 \begin{proof}
1555 Let
1556 \[
1557 W
1558 =
1559 \operatorname{span}
1560 \left\{
1561 (t_1(\omega),\ldots,t_r(\omega)):\omega\in\Omega
1562 \right\}
1563 \subseteq E'^r.
1564 \]
1565 If \(W\neq E'^r\), a nonzero linear functional on \(E'^r\) would vanish on every evaluation vector, giving a nontrivial linear relation among the functions. Thus \(W=E'^r\). Choose \(r\) evaluation vectors forming a basis.
1566 \end{proof}
1567 
1568 \begin{figure}[t]
1569 \centering
1570 \includegraphics[width=.94\textwidth]{14_companion_spine.pdf}
1571 \caption{Under the coefficient and effectivity hypotheses of \cref{thm:simultaneous_companion_completion}, local companion branches realize the Frobenius spine fixed in advance.}
1572 \label{fig:companion_spine}
1573 \end{figure}
1574 
1575 \section{The coefficient prime two}\label{sec:two}
1576 
1577 The auxiliary augmentation algebra works at every coefficient prime. What changes at two is the availability of integral character projectors and, in many applications, the residual image and local deformation hypotheses.
1578 
1579 \begin{proposition}[Failure of integral sign projectors]\label{prop:dyadic_sign_projectors}
1580 Let \(C_2=\langle g\rangle\). Over \(\QQ_2\), the two sign projectors are
1581 \[
1582 \boxed{
1583 e_+=\frac{1+g}{2},
1584 \qquad
1585 e_-=\frac{1-g}{2}.
1586 }
1587 \]
1588 Neither belongs to \(\ZZ_2[C_2]\). After reduction modulo two,
1589 \[
1590 \boxed{
1591 \FF_2[C_2]
1592 \cong
1593 \FF_2[X]/(X^2),
1594 \qquad
1595 X=g-1.
1596 }
1597 \]
1598 This ring is local and has no nontrivial idempotents.
1599 \end{proposition}
1600 
1601 \begin{proof}
1602 The displayed rational elements are the unique primitive idempotents because they project to the two characters of \(C_2\). Their coefficients contain \(1/2\), so they are not integral. In characteristic two,
1603 \[
1604 (g-1)^2=g^2-2g+1=0.
1605 \]
1606 The map \(X\mapsto g-1\) gives the displayed isomorphism. The quotient by \((X)\) is \(\FF_2\), and \((X)\) is nilpotent. Thus the ring is local.
1607 \end{proof}
1608 
1609 \begin{corollary}[Dyadic coinvariant recovery]\label{cor:dyadic_coinvariant_recovery}
1610 Let \(\Delta\) be a finite two group, let \(\Lambda=\OO[\Delta]\) with \(\OO\) a finite extension of \(\ZZ_2\), and let \(M\) be finite free over \(\Lambda\). Then
1611 \[
1612 \boxed{
1613 M\otimes_{\Lambda,\epsilon}\OO
1614 \cong
1615 M/\fraka M
1616 }
1617 \]
1618 is free over \(\OO\) of the same \(\Lambda\) rank. No semisimple character decomposition is required.
1619 \end{corollary}
1620 
1621 \begin{proof}
1622 Use the right module convention fixed in \cref{sec:auxiliary}. Quotienting by all balancing relations identifies \(M\otimes_{\Lambda,\epsilon}\OO\) with \(M/\fraka M\), without any commutativity assumption on \(\Delta\). Applying \(\epsilon\) to the coordinates of a finite \(\Lambda\) basis gives an \(\OO\) basis with the same index set.
1623 \end{proof}
1624 
1625 \begin{remark}
1626 The corollary is an algebraic statement about augmentation and coinvariants. It does not supply a coefficient two adequacy theorem, a local deformation ring with the desired geometry, or a classicality theorem. Those inputs must be checked in the automorphy lifting theorem being used.
1627 \end{remark}
1628 
1629 \begin{figure}[t]
1630 \centering
1631 \includegraphics[width=.92\textwidth]{15_coefficient_two_boundary.pdf}
1632 \caption{Augmentation survives at two, while semisimple character projectors and arithmetic hypotheses require separate treatment.}
1633 \label{fig:coefficient_two_boundary}
1634 \end{figure}
1635 
1636 \section{Conditional automorphic completion}\label{sec:completion}
1637 
1638 The following theorem assembles the preceding statements as a chain of gates. Each gate has a distinct mathematical source.
1639 
1640 \begin{definition}[Ordinary completion datum at a point]\label{def:ordinary_completion_datum}
1641 An ordinary completion datum at a characteristic zero point \(x:R\to E'\) consists of the following objects.
1642 \begin{enumerate}
1643 \item A represented global deformation ring \(R\) with declared local quotient conditions and universal representation \(\rho_R\).
1644 \item An ordinary patching datum
1645 \[
1646 (R_\infty,\fraka,M_\infty,R,H)
1647 \]
1648 whose finite level module \(H\) is an automorphic Hecke carrier.
1649 \item Full patched support
1650 \[
1651 \Supp_{R_\infty}(M_\infty)=\Spec R_\infty.
1652 \]
1653 \item An isomorphism
1654 \[
1655 R\cong\TT
1656 \]
1657 with the Hecke algebra acting on \(H\). The \(R\) action on \(H\) supplied by the patched control isomorphism is the restriction of this \(\TT\) action along the displayed isomorphism.
1658 \item An automorphic Hecke datum \((\TT,H,(P_v))\) and a pointwise classicality and Galois realization theorem satisfying all the inputs of \cref{thm:pointwise_galois_realization} for the nonzero fiber at \(x\): an occurring classical automorphic representation with a continuous semisimple attached representation; equality of the characteristic polynomials of both that representation and \(\rho_x=x\circ\rho_R\) with \(x(P_v(X))\) on the same declared Chebotarev dense union of Frobenius conjugacy classes; and the standard semisimplification, density, and general Brauer Nesbitt inputs. The coefficient topology and continuity requirements are retained in \cref{thm:ordinary_conditional_completion}.
1659 \end{enumerate}
1660 \end{definition}
1661 
1662 \begin{theorem}[Ordinary conditional automorphic completion]\label{thm:ordinary_conditional_completion}
1663 Let \(x:R\to E'\) admit an ordinary completion datum. Assume \(E'\) is a Hausdorff topological field of characteristic zero with continuous ring operations, and that both \(\rho_x=x\circ\rho_R\) and its attached comparison representation are continuous. Then
1664 \[
1665 \boxed{
1666 H\otimes_{\TT,x}E'\neq0.
1667 }
1668 \]
1669 The specialization
1670 \[
1671 \rho_x=x\circ\rho_R
1672 \]
1673 is identified after semisimplification with the Galois representation attached to a classical automorphic representation in that fiber. If \(\rho_x\) is irreducible, it is itself automorphic.
1674 \end{theorem}
1675 
1676 \begin{proof}
1677 Full patched support descends to full support of \(H\) over \(R\) by
1678 \cref{thm:ordinary_support_descent}. The isomorphism \(R\cong\TT\) transports that support by \cref{thm:rt_support_transport}. The field fiber is nonzero by
1679 \cref{thm:support_gives_hecke_system}. The declared classicality and realization theorem supplies an automorphic representation in the fiber and an attached Galois representation. The comparison with \(\rho_x\) follows from \cref{thm:pointwise_galois_realization}.
1680 \end{proof}
1681 
1682 \begin{definition}[Derived completion datum at a point]\label{def:derived_completion_datum}
1683 A derived completion datum is defined in the same way, with a perfect patched complex
1684 \(C_\infty\) of full derived support and a finite level automorphic complex
1685 \[
1686 C
1687 \simeq
1688 C_\infty
1689 \mathbin{\mathop{\otimes}\limits_{R_\infty}^{\mathbf L}}R
1690 \]
1691 in place of the ordinary modules. Under the Hecke ring isomorphism \(e:R\cong\TT\), require an actual derived carrier identification between the scalar transport of this finite level complex and the automorphic Hecke complex. This identification retains the \(R\) action induced by patched control as the restriction of the \(\TT\) action along \(e\).
1692 \end{definition}
1693 
1694 \begin{theorem}[Derived conditional automorphic completion]\label{thm:derived_conditional_completion}
1695 Let \(x:R\to E'\) admit a derived completion datum, with Hecke identification \(e:R\cong\TT\), and put \(y=x\circ e^{-1}\). Then
1696 \[
1697 \boxed{
1698 C\mathbin{\mathop{\otimes}\limits_{\TT,y}^{\mathbf L}}E'\not\simeq0.
1699 }
1700 \]
1701 Some integer cohomological degree contains a nonzero Hecke eigensystem with character \(y\). Its degree lies between the bounds of any chosen finite projective model for \(C\).
1702 
1703 For the conditional conclusion, retain the Hausdorff coefficient topology, continuous specialization, supplied semisimplification, and common Frobenius polynomial hypotheses in \cref{thm:derived_pointwise_realization}. If the declared classicality and Galois realization theorem applies to this eigensystem and supplies an occurring classical automorphic representation with a continuous semisimple attached representation and those Frobenius polynomials, then \(\rho_x\) is automorphic after semisimplification. If \(\rho_x\) is irreducible, it is itself isomorphic to the attached representation. This pointwise applicability condition does not require a uniform classicality assertion in other degrees.
1704 \end{theorem}
1705 
1706 \begin{proof}
1707 Full support descends from the patched perfect complex by \cref{thm:derived_support_descent}. Scalar transport through \(e\), followed by the actual derived isomorphism with the automorphic Hecke complex, gives full support for \(C\). Its fiber at \(y\) is therefore nonzero. The bounded model and induced Hecke action argument in \cref{thm:derived_pointwise_realization} supplies a nonzero cohomology eigenvector in an integer degree within the model's bounds.
1708 
1709 If realization applies to this eigensystem, it supplies the occurring automorphic object and a continuous semisimple attached representation with the declared Frobenius polynomials. The representation comparison in \cref{thm:derived_pointwise_realization} then identifies the supplied semisimplification of \(\rho_x\) with that attached representation. Only applicability to this eigensystem is used. A classicality theorem for every degree in a prescribed interval is unnecessary.
1710 \end{proof}
1711 
1712 \begin{theorem}[Compatible system completion from one automorphic member]\label{thm:system_completion}
1713 Let
1714 \[
1715 \{\rho_\lambda\}_{\lambda\in\Lambda}
1716 \]
1717 be a semisimple strictly compatible system with common Frobenius spine. Suppose the member at \(\lambda_0\) admits an ordinary or derived completion datum and is identified with the Galois representation attached to an automorphic representation \(\pi\). Assume that the compatible system attached to \(\pi\) has the same Frobenius spine. Then
1718 \[
1719 \boxed{
1720 \rho_\lambda
1721 \cong
1722 \rho_{\pi,\lambda}^{\mathrm{ss}}
1723 \quad
1724 \text{for every }\lambda\in\Lambda.
1725 }
1726 \]
1727 \end{theorem}
1728 
1729 \begin{proof}
1730 The completion theorem at \(\lambda_0\) gives the automorphic representation \(\pi\). Apply \cref{thm:one_member_propagation} to the two compatible systems.
1731 \end{proof}
1732 
1733 \begin{theorem}[Five gate formulation]\label{thm:five_gate_completion}
1734 Fix a characteristic zero deformation point \(x:R\to E'\). Give \(E'\) a Hausdorff topological field structure. The conditional argument uses the following five gates.
1735 \begin{enumerate}
1736 \item \textbf{Residual gate.} Residual occupancy in the declared automorphic carrier and representability of the chosen deformation problem are supplied arithmetic inputs. In particular, the deformation ring \(R\) and its universal representation \(\rho_R\) are available.
1737 \item \textbf{Patching gate.} An applicable patching theorem supplies an ordinary finite module or a perfect complex with full patched support, together with the coefficient quotient and the module or derived control isomorphism. Write \(M\) for the resulting finite level carrier over \(R\).
1738 \item \textbf{Comparison gate.} Let \(H\) be a finite ordinary Hecke module or a perfect Hecke complex over \(\TT\). Supply a ring map \(f:R\to\TT\) satisfying
1739 \[
1740 (f^*)^{-1}\bigl(\Supp_R(M)\bigr)\subseteq\Supp_{\TT}(H).
1741 \]
1742 Use ordinary or derived support according to the carrier. Actual scalar extension satisfies this inclusion, as does transport through a ring isomorphism with the corresponding carrier identification.
1743 \item \textbf{Fiber gate.} Supply a Hecke point \(y:\TT\to E'\) with \(y\circ f=x\). Then the fiber of \(H\) at \(y\) is nonzero. It contains a nonzero Hecke eigenvector, in some integer cohomological degree in the derived case, with character \(y\).
1744 \item \textbf{Realization gate.} The declared classicality theorem applies to the resulting eigensystem and supplies an occurring classical automorphic representation \(\pi\), with a continuous semisimple attached representation. Require the specialization \(\rho_x=x\circ\rho_R\) to be continuous and supply its semisimplification. On the same Chebotarev dense set, assume that the characteristic polynomials of both \(\rho_x\) and the attached representation are \(y(P_v(X))\). Retain the standard density and general Brauer Nesbitt inputs of \cref{fact:chebotarev_brauer_nesbitt}.
1745 \end{enumerate}
1746 Then \(\rho_x^{\mathrm{ss}}\) is isomorphic to the representation attached to \(\pi\). If \(\rho_x\) is irreducible, the same conclusion holds for \(\rho_x\) itself.
1747 
1748 For propagation, suppose both a semisimple compatible family \(\{\rho_\lambda\}\) containing \(\rho_x\) and a family \(\{\rho_{\pi,\lambda}\}\) attached to this same \(\pi\) already exist. Require the distinguished members to be \(\rho_x\) and its attached representation, respectively. Assume the coefficient, continuity, density, semisimplification and common algebraic Frobenius spine hypotheses of \cref{thm:one_member_propagation}, with that spine agreeing with the specialized Hecke polynomials at the distinguished place. Then
1749 \[
1750 \rho_\lambda\cong\rho_{\pi,\lambda}^{\mathrm{ss}}
1751 \qquad\text{for every }\lambda.
1752 \]
1753 \end{theorem}
1754 
1755 \begin{proof}
1756 The residual and representability inputs specify the setting in which the supplied patching theorem applies. The formal deduction begins with its actual rings, carriers and comparison maps. In the ordinary branch, finite generation and full support at finite level follow from the coefficient quotient and module control isomorphism. In the derived branch, the derived control isomorphism gives a perfect finite level model, and \cref{thm:derived_support_descent} gives full support.
1757 
1758 The comparison inclusion transports this full support to \(H\). More specifically, \(y\circ f=x\) identifies the contraction of \(\ker y\) with \(\ker x\), so support at the source point gives support at the Hecke point. In the ordinary case, \cref{thm:field_fiber_criterion} gives a nonzero actual tensor fiber. In the derived case, the support criterion gives a nonzero actual derived fiber and hence a nonzero cohomology vector. Its integer degree lies within the bounds of the chosen finite projective model. In both cases, multiplication on the original carrier induces the scalar \(y(t)\) on the specialized vector for every \(t\in\TT\).
1759 
1760 Choose this nonzero eigensystem and apply the declared realization theorem to it. No realization statement in other degrees is needed. The two continuous representations have the same characteristic polynomials on the declared dense Frobenius conjugacy classes. Continuity extends their equality to the whole group. The supplied semisimplification preserves those polynomials, and the general Brauer Nesbitt input gives the required invertible linear intertwiner. The irreducible conclusion follows as in \cref{thm:pointwise_galois_realization}.
1761 
1762 Finally, retain the same \(\pi\) in its attached family. The distinguished member identities connect both families to the pointwise construction, while the common algebraic spine gives the required Frobenius polynomials at every coefficient place. Apply \cref{thm:one_member_propagation} to these two existing families. The construction does not produce a missing companion or an attached compatible family.
1763 \end{proof}
1764 
1765 \begin{figure}[t]
1766 \centering
1767 \includegraphics[width=.97\textwidth]{17_final_completion.pdf}
1768 \caption{The final theorem is a composition of separate residual, support, comparison, fiber, and realization gates.}
1769 \label{fig:final_completion}
1770 \end{figure}
1771 
1772 \section{Exact boundary of the chapter}\label{sec:boundary}
1773 
1774 The formal results above sharpen the logical role of patching support, Hecke packets, and compatible systems. They do not replace the arithmetic theorems that supply the gates.
1775 
1776 \begin{table}[t]
1777 \centering
1778 \caption{Proved formal statements and arithmetic inputs that remain external.}
1779 \label{tab:boundary}
1780 \begin{tabular}{p{.44\textwidth}p{.44\textwidth}}
1781 \toprule
1782 Proved in this chapter & Not proved in this chapter\\
1783 \midrule
1784 Local conditions combine through completed quotient rings & Representability of every desired local deformation condition\\
1785 Full ordinary and derived support descends through the patching quotient & Near faithfulness or full support for every global deformation problem\\
1786 An isomorphism \(R\cong\TT\) transports support and Fitting data & An \(R\cong\TT\) theorem outside published hypotheses\\
1787 Finite Hecke algebras split into Artin packets & Positive automorphic occupancy of every residual or characteristic zero packet\\
1788 Nonzero stable cores produce compatible inverse limit points & Universal residual companion existence\\
1789 One automorphic member determines a fixed compatible system & Existence of a compatible system for every geometric representation\\
1790 Augmentation and coinvariant recovery work at coefficient prime two & A universal coefficient two replacement for residual image, local geometry, and classicality hypotheses\\
1791 \bottomrule
1792 \end{tabular}
1793 \end{table}
1794 
1795 \begin{remark}
1796 The strongest global conclusion is conditional automorphic realization inside a declared class for which the five gates have been verified. The chapter does not prove unrestricted global Langlands reciprocity.
1797 \end{remark}
1798 
1799 \begin{remark}
1800 A numerical certificate can check the finite algebra appearing in an example. It cannot verify a published automorphy lifting theorem, a classicality theorem, or a universal existence statement.
1801 \end{remark}
1802 
1803 \section*{Lean verification and revision scope}
1804 
1805 The preserved Lean release 0.17.0, reverified in evidence release 0.17.1, reports 748 named theorem declarations written for Paper XII, including supporting lemmas and interface results. A further 81 theorem declarations are reused unchanged from Paper X and counted separately. The cumulative verification rebuilds all 96 registered project modules with Lean 4.34.0-rc2 and warnings treated as errors. The transitive axiom audit covers 1,229 named declarations and permits only \texttt{propext}, \texttt{Classical.choice}, and \texttt{Quot.sound}. Three deliberately invalid controls test rejection of a false proof, a placeholder, and an incorrect empty family normalization. The pinned Mathlib dependency cache is not itself rebuilt. Exact compiler results, source hashes, and the verification scope are recorded with the archive.
1806 
1807 The preserved release records complete mapped Lean statements for all 49 internal numbered claims of its revised manuscript. The present traditional edition retains those proof bodies, exposes the hypotheses on the local map and coefficient target in \cref{prop:global_local_basechange}, makes the \(r>n\) convention explicit in the proof of \cref{thm:higher_fitting_strata}, states all the pointwise comparison inputs in \cref{def:ordinary_completion_datum}, and declares a finite ramification set and coherent geometric Frobenius normalization. These editorial clarifications are recorded separately from the inherited eight amendments. They are not counted as newly compiled Lean certificates. No new statement amendment was needed for the completion and tensor results. The eight inherited amendments remain explicitly separate from the original wording, and the cited arithmetic inputs remain outside the internal claim census. Formal proof coverage is recorded claim by claim in the roadmap. These checks certify the formal statements under their explicit hypotheses, not every prose claim, novelty assertion, or external arithmetic result.
1808 
1809 The completion block proves \cref{thm:tensor_quotient,prop:global_local_basechange} using actual algebraic tensor products, actual Hausdorff completions, and the actual closed generated ideals. Both inverse laws, continuity in both directions, and the canonical factor maps are checked. An independent comparison with the algebraic inverse limit completion identifies the topology and local ring structure. The global theorem retains continuous local algebra points and their naturality, rather than only an unstructured point existence statement. The empty family retains the scalar adic topology. The zero condition and unit ideal boundaries are checked separately.
1810 
1811 The preceding Fitting block proves \cref{thm:fitting_support,thm:higher_fitting_strata,prop:fitting_base_change,thm:rt_support_transport}. Its intrinsic Fitting ideals are independent of the chosen finite presentation, including the number of generators and relations. Arbitrary base change, all higher fiber dimension strata, and the complete support and Fitting transport statement are checked. The Noetherian and finite module hypotheses of the manuscript provide the finite presentation needed by the general construction.
1812 
1813 The new checks for \cref{prop:group_algebra_transfer,thm:coinvariant_recovery,cor:dyadic_coinvariant_recovery} include actual group algebra transfer and augmentation. Coinvariant recovery uses the quotient by all balancing relations, with its universal property proved. In the commutative case, this construction is identified with the ordinary tensor product. The augmentation relations generate exactly the augmentation ideal acting on the module. Applying augmentation to the coordinates of a supplied free basis gives a coefficient basis with the same index set. The right module argument applies to arbitrary groups, including nonabelian two groups, and includes rank zero.
1814 
1815 The new checks for \cref{thm:residual_augmentation_algebra,cor:no_residual_character_splitting,cor:rank_trace_detection,prop:dyadic_sign_projectors} construct the full multivariable truncated polynomial algebra isomorphism and identify its augmentation generators. The residual group algebra is local for abelian \(p\) groups in characteristic \(p\). For each supplied Hecke idempotent, the trace is the image dimension cast into the coefficient field. For that idempotent, occupancy is equivalent to positive rank and, in characteristic zero, nonzero trace. The dyadic calculation gives the two rational sign projectors, proves that neither lies in the integral group algebra, and identifies the residual algebra with \(\FF_2[X]/(X^2)\).
1816 
1817 Corollary~\ref{cor:no_residual_character_splitting} is now checked for every finite \(p\) group, including nonabelian groups, over every field of characteristic \(p\). The proof uses a finite prime field orbit span and a nonzero fixed vector. The original unrestricted statement is restored, and the earlier explicit abelian restriction is no longer needed.
1818 
1819 The checks for \cref{prop:quotient_erases_component,thm:canonical_hecke_packets,cor:simultaneous_generalized_eigenspaces} now include the actual formal power series quotient and the canonical Hecke packet maps. In the node \(k[[x,y]]/(xy)\), quotienting by \((x)\) gives \(k[[y]]\), with support \(V(x)\). Lean verifies both irreducible components and the exclusion of the generic point \((y)\). The components can still meet, so this is not a claim that their supports are disjoint.
1820 
1821 For the Hecke results, the canonical ring decomposition in \cref{fact:artin_decomposition} remains a declared external input. Its coordinates are the actual localization maps. The module direct sum, the packet identification with the localized module, and the formula \(v\mapsto v/1\) are constructed in Lean. Nilpotence in the selected Artin local factor, together with invertibility of a generator on each other factor, gives a single positive exponent for the simultaneous generalized eigenspace. The result includes the explicit generators \(T_i-\lambda_i\), agrees with the packet used in the trace theorem, and does not assume semisimplicity.
1822 
1823 The revised five gate statement in \cref{thm:five_gate_completion} is now checked for both ordinary and derived carriers and for a general support comparison. The comparison is an actual inclusion of subsets of prime spectra, and scalar extension is proved to satisfy it. The coefficient quotient and ordinary or derived control maps yield finite level support. That conclusion is not supplied as a separate patching assumption. The specialized tensor module or derived cohomology supplies an actual nonzero eigenvector. The declared realization theorem is applied to this particular eigensystem, and the resulting representation comparison is an actual invertible linear intertwiner. The system conclusion uses the family attached to the very same automorphic object, with distinguished member identities and a common algebraic polynomial spine.
1824 
1825 The original comparison wording did not explicitly supply a compatible Hecke point over the fixed coefficient field. Support preservation alone is insufficient: extension from \(\mathbb Q\) to \(\mathbb Q(i)\) preserves full support, but there is no ring map \(\mathbb Q(i)\to\mathbb Q\) extending the identity. The revision therefore states \(y\circ f=x\) and exposes the arithmetic comparison and existing-family inputs. Residual occupancy, representability and the applicable patching theorem remain supplied arithmetic provenance. The original full statement remains partial. The completed tensor quotients and intrinsic Fitting ideals are now checked as described above, including the full Fitting transport clause.
1826 
1827 The derived realization checks cover the revised \cref{thm:derived_pointwise_realization,thm:derived_conditional_completion}. They prove vanishing outside the bounds of an actual finite projective model and construct a nonzero cohomology vector inside those bounds. The Hecke action is induced from multiplication on the original cochain model, carried through scalar extension and derived localization, and proved to act by the specialized character on actual cohomology. The conditional arithmetic step gives an actual invertible linear intertwiner from the declared realization input and common Frobenius polynomials.
1828 
1829 The original formulation of \cref{thm:derived_pointwise_realization} did not ensure that the surviving degree lies in the classicality range. A complex concentrated in degree one has full support over a field, while a classicality condition restricted to degree zero says nothing about its nonzero fiber. The revision requires the declared range to contain the model interval. The conditional conclusion of \cref{thm:derived_conditional_completion} retains applicability at the selected eigensystem itself. Both statements now expose the topology, continuity, semisimplification, and common polynomial inputs needed for the representation comparison. Their original unconditional cohomological conclusions are checked, but their original complete statements remain partial. The general support comparison and compatible-point formulation is now checked in the revised \cref{thm:five_gate_completion}, as described above.
1830 
1831 The derived support checks prove \cref{thm:derived_quotient_support,thm:derived_support_descent,cor:derived_degree_survives} as originally stated. Perfect complexes are actual derived category objects equipped with bounded finite projective models and derived isomorphisms to those models. Scalar extension is constructed on cochain complexes. Its associativity, preservation of homotopy equivalences, and independence under actual derived isomorphisms are checked. The quotient support formula uses the actual map of spectra and its image \(V(I)\). Every field valued point factors through the residue field at its kernel, and faithful flatness of field extensions preserves and reflects acyclicity. The surviving integer degree is expressed using the actual derived cohomology functor, with a corresponding witness in the specialized cochain model. These proofs do not require the external cohomological support description in \cref{fact:derived_support_cohomology}. The external classicality theorems remain supplied arithmetic inputs. The conditional derived realization argument is checked as described above.
1832 
1833 The adequacy checks prove \cref{thm:s3_adequacy} as originally stated. They construct the faithful standard representation from the actual permutation module, prove irreducibility after extension to the algebraic closure, and split every group element's characteristic polynomial over \(\FF_7\). The trace zero adjoint is the kernel of matrix trace with its conjugation action, and its sign plus standard decomposition is an actual equivariant linear isomorphism. The averaging proof is connected to Mathlib's actual first group cohomology, while the invariant calculation gives actual degree zero vanishing. Canonical projectors are identified with generalized eigenspace projectors for every positive exponent. Their trace pairings detect every nonzero endomorphism and hence every irreducible adjoint submodule. The two printed constituent witnesses and their traces are checked exactly. The adequacy definition remains a cited convention. No external adequacy theorem is assumed in this finite certificate.
1834 
1835 The realization checks cover \cref{thm:pointwise_galois_realization,cor:full_support_pointwise_automorphy,thm:one_member_propagation,thm:ordinary_conditional_completion,thm:system_completion}. Characteristic polynomial coefficients are continuous by the principal minor formula. Equality on the declared Frobenius conjugacy classes therefore extends to the whole Galois group. The finite dimensional algebra input is explicit: a supplied semisimple representative preserves every characteristic polynomial, and a general Brauer Nesbitt theorem identifies semisimple representations with equal polynomials. Lean proves independence of this representative and the irreducible conclusion. Construction of semisimplification, the general Brauer Nesbitt theorem, and arithmetic Chebotarev density remain external inputs.
1836 
1837 The ordinary completion argument derives finite generation, full finite level support, and an actual nonzero Hecke tensor fiber from the patched support and control isomorphisms. The declared classicality input then supplies the occurring automorphic object and its attached representation. Both existing compatible systems, with their common polynomial spine, are retained as hypotheses in the propagation results. These results do not construct missing companions or an attached compatible system.
1838 
1839 The pointwise realization and ordinary completion statements now explicitly require Hausdorff coefficient topology and continuity of the compared representations, including the universal specialization. The corresponding locus statement is restricted to such points. These three revised claims are counted as complete. Their original wording remains partial. This clarification also makes the coefficient topology in \cref{fact:chebotarev_brauer_nesbitt} explicit without claiming a new proof of that external arithmetic fact.
1840 
1841 The earlier revision made two further substantive corrections. In \cref{cor:componentwise_occupancy}, every irreducible component is contained in the full support. The previous sentence reversed that containment. In \cref{thm:simultaneous_companion_completion}, the coefficient, continuity, integrality, class finiteness, and quotient condition hypotheses are now explicit. Finite forests by themselves establish branches, not all arithmetic effectivity assertions. Corollary~\ref{cor:simultaneous_local} now gives the closed kernel argument and the continuity and uniqueness of its factors.
1842 
1843 The original manuscript and its literal claim records are preserved with the release. In that original census, 41 claims are fully checked, seven are partial, and one is not checked as written. The corrected \cref{cor:componentwise_occupancy} and restricted \cref{thm:simultaneous_companion_completion} are counted as proved only for their revised statements. The original unrestricted completion wording is not retrospectively marked proved. Source hashes, the exact amendments, compiler logs, and a mathematical self-review accompany the code.
1844 
1845 Compiler and axiom checks are distinguished from semantic proof review and external arithmetic results.
1846 
1847 \bibliographystyle{amsplain}
1848 \bibliography{Paper_XII_Traditional_Final}
1849 
1850 \end{document}

Back to source controls

Back to Realization Calculus