Paper_X_Block27_Amended.tex
Realization Calculus
Paper_X_Block27_Amended.tex
This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.
Included manuscript sections
1 \documentclass[11pt]{article}
2
3 \usepackage[T1]{fontenc}
4 \usepackage{lmodern}
5 \usepackage[margin=0.90in]{geometry}
6 \usepackage{microtype}
7 \usepackage{amsmath,amssymb,amsthm,mathtools,mathrsfs}
8 \usepackage{booktabs,longtable,array,tabularx}
9 \usepackage{graphicx}
10 \usepackage{float}
11 \usepackage{xcolor}
12 \usepackage{enumitem}
13 \usepackage{fancyhdr}
14 \usepackage{hyperref}
15 \usepackage[nameinlink,noabbrev]{cleveref}
16 \usepackage{listings}
17 \usepackage{caption}
18 \usepackage{bm}
19 \usepackage{needspace}
20 \usepackage{placeins}
21
22
23 \graphicspath{{figures/}}
24 \allowdisplaybreaks
25
26
27 \hypersetup{
28 pdftitle={Projector-Resolved Seed Calculus X},
29 pdfauthor={Komorebi P.},
30 pdfsubject={Universal residual seeds, deformation forests, directed transport, seed zeta functions, companion completion, compatible carriers, and finite occupancy},
31 colorlinks=true,
32 linkcolor=black,
33 citecolor=black,
34 urlcolor=black
35 }
36
37 \pagestyle{fancy}
38 \fancyhf{}
39 \fancyhead[L]{Projector-Resolved Seed Calculus X}
40 \fancyhead[R]{Komorebi P.}
41 \fancyfoot[C]{\thepage}
42 \setlength{\headheight}{14pt}
43
44 \newtheorem{theorem}{Theorem}[section]
45 \newtheorem{proposition}[theorem]{Proposition}
46 \newtheorem{lemma}[theorem]{Lemma}
47 \newtheorem{corollary}[theorem]{Corollary}
48 \theoremstyle{definition}
49 \newtheorem{definition}[theorem]{Definition}
50 \newtheorem{example}[theorem]{Example}
51 \newtheorem{conjecture}[theorem]{Conjecture}
52 \newtheorem{classicalinput}[theorem]{Classical Input}
53 \newtheorem{numericalcertificate}[theorem]{Numerical Certificate}
54 \theoremstyle{remark}
55 \newtheorem{remark}[theorem]{Remark}
56
57 \newcommand{\Ocal}{\mathcal O}
58 \newcommand{\mfrak}{\mathfrak m}
59 \newcommand{\F}{\mathbf F}
60 \newcommand{\Z}{\mathbf Z}
61 \newcommand{\Q}{\mathbf Q}
62 \newcommand{\C}{\mathbf C}
63 \newcommand{\Spf}{\operatorname{Spf}}
64 \newcommand{\Spec}{\operatorname{Spec}}
65 \newcommand{\GL}{\operatorname{GL}}
66 \newcommand{\Hom}{\operatorname{Hom}}
67 \newcommand{\End}{\operatorname{End}}
68 \newcommand{\Tr}{\operatorname{Tr}}
69 \newcommand{\Frob}{\operatorname{Frob}}
70 \newcommand{\WD}{\operatorname{WD}}
71 \newcommand{\HT}{\operatorname{HT}}
72 \newcommand{\ad}{\operatorname{ad}}
73 \newcommand{\red}{\operatorname{red}}
74 \newcommand{\Def}{\operatorname{Def}}
75 \newcommand{\rad}{\operatorname{rad}}
76 \newcommand{\srank}{\operatorname{srank}}
77 \newcommand{\Cl}{\operatorname{Cl}}
78 \newcommand{\SCC}{\operatorname{SCC}}
79 \newcommand{\rank}{\operatorname{rank}}
80 \newcommand{\im}{\operatorname{im}}
81 \newcommand{\coker}{\operatorname{coker}}
82 \newcommand{\id}{\operatorname{id}}
83 \newcommand{\Sys}{\mathscr S}
84 \newcommand{\Forest}{\mathfrak F}
85 \newcommand{\Compat}{\mathfrak C}
86 \newcommand{\Packet}{\mathfrak P}
87
88 \setlength{\parindent}{0pt}
89 \setlength{\parskip}{0.62em}
90 \setlist[itemize]{leftmargin=1.55em,itemsep=0.20em,topsep=0.30em}
91 \setlist[enumerate]{leftmargin=1.75em,itemsep=0.24em,topsep=0.32em}
92 \captionsetup{font=small,labelfont=bf}
93
94 \lstset{
95 basicstyle=\ttfamily\scriptsize,
96 breaklines=true,
97 columns=fullflexible,
98 frame=single,
99 showstringspaces=false,
100 tabsize=4,
101 numbers=left,
102 numberstyle=\tiny,
103 xleftmargin=1.5em,
104 framexleftmargin=1.2em
105 }
106
107 \title{\textbf{Projector-Resolved Seed Calculus X}\\[0.35em]
108 \large Universal Residual Seeds: Deformation Forests, Transport Categories, and System Completion}
109 \author{Komorebi P.}
110 \date{}
111
112 \usepackage{komorebi-publication}
113 \renewcommand{\KomorebiTitle}{Universal Residual Seeds}
114 \renewcommand{\KomorebiSubtitle}{Deformation forests, transport categories, and conditional system completion}
115 \renewcommand{\KomorebiSeries}{Chapter X}
116 \renewcommand{\KomorebiKind}{Mathematical text}
117 \renewcommand{\KomorebiShortTitle}{Chapter X}
118 \renewcommand{\KomorebiTitleSize}{36}
119 \renewcommand{\KomorebiTitleLeading}{41}
120 \renewcommand{\KomorebiEdition}{}
121 \KomorebiSetup
122 \begin{document}
123 \KomorebiCover
124 \KomorebiOpeningNote{Residual forests describe deformation above a fixed residual root. The later constructions compare compatible families and recover summands inside supplied carriers. Universal companion existence, carrier existence, and nonzero occupancy require additional inputs. Section~\ref{sec:conditional-final} assembles the conditional result and states those inputs explicitly.}
125
126
127
128 \begin{abstract}
129 A residual representation is a zeroth-order coordinate. All positive-depth perturbations above it may fill its formal deformation neighborhood, but they cannot move into a different residual class. This chapter develops the corresponding universal object: a residual forest whose roots are residual representations, whose finite levels are lifts modulo powers of a uniformizer, and whose infinite branches are complete characteristic-zero objects. We prove the residual partition, no-crossing, inverse-limit reconstruction, finite-branch compactness, exact smooth and singular branch counts, packet decomposition of tangent and obstruction cohomology, a directed minimum-seed theorem, rational seed-zeta formulas, and finite companion-forest completion. The coefficient prime two is represented by a weighted forest in which characteristic-zero packets may merge modulo two and become visible only at later depth. We then define a prime-independent system seed through a common Frobenius spine, prove a compatible-carrier summand theorem under finite Frobenius separation, and reduce finite occupancy in a fixed semisimple carrier to the nonnegative integer trace of an exact joint projector. The chapter does not prove that every admissible residual companion exists or that every finite Hecke packet is occupied. Those two existence statements remain the exact horizontal boundary beyond vertical deformation theory.
130 \end{abstract}
131
132 \input{reading_contract.tex}
133 \clearpage
134 \tableofcontents
135 \newpage
136
137 \section{The universal seed at residual depth}
138
139 The earlier chapters treat a seed as a primitive object together with an operator grammar, a packet system, a topology, and an exact reconstruction law. In arithmetic deformation problems, the primitive coordinate has two layers:
140
141 \[
142 \boxed{
143 \text{residual root}
144 \quad+\quad
145 \text{positive-depth deformation coordinates}.
146 }
147 \]
148
149 The distinction is structural. A correction divisible by the uniformizer changes higher digits but leaves the residual digit fixed. Therefore the correct universal arithmetic seed cannot be one residual representation unless the admissible residual space has only one point. It must contain every residual root and the complete formal neighborhood above each root.
150
151 Let \(\Ocal\) be a complete discrete valuation ring with uniformizer \(\varpi\), maximal ideal \((\varpi)\), residue field
152 \[
153 k=\Ocal/(\varpi),\qquad |k|=q,
154 \]
155 and fraction field \(K\). When a characteristic-zero conclusion is intended, assume additionally that \(\operatorname{char}K=0\). The general counting statements do not require that restriction. Let \(\mathcal M\) be a moduli functor on complete local Noetherian \(\Ocal\)-algebras with residue field \(k\), equipped with a well-defined reduction map
156 \[
157 \red_A:\mathcal M(A)\longrightarrow \mathcal M(k).
158 \]
159 For a Galois representation this means either that a framed integral model has been fixed or that the residual semisimplified class is used.
160
161 \begin{definition}[Residual seed system]\label{px:1.1}
162 For \(\bar x\in\mathcal M(k)\), define the residual fiber
163 \[
164 \mathcal M_{\bar x}(A)
165 =
166 \{x\in\mathcal M(A):\red_A(x)=\bar x\}.
167 \]
168 The point \(\bar x\) is the residual root. The family of all nonempty fibers is the residual special fiber, and the formal deformation problems above them form the residual forest.
169 \end{definition}
170
171 For a Galois problem the principal example is
172 \[
173 \bar\rho:G_{F,S}\longrightarrow \GL_n(k),
174 \]
175 with a deformation functor \(\Def_{\bar\rho}\) cut out by a determinant and selected local conditions.
176
177 \begin{figure}[H]
178 \centering
179 \includegraphics[width=0.87\linewidth]{01_residual_seed_architecture.pdf}
180 \caption{The universal residual seed is not one point. It is the special fiber together with one complete formal neighborhood above each admissible root.}
181 \end{figure}
182
183 \subsection{What the chapter is designed to separate}
184
185 Three statements are often compressed into one sentence even though they have different logical content.
186
187 \begin{enumerate}
188 \item \textbf{Vertical completeness:} every compatible perturbation stream above a fixed root reconstructs a point of its complete deformation space.
189 \item \textbf{Horizontal companion existence:} every required residual root, including roots at other coefficient primes, actually exists.
190 \item \textbf{Occupancy:} the resulting arithmetic packet occurs in a nonzero global carrier of the required type.
191 \end{enumerate}
192
193 The first belongs to deformation and inverse-limit theory. The second is a residual companion problem. The third is an arithmetic or automorphic nonvanishing problem. Neither of the last two follows from arbitrarily deep perturbation above one already occupied root.
194
195 \section{Residual partition and no crossing}
196
197 \begin{theorem}[Residual partition]\label{px:2.1}
198 For every coefficient algebra \(A\),
199 \[
200 \boxed{
201 \mathcal M(A)
202 =
203 \bigsqcup_{\bar x\in\mathcal M(k)}
204 \mathcal M_{\bar x}(A).
205 }
206 \]
207 \end{theorem}
208
209 \begin{proof}
210 Every \(A\)-valued object has one reduced object \(\red_A(x)\in\mathcal M(k)\), so the union is exhaustive. Two distinct fibers cannot intersect because an object cannot have two different reductions. Hence the union is disjoint.
211 \end{proof}
212
213 \begin{theorem}[No crossing under positive-depth perturbation]\label{px:2.2}
214 Suppose \(x,y\in\mathcal M(\Ocal)\) are related by a deformation operation that is congruent to the identity modulo \(\varpi\). Then
215 \[
216 \red(x)=\red(y).
217 \]
218 Every finite composition remains in one residual fiber. If an infinite perturbation stream converges in the \(\varpi\)-adic topology, its limit remains in the same fiber. The existence of that limit is an explicit hypothesis, not a consequence of positive depth alone.
219 \end{theorem}
220
221 \begin{proof}
222 A correction in \(\varpi\Ocal\) vanishes after reduction modulo \(\varpi\). Thus one operation preserves the residual root, and induction proves the finite statement. For a convergent stream, convergence at the first finite precision makes its reduction eventually equal to that of its limit. Every term already has the initial reduction, so the limit has that reduction too. Completeness applies to Cauchy streams. It does not make every root-preserving stream Cauchy. For example, \(0,3,0,3,\ldots\) has constant reduction modulo \(3\) but no limit modulo \(9\).
223 \end{proof}
224
225 \begin{corollary}[Zeroth-order obstruction]\label{px:2.3}
226 If two admissible objects have different residual roots, no sequence of genuinely positive-depth perturbations beginning at one can reach the other. A horizontal transport between their roots is a zeroth-order operation, not a deeper lift.
227 \end{corollary}
228
229 \begin{figure}[H]
230 \centering
231 \includegraphics[width=0.95\linewidth]{03_no_crossing_branches.pdf}
232 \caption{Each perturbation stream remains above its initial residual root. Refinement adds digits vertically. It does not move a branch horizontally.}
233 \end{figure}
234
235 \begin{numericalcertificate}[Exact residual partition]\label{px:2.4}
236 The finite implementation partitions the integers \(0,\ldots,8\) into the three classes modulo \(3\):
237 \[
238 \{0,3,6\},\qquad \{1,4,7\},\qquad \{2,5,8\}.
239 \]
240 Every tested correction of the form \(x\mapsto x+p h\) preserves the residual class exactly.
241 \end{numericalcertificate}
242
243 \section{Lift forests and inverse-limit reconstruction}
244
245 Fix \(\bar x\in\mathcal M(k)\). For \(m\ge1\), set
246 \[
247 X_m(\bar x)=\mathcal M_{\bar x}(\Ocal/\varpi^m).
248 \]
249 Reduction gives transition maps
250 \[
251 r_{m+1,m}:X_{m+1}(\bar x)\longrightarrow X_m(\bar x).
252 \]
253 A compatible branch is a sequence \((x_m)_{m\ge1}\) satisfying
254 \[
255 r_{m+1,m}(x_{m+1})=x_m.
256 \]
257
258 \begin{classicalinput}[Represented complete deformation problems]\label{px:3.1}
259 When a deformation functor is represented by a complete local ring \(R_{\bar x}\), its \(\Ocal\)-valued points are continuous local maps \(R_{\bar x}\to\Ocal\). Completeness identifies such maps with compatible maps to every quotient \(\Ocal/\varpi^m\).
260 \end{classicalinput}
261
262 \begin{theorem}[Formal inverse-limit reconstruction]\label{px:3.2}
263 Assume \(\mathcal M_{\bar x}\) is represented by a complete local \(\Ocal\)-algebra \(R_{\bar x}\). Then reduction induces a natural bijection
264 \[
265 \boxed{
266 \mathcal M_{\bar x}(\Ocal)
267 \cong
268 \varprojlim_m
269 \mathcal M_{\bar x}(\Ocal/\varpi^m).
270 }
271 \]
272 \end{theorem}
273
274 \begin{proof}
275 A continuous local homomorphism \(R_{\bar x}\to\Ocal\) reduces to a compatible family of homomorphisms into \(\Ocal/\varpi^m\). Conversely, compatible finite-level maps determine a map
276 \[
277 R_{\bar x}\longrightarrow\varprojlim_m\Ocal/\varpi^m\cong\Ocal.
278 \]
279 The two constructions are inverse because equality in a separated complete ring is detected modulo every power of its maximal ideal.
280 \end{proof}
281
282 \begin{theorem}[Finite-branch compactness]\label{px:3.3}
283 Suppose every \(X_m(\bar x)\) is finite and nonempty and every node has finitely many children. Then the lift tree above \(\bar x\) contains an infinite compatible branch.
284 \end{theorem}
285
286 \begin{proof}
287 The tree is infinite because it has a nonempty level at every depth, and it is finitely branching by hypothesis. K\"onig's lemma gives an infinite path. The edge relation is reduction, so that path is a compatible branch.
288 \end{proof}
289
290 Surjectivity of every transition map is sufficient but not necessary. Finite branching and nonempty arbitrarily deep levels are the compactness mechanism.
291
292 \begin{proposition}[Smooth formal branch count]\label{px:3.4}
293 If
294 \[
295 R_{\bar x}\cong\Ocal[[t_1,\ldots,t_d]]\quad\text{as complete local }\Ocal\text{-algebras},
296 \]
297 then
298 \[
299 \boxed{
300 \#X_m(\bar x)=q^{d(m-1)}.
301 }
302 \]
303 Fix a uniformizer and a section \(s:k\to\Ocal\) of reduction, with \(s(0)=0\). Every \(\Ocal\)-valued branch is encoded by \(d\) positive-depth digit streams
304 \[
305 t_i=s(a_{i,1})\varpi+s(a_{i,2})\varpi^2+\cdots,
306 \qquad a_{i,j}\in k,
307 \]
308 \end{proposition}
309
310 \begin{proof}
311 A local map sends each parameter into the image of \((\varpi)\) in \(\Ocal/\varpi^m\). Conversely, every tuple in that image is nilpotent and defines a coefficient-preserving evaluation homomorphism. This homomorphism is local. To prove uniqueness without assuming continuity of an arbitrary competing homomorphism, observe in one variable that a homomorphism killing \(X^N\) only sees the finite polynomial truncation modulo \(X^N\). Induction over the finite number of variables gives uniqueness in all dimensions. The actual local maps are therefore in bijection with the full parameter tuple set. Its cardinality is \(q^{d(m-1)}\), including the zero-dimensional chart.
312
313 For integral maps, reduce an arbitrary tuple in \((\varpi)\Ocal\) at every precision, evaluate there, and use the represented-map reconstruction theorem. The finite evaluations are compatible, the reconstructed algebra map is local, and every competing local map has the same finite reductions. Separatedness gives uniqueness. Local maps are continuous in the maximal-ideal adic topologies. This establishes the integral parameter classification rather than assuming it from the finite count.
314
315 For the digit claim, subtract the chosen representative of the residue and divide the remainder by the uniformizer. Iterating gives unique digits. Conversely, the partial sums of any digit stream form a compatible Cauchy family and reconstruct uniquely by completeness and separatedness. More precisely, for each parameter there is a unique stream \((a_{i,j})_{j\ge1}\) such that
316 \[
317 \varpi^{n+1}\mid t_i-\sum_{j=1}^{n}s(a_{i,j})\varpi^j\qquad(n\ge0).
318 \]
319 The section is a set-theoretic section of reduction, not an asserted embedding of residue fields into the coefficient ring. Finally, a supplied local \(\Ocal\)-algebra isomorphism from \(R_{\bar x}\) transports both the map classification and the count.
320 \end{proof}
321
322 \begin{figure}[H]
323 \centering
324 \includegraphics[width=0.94\linewidth]{02_residual_digit_forest.pdf}
325 \caption{The first four levels of a full \(3\)-adic digit forest. A path is a compatible finite-depth perturbation stream.}
326 \end{figure}
327
328 \begin{figure}[H]
329 \centering
330 \includegraphics[width=0.82\linewidth]{04_inverse_limit_digits.pdf}
331 \caption{A compatible base-five residue tower reconstructs the digit stream \((2,4,1,3,0,2)\).}
332 \end{figure}
333
334 \section{Tangent and obstruction packets}
335
336 For a residual representation \(\bar\rho\), first-order deformations and lifting obstructions are classically controlled by cohomology of the adjoint module. The projector calculus does not replace that theory. It resolves the controlling complex into invariant packets when suitable projectors exist.
337
338 \begin{classicalinput}[Tangent and obstruction spaces]\label{px:4.1}
339 For a framed representation problem, first-order lifts are described by \(Z^1(G,\ad\bar\rho)\). For an unframed Schur problem, tangent directions are described by \(H^1(G,\ad\bar\rho)\). Relations in a presentation of a deformation ring map into \(H^2(G,\ad\bar\rho)\), which contains the obstruction classes.
340 \end{classicalinput}
341
342 Let
343 \[
344 C^0\xrightarrow{d_0}C^1\xrightarrow{d_1}C^2\xrightarrow{}\cdots
345 \]
346 be a cochain complex over a field. Suppose a finite family of projectors \(P_j^r:C^r\to C^r\) satisfies
347 \[
348 \sum_jP_j^r=I,
349 \qquad
350 P_i^rP_j^r=\delta_{ij}P_j^r,
351 \qquad
352 d_rP_j^r=P_j^{r+1}d_r.
353 \]
354
355 \begin{theorem}[Cohomology packet decomposition]\label{px:4.2}
356 Under these hypotheses, each packet is a subcomplex and
357 \[
358 \boxed{
359 H^r(C^\bullet)
360 \cong
361 \bigoplus_jH^r(P_jC^\bullet).
362 }
363 \]
364 In particular,
365 \[
366 H^1=\bigoplus_jH^1_j,
367 \qquad
368 H^2=\bigoplus_jH^2_j,
369 \]
370 so tangent and obstruction spaces reconstruct exactly from their packet components.
371 \end{theorem}
372
373 \begin{proof}
374 For each packet, use the actual image submodules
375 \(C_j^r=\operatorname{im}P_j^r\). Commutation with the differential
376 makes these a subcomplex. Write
377 \[
378 Z^r=\ker d_r,\qquad B^r=\operatorname{im}d_{r-1}\subseteq Z^r,
379 \qquad H^r=Z^r/B^r,
380 \]
381 and define \(Z_j^r,B_j^r,H_j^r\) using the restricted differentials of
382 \(C_j^\bullet\). The inclusion \(i_j:C_j^\bullet\to C^\bullet\)
383 and the image-valued projection \(p_j:C^\bullet\to C_j^\bullet\)
384 are cochain maps, so they induce maps on these genuine quotients.
385
386 For \(i\ne j\), orthogonality gives
387 \(H(p_i)H(i_j)=0\). Idempotence gives
388 \(H(p_j)H(i_j)=I\), and completeness gives
389 \(\sum_j H(i_j)H(p_j)=I\). Thus the maps
390 \[
391 [z]\longmapsto([P_j^r z])_j,
392 \qquad
393 ([z_j])_j\longmapsto\left[\sum_j i_j z_j\right]
394 \]
395 are inverse linear maps. The finite product equals the direct sum, proving
396 the assertion. In the formalization, both sides are also identified with
397 Mathlib's standard homology objects of the genuine graded complexes.
398 \end{proof}
399
400 \paragraph{Scope of the splitting.}
401 The algebraic proof works over any commutative ring and does not divide by
402 \(2\), so it applies in characteristic two when the stated integral
403 chain projectors exist. It does not construct those projectors. The
404 identification of a particular Galois tangent or obstruction problem with
405 this cohomology remains the preceding classical input.
406 The splitting detects vanishing:
407 \[
408 H^r(C^\bullet)=0\quad\Longleftrightarrow\quad
409 H^r(C_j^\bullet)=0\text{ for every }j.
410 \]
411 It does not force either side to vanish or decouple nonlinear deformation
412 equations. Moreover, commutation with the differential is essential:
413 complementary idempotents on the underlying vector spaces need not
414 preserve cocycles or coboundaries.
415
416 \paragraph{Naturality.}
417 If a cochain map \(F:C^\bullet\to D^\bullet\) intertwines the supplied
418 projectors, it restricts to maps \(F_j:C_j^\bullet\to D_j^\bullet\).
419 The direct-sum decomposition commutes with \(H^r(F)\) and the family
420 \(H^r(F_j)\). This is checked using representatives in the actual
421 quotients, independently of any dimension computation.
422
423
424 \begin{remark}[Odd and dyadic nonlinear equations]\label{px:4.3}
425 At odd residue characteristic, a differential graded Lie model may be written in Maurer--Cartan form
426 \[
427 d\eta+\frac12[\eta,\eta]=0,
428 \]
429 and a cyclic grading converts this into exact packet convolutions. At residue characteristic two, division by \(2\) is not integral. A quadratic or divided-square refinement must be retained. This is one reason the dyadic residual forest is weighted rather than obtained by formal substitution into the odd-prime formulas.
430 \end{remark}
431
432 \begin{numericalcertificate}[Finite packet complex]\label{px:4.4}
433 The exact modular test uses two invariant subcomplexes over \(\F_5\). Their cohomology dimensions are
434 \[
435 (0,0,0),
436 \qquad
437 (1,2,1),
438 \]
439 and the reconstructed total is
440 \[
441 \dim(H^0,H^1,H^2)=(1,2,1).
442 \]
443 The packet-sum residual is zero.
444 \end{numericalcertificate}
445
446 \paragraph{An explicit realization of the finite pattern.}
447 A separate finite-complex implementation uses
448 \[
449 \mathbf F_5^2\xrightarrow{d_0}\mathbf F_5^4\xrightarrow{d_1}\mathbf F_5^2,
450 \quad d_0(a,b)=(a,0,0,0),\quad d_1(a,b,c,d)=(b,0).
451 \]
452 The first packet is the exact complex with dimensions \((1,2,1)\),
453 and the second packet has zero differentials and dimensions \((1,2,1)\).
454 The actual middle cohomology is linearly isomorphic to \(\mathbf F_5^2\),
455 which is checked in Lean. Independent exhaustive coset tests check all
456 three cohomology degrees after changes of basis. This realizes the displayed dimension pattern. Its formal check is
457 distinct from the original companion implementation.
458
459
460 \begin{figure}[H]
461 \centering
462 \includegraphics[width=0.78\linewidth]{11_tangent_obstruction_packets.pdf}
463 \caption{A finite chain-projector model. Tangent and obstruction dimensions are carried by one packet and reconstruct exactly.}
464 \end{figure}
465
466 \section{The weighted dyadic residual forest}
467
468 At an odd prime, distinct sign characters remain distinct in the residue field. At the coefficient prime two,
469 \[
470 1\equiv-1\pmod2.
471 \]
472 Thus distinct characteristic-zero packets can share one residual root and separate only after more precision is retained.
473
474 \begin{definition}[Visibility weight]\label{px:5.1}
475 For two integral packet coordinates \(a,b\in\Ocal\), define their separation depth
476 \[
477 w(a,b)=\min\{m\ge1:a\not\equiv b\pmod{\varpi^m}\},
478 \]
479 when such an \(m\) exists. A dyadic packet decomposition is weighted by these first visibility depths and by the valuations of any denominators required by its rational projectors.
480 \end{definition}
481
482 \begin{example}[The two sign branches]\label{px:5.2}
483 The characters \(\chi_+(g)=1\) and \(\chi_-(g)=-1\) have the same reduction modulo \(2\), but
484 \[
485 1\not\equiv-1\pmod4.
486 \]
487 Their first separation depth is therefore \(2\). One mod-two root contains two branches that become distinct at the next level.
488 \end{example}
489
490 \begin{figure}[H]
491 \centering
492 \includegraphics[width=0.82\linewidth]{05_dyadic_delayed_separation.pdf}
493 \caption{The sign packets merge at residual depth and separate at depth two. This is a genuine change in integral coordinates, not a numerical plotting effect.}
494 \end{figure}
495
496 A simple weighted formal model already captures delayed visibility. Let \(w_i\ge1\) and constrain
497 \[
498 t_i\in(\varpi^{w_i}\Ocal+\varpi^m\Ocal)/\varpi^m\Ocal.
499 \]
500 Then coordinate \(i\) is invisible until \(m>w_i\).
501
502 \begin{proposition}[Weighted smooth-chart count]\label{px:5.3}
503 For weights \(\bm w=(w_1,\ldots,w_d)\),
504 \[
505 \boxed{
506 N_{\bm w}(m)
507 =
508 q^{\sum_{i=1}^d\max(m-w_i,0)}.
509 }
510 \]
511 \end{proposition}
512
513 \begin{proof}
514 The image of \(\varpi^{w_i}\Ocal\) in \(\Ocal/\varpi^m\) has one element when \(m\le w_i\), and \(q^{m-w_i}\) elements when \(m>w_i\). Multiplying the independent coordinate counts gives the formula.
515 \end{proof}
516
517 This model does not assert that every dyadic Galois deformation ring is a weighted formal ball. It gives the exact local counting law once such weighted coordinates or a Smith-normal-form chart have been proved.
518
519 \begin{figure}[H]
520 \centering
521 \includegraphics[width=0.82\linewidth]{07_weighted_formal_chart.pdf}
522 \caption{Weights delay finite-depth visibility. Once all coordinates are active, the asymptotic slope equals the ordinary formal dimension.}
523 \end{figure}
524
525 \section{Seed zeta functions and branching dimensions}
526
527 Finite-depth counts record more than the existence of a branch. They distinguish smooth, weighted, and singular local geometry.
528
529 \begin{definition}[Seed zeta function]\label{px:6.1}
530 For a residual root \(\bar x\) with finite levels, define
531 \[
532 \boxed{
533 Z_{\bar x}(T)
534 =
535 \sum_{m\ge1}\#X_m(\bar x)T^m.
536 }
537 \]
538 When a weighted chart is specified, write \(Z_{\bm w}(T)\).
539 \end{definition}
540
541 \begin{theorem}[Smooth seed zeta function]\label{px:6.2}
542 For a smooth formal component of dimension \(d\),
543 \[
544 \boxed{
545 Z_d(T)=\frac{T}{1-q^dT}.
546 }
547 \]
548 \end{theorem}
549
550 \begin{proof}
551 By the proved formal-model map-to-parameter equivalence, \(\#X_m=q^{d(m-1)}\) counts all the actual local coefficient-algebra maps. Summing the geometric series gives the identity. The checked statement is an equality of infinite formal power series, with zero constant coefficient.
552 \end{proof}
553
554 \begin{theorem}[Weighted seed zeta function]\label{px:6.3}
555 Let \(1\le w_1\le\cdots\le w_d\), put \(W=\sum_iw_i\), and let
556 \[
557 a_m=q^{\sum_i\max(m-w_i,0)}.
558 \]
559 Then
560 \[
561 \boxed{
562 Z_{\bm w}(T)
563 =
564 \sum_{m=1}^{w_d}a_mT^m
565 +
566 q^{-W}\frac{(q^dT)^{w_d+1}}{1-q^dT}.
567 }
568 \]
569 In particular, every weighted smooth chart has a rational seed zeta function.
570 \end{theorem}
571
572 \begin{proof}
573 The finite sum records the depths before all coordinates are active. For \(m\ge w_d+1\),
574 \[
575 a_m=q^{dm-W},
576 \]
577 so the remaining terms form one geometric series.
578 \end{proof}
579
580 \begin{theorem}[Singular power seed]\label{px:6.4}
581 For integers \(e\ge1\) and \(m\ge1\), in \(\Ocal/\varpi^m\) the equation
582 \[
583 x^e=0
584 \]
585 has exactly
586 \[
587 \boxed{
588 q^{m-\lceil m/e\rceil}
589 }
590 \]
591 solutions. Its seed zeta function is
592 \[
593 \boxed{
594 Z_e(T)
595 =
596 \frac{\sum_{r=1}^{e}q^{r-1}T^r}
597 {1-q^{e-1}T^e}.
598 }
599 \]
600 \end{theorem}
601
602 \begin{proof}
603 The congruence is equivalent to
604 \[
605 e\,v_\varpi(x)\ge m,
606 \]
607 so \(x\) must lie in \(\varpi^{\lceil m/e\rceil}\Ocal/\varpi^m\), which has the stated cardinality. Write \(m=ek+r\), \(1\le r\le e\). The exponent becomes \((e-1)k+r-1\). Summing over \(k\ge0\) and \(1\le r\le e\) gives the rational expression.
608 \end{proof}
609
610 \begin{definition}[Branching dimension]\label{px:6.5}
611 When the limit exists, define the finite-level counting exponent
612 \[
613 \dim_{\mathrm{seed}}(\bar x)
614 =
615 \lim_{m\to\infty}
616 \frac{\log_q\#X_m(\bar x)}{m}.
617 \]
618 A limsup may be used in general.
619 \end{definition}
620
621 \begin{corollary}[Fractional singular dimension]\label{px:6.6}
622 For \(x^e=0\),
623 \[
624 \boxed{
625 \dim_{\mathrm{seed}}=1-\frac1e.
626 }
627 \]
628 In particular, \(x^2=0\) has branching dimension \(1/2\).
629
630 \paragraph{Counting exponent versus compatible branches.}
631 The preceding exponent counts all finite-level solutions, including nodes which cannot lift indefinitely. It is not the cardinality or dimension of the space of infinite branches. In fact every compatible tower of solutions to \(x^e=0\), for \(e\ge1\), is the zero tower. For each \(m\), a solution at depth \(em\) lies in \(\varpi^m\Ocal/\varpi^{em}\). Its reduction at depth \(m\) is therefore zero. Compatibility proves the assertion at every depth. The formal companion identifies proofs of both this observation and the real logarithmic limit.
632
633 \end{corollary}
634
635 \begin{figure}[H]
636 \centering
637 \includegraphics[width=0.83\linewidth]{06_smooth_singular_counts.pdf}
638 \caption{A smooth two-dimensional formal chart and the singular equation \(x^2=0\) have visibly different exponential growth.}
639 \end{figure}
640
641 \begin{figure}[H]
642 \centering
643 \includegraphics[width=0.78\linewidth]{08_fractional_seed_dimension.pdf}
644 \caption{The finite-depth branching dimension of \(x^e=0\) is \(1-1/e\), giving a family of fractional local growth exponents.}
645 \end{figure}
646
647 \section{Residual transport categories}
648
649 Vertical lifting never changes a residual root. Horizontal coverage requires operations whose residual effect is not congruent to the identity. Examples that may define such transports include twisting, duality, restriction, induction, tensor product, symmetric powers, exterior powers, and functorial transfer. The word ``may'' is essential: each operation must preserve the deformation conditions and the realization statement being transported.
650
651 \begin{definition}[Admissible residual transport]\label{px:7.1}
652 An admissible transport from \(\bar\rho\) to \(\bar\rho'\) consists of
653 \[
654 \mathcal T:\bar\rho\longmapsto\bar\rho'
655 \]
656 together with natural maps
657 \[
658 \mathcal T_A:\Def_{\bar\rho}(A)\longrightarrow\Def_{\bar\rho'}(A)
659 \]
660 for every coefficient algebra \(A\), compatible with base change and reduction. When the transport is reversible, it is an isomorphism in the residual transport groupoid. One-way operations give a directed category.
661 \end{definition}
662
663 For a finite collection of roots, record a directed edge \(u\to v\) whenever occupancy or the relevant property is known to propagate from \(u\) to \(v\).
664
665 \begin{definition}[Directed seed rank]\label{px:7.2}
666 For a directed transport graph \(G\), define
667 \[
668 \srank_G
669 =
670 \min\{|S|:\Cl_G(S)=V(G)\},
671 \]
672 where \(\Cl_G(S)\) is the set of vertices reachable from \(S\).
673 \end{definition}
674
675 \begin{theorem}[Directed minimum-seed theorem]\label{px:7.3}
676 Let \(G\) be a finite directed graph. Collapse every strongly connected component to one vertex, obtaining the condensation DAG. Then
677 \[
678 \boxed{
679 \srank_G
680 =
681 \#\{\text{source strongly connected components of }G\}.
682 }
683 \]
684 One representative from each source component is a minimum seed set.
685 \end{theorem}
686
687 \begin{proof}
688 Every vertex of a finite DAG is reachable from a source, so one seed in each source component reaches the entire condensation graph. Within a strongly connected component, one vertex reaches every other. Hence the source representatives are sufficient.
689
690 Conversely, a source component has no incoming edge from another component. It cannot be reached from a seed outside itself, so every generating seed set must meet it. Therefore the number of source components is also a lower bound.
691 \end{proof}
692
693 For reversible transports the condensation has one vertex per connected component, recovering the undirected minimum-seed theorem.
694
695 \paragraph{Formal scope and propagation.}
696 Reachability is the reflexive-transitive closure of the supplied directed edge
697 relation, and a strongly connected component is the actual quotient by mutual
698 reachability. The minimum seed count is defined independently as the least
699 cardinality of a set that reaches all vertices. Every covering set must meet
700 every source component. Conversely, meeting every source component suffices
701 in a finite graph. Thus any choice of one representative from each source is
702 optimal. Empty graphs have rank zero, and self-loops are permitted. Adding
703 admissible edges cannot increase the minimum seed count.
704
705 If a property $P$ propagates along every supplied edge and holds at all selected
706 seeds, it holds at every reached vertex. These are explicit hypotheses. The
707 minimum-seed theorem does not construct valid arithmetic edges or supply
708 initial occupancy.
709
710 \paragraph{Why the finite hypothesis cannot be dropped.}
711 Take vertices $\{*\}\sqcup\{v_n:n\in\mathbf N\}$, with $*$ isolated and
712 edges $v_{n+1}\to v_n$. Every strongly connected component is a singleton,
713 and $\{*\}$ is the unique source component. No finite seed set covers all
714 vertices: it can reach only indices no larger than the largest chosen index.
715 Both the unique-source statement and the failure of every finite cover are
716 checked in Lean. Hence one source component in an infinite condensation does
717 not imply that one seed reaches all objects.
718
719
720 \begin{figure}[H]
721 \centering
722 \includegraphics[width=0.91\linewidth]{09_directed_transport_graph.pdf}
723 \caption{A finite directed transport model. The components \(\{A,B\}\), \(\{D,E\}\), and \(\{G\}\) are sources. \(C\) and \(F\) are reached downstream.}
724 \label{fig:transport-graph}
725 \end{figure}
726
727 \begin{figure}[H]
728 \centering
729 \includegraphics[width=0.86\linewidth]{10_source_scc_condensation.pdf}
730 \caption{The condensation DAG makes the minimum seed count visible without searching every subset of roots.}
731 \end{figure}
732
733 \begin{numericalcertificate}[Directed seed count]\label{px:7.4}
734 The test graph has five strongly connected components and three source components. The theorem gives seed rank three. Exhaustive search over every subset of vertices independently returns three, and the selected representatives reach all seven roots.
735
736 \paragraph{An explicit realization of the directed graph.}
737 An independently specified graph has vertices $A,B,C,D,E,F,G$ and the eight edges
738 \[
739 A\to B,\ B\to A,\ B\to C,\ C\to F,\ D\to E,\ E\to D,\ E\to F,\ G\to F.
740 \]
741 The source components are $\{A,B\}$, $\{D,E\}$, and $\{G\}$. The other
742 components are $\{C\}$ and $\{F\}$. A bounded path search to length three
743 is proved closed under every original edge, which certifies equality with
744 unbounded reachability. The resulting label certificate is identified with
745 the actual quotient by mutual reachability. Lean checks seed rank three and
746 exactly the four minimum sets
747 \[
748 \{A,D,G\},\quad\{A,E,G\},\quad\{B,D,G\},\quad\{B,E,G\}.
749 \]
750 Independent exact tests enumerate every directed graph on zero through four
751 vertices, including loops, and every seed subset. These finite tests audit the
752 implementation. The universal theorem is a separate formal proof.
753
754 \end{numericalcertificate}
755
756 \section{Prime-independent system seeds}
757
758 A compatible system should not be treated as an unrelated collection of \(\lambda\)-adic roots. Its members share algebraic Frobenius polynomials, Hodge--Tate data, determinant information, and local Weil--Deligne packets.
759
760 \begin{definition}[Common arithmetic spine]\label{px:8.1}
761 Let \(M\) be a number field. A common spine \(\Compat\) consists of:
762 \begin{itemize}
763 \item characteristic polynomials \(P_v(X)\in M[X]\) at almost all places;
764 \item coefficient-prime independent weight and determinant data;
765 \item prescribed local Weil--Deligne or inertial packet labels at the ramified places.
766 \end{itemize}
767 For each finite place \(\lambda\) of \(M\), let
768 \[
769 X_{\lambda,m}(\Compat)
770 \]
771 be the finite set of admissible objects modulo \(\varpi_\lambda^m\) realizing the reduction of this spine.
772 \end{definition}
773
774 The system seed is the fibered object
775 \[
776 \boxed{
777 \Sys_{\mathrm{sys}}
778 =
779 \Sys_2^{\mathrm{wt}}
780 \times_{\Compat}
781 \prod_{\lambda\nmid2}'\Sys_\lambda.
782 }
783 \]
784 The fiber product notation states a compatibility requirement. It does not prove that every fiber is nonempty.
785
786 \begin{theorem}[Adelic finite-depth completion]\label{px:8.2}
787 Assume:
788 \begin{enumerate}
789 \item an algebraic common spine \(\Compat\) over a number field \(M\) is fixed;
790 \item for every finite place \(\lambda\) of \(M\) and every \(m\ge1\), the companion level \(X_{\lambda,m}(\Compat)\) is finite and nonempty;
791 \item the reduction forests are finitely branching;
792 \item the selected local conditions are closed under inverse limits.
793 \end{enumerate}
794 Then for every \(\lambda\) there is an infinite compatible branch
795 \[
796 \rho_\lambda\in\varprojlim_mX_{\lambda,m}(\Compat),
797 \]
798 and the collection \(\{\rho_\lambda\}_\lambda\) realizes the prescribed strictly compatible spine.
799 \end{theorem}
800
801 \begin{proof}
802 Finite-branch compactness gives an infinite branch in every coefficient-prime forest. Inverse-limit closure gives an admissible \(\lambda\)-adic object. By definition each finite level has the prescribed reductions of the common Frobenius and local packets. Equality at every finite precision implies equality in the complete coefficient ring. Thus all members realize the same spine.
803 \end{proof}
804
805 \begin{corollary}[Residual companion obstruction]\label{px:8.3}
806 If
807 \[
808 X_{\lambda,1}(\Compat)=\varnothing
809 \]
810 for one coefficient prime \(\lambda\), no compatible completion with spine \(\Compat\) exists. Deeper perturbations at other primes cannot create the missing residual companion.
811 \end{corollary}
812
813 \begin{figure}[H]
814 \centering
815 \includegraphics[width=0.82\linewidth]{13_common_system_spine.pdf}
816 \caption{The local members are coordinates of one system only after their finite data descend to a common algebraic spine.}
817 \end{figure}
818
819 \begin{example}[A scalar companion failure]\label{px:8.4}
820 For
821 \[
822 f(x)=x^2+1,
823 \]
824 there are two simple branches at \(p=5\) and \(p=13\), no residual roots at \(p=3\) or \(p=7\), and one root modulo \(2\) that has no child modulo \(4\). A complete \(5\)-adic branch therefore does not imply an adelic solution.
825 \end{example}
826
827 \begin{figure}[H]
828 \centering
829 \includegraphics[width=0.79\linewidth]{12_companion_forest_occupancy.pdf}
830 \caption{Finite companion levels for \(x^2+1=0\). The obstruction at \(2,3,7\) is visible before any deep lifting argument begins.}
831 \end{figure}
832
833
834 \paragraph{Conditional scope and complete assembly.}\phantomsection\label{book:x-construction-23}
835 The theorem above is conditional on the chosen spine and the stated local
836 inverse-limit closure. In the fixed-rank integral representation setting,
837 ``closed under inverse limits'' means that every compatible family of admissible
838 finite representation classes, after coherent matrix framing and reconstruction,
839 satisfies the full selected local realization relations. It is not merely
840 closedness of an unrelated label space. Weight and packet relations retain their
841 supplied arithmetic meaning. They are parameters of the universal theorem.
842 For a general moduli functor, effectivity requires its own reconstruction
843 hypothesis or the corresponding full meaning of admissible inverse-limit closure.
844
845 The complete Lean assembly now includes the common polynomials, good-place sets
846 with finite complements, coefficient-specific prescribed determinants, and every
847 selected weight and packet relation. Determinants are recovered from their
848 actual finite-class determinants. A single common field-valued character on the
849 whole Galois group is not assumed. The returned representations are continuous,
850 and their reductions form the actual compatible branches. Their common
851 polynomial identities hold at every declared good place, hence almost everywhere
852 for each coefficient prime.
853
854 This checks Claim 8.2 as the universal conditional source theorem. The previous
855 partial status also demanded proofs that particular intended arithmetic packets
856 satisfy its premises. That stronger application target is not a conclusion of
857 the theorem. Concrete Hodge--Tate and Weil--Deligne attachments, torsion interpretations,
858 closure instances, and companion nonemptiness remain obligations of arithmetic
859 applications. Inertial-type labels are not upgraded to full Weil--Deligne data.
860
861 \paragraph{Checked representation-level completion and its arithmetic boundary.}
862 The representation-level completion construction works with actual matrix
863 representations of a fixed group. For a complete separated ring $R$
864 and ideal $I$, compatible maps
865 $\rho_m:G\to\operatorname{GL}_d(R/I^m)$ reconstruct a unique integral
866 representation for that fixed compatible family. Multiplication and inverses
867 are verified after every reduction. If all finite representations are continuous
868 for the discrete quotient topology, the integral representation is continuous
869 for the ideal-adic topology. This does not assert uniqueness among all possible
870 branches of the allowed forest.
871
872 The forest has as its level the actual subtype of representations satisfying
873 the declared finite conditions. Those conditions must be preserved by reduction.
874 Finiteness and nonemptiness at every level give an infinite branch and hence an
875 actual continuous representation. Finiteness of the coefficient quotient alone
876 is not a substitute for finiteness of the allowed representation set for an
877 arbitrary source group. Surjectivity of the reductions is not required.
878
879 All coefficients of the characteristic polynomial commute with reduction.
880 Consequently, prescribed integral characteristic polynomials at every precision
881 hold exactly in the reconstructed representation. For a common coefficient field
882 $E$, local integral polynomials lie in $\Ocal_\lambda[X]$ and are compared with
883 $P_v\in E[X]$ only after mapping both into the local coefficient field. No field
884 embedding $E\to\Ocal_\lambda$ is assumed. The allowed-place predicate is explicit
885 and may depend on $\lambda$. Trivial action on a supplied subgroup is likewise
886 detected at every precision. Identifying that subgroup with arithmetic inertia
887 is a separate input.
888
889 The eleventh block assembles continuous coefficient-field representations, exact
890 common polynomials and the prescribed local predicate from positive finite
891 depths. Depth-zero finiteness and nonemptiness are derived. Claims 8.2 and 11.1
892 already assume inverse-limit closure of the selected local conditions. An
893 unconditional closure theorem is not a missing hypothesis of their conditional
894 proofs. Their conditional matrix core is checked. The remaining full arithmetic
895 interpretation must identify the admissible finite objects and the actual local
896 invariants with these data. The coherent-framing obligation is resolved by the \hyperref[book:x-construction-14]{completion from conjugacy classes}
897 below. An arbitrary local
898 predicate is not being renamed Hodge--Tate or Weil--Deligne compatibility.
899
900
901 \paragraph{Completion from conjugacy classes.}\phantomsection\label{book:x-construction-14}
902 Over an $I$-adically complete separated commutative coefficient ring $R$,
903 for a fixed finite rank, the formalization now takes finite-level objects to be
904 actual matrix representations modulo conjugation by an invertible matrix.
905 Assume the coefficient quotients $R/I^k$ are finite.
906 Conjugation commutes with coefficient reduction, and each conjugacy class has
907 finitely many frames over a finite coefficient ring. Thus finite allowed class
908 levels give finite full preimages of allowed matrix representations. Downward
909 admissibility and positive-depth nonemptiness yield an exactly compatible
910 matrix branch and an actual integral representation. More strongly, every
911 prescribed compatible class branch has such representatives, using finite
912 nonempty fibers over that branch. No surjectivity of reductions or lifting of
913 prescribed change-of-basis matrices is assumed. This does not assert uniqueness
914 up to integral conjugacy.
915
916 For finitely generated $I$ with finite $R/I$, finiteness of $R/I^k$ is derived.
917 One continuous representative per allowed class suffices, because continuity
918 is proved invariant under conjugation. Characteristic polynomials, determinants
919 and trivial action on a supplied subgroup are likewise actual invariants.
920 The unframed common-spine theorem constructs continuous coefficient-field
921 representations with the prescribed whole polynomials and the explicitly
922 supplied inverse-limit-closed local predicate.
923
924 An actual $\mathbb Z_3$ example applies the class-level completion theorem
925 for the cyclic group of order two and polynomial $X^2-1$, producing a nonidentity generator. Another
926 checked example has compatible classes represented by
927 $\operatorname{diag}(1,-1)$ modulo $3$ and
928 $\operatorname{diag}(-1,1)$ modulo $9$: these chosen matrices disagree under
929 reduction, and an actual swap of basis repairs them. Arbitrary independent
930 representatives therefore do not replace the framing argument.
931
932 The framing obligation is finished. Identifying the manuscript's arithmetic
933 admissible objects, actual local invariants and finite-level packet reductions
934 with this interface remains separate. An uninterpreted local predicate is not
935 a construction of Hodge--Tate or Weil--Deligne compatibility. The source's local
936 closure hypothesis remains explicit. The \hyperref[book:x-construction-23]{conditional completion construction} completes the universal
937 conditional implication. These particular arithmetic applications remain
938 unproved.
939
940
941 \paragraph{Actual local comparisons from fixed-depth certificates.}\phantomsection\label{book:x-construction-15}
942 Let $R$ be an $I$-adically complete separated commutative ring with finite
943 coefficient quotients and an injective map into a field $K$. Fix a finite matrix
944 rank. For finitely many
945 local group maps $\phi_s:H_s\to G$ and integral template representations
946 $\tau_s$, fix detecting depths $d_s$. At precision $m$ retain matrices $P_{s,m}$
947 as part of the admissible object and require
948 \[
949 \rho_m(\phi_s(h))P_{s,m}=P_{s,m}\tau_{s,m}(h).
950 \]
951 For $m\ge d_s$ require their determinants to remain nonzero after reduction to
952 $R/I^{d_s}$. Earlier levels omit that test. Finite occupied augmented levels
953 give a compatible branch of both representations and comparisons. The integral
954 limits satisfy the actual equations and have nonzero determinants, so the
955 comparisons are units over $K$. A converse supplies all finite nodes from any
956 integral realization with these detectors. Finite-level invertibility and
957 compatible prior choices of comparisons are not assumed.
958
959 The unframed positive-depth version also retains continuity and whole common
960 polynomials. Its actual local isomorphisms are derived from the certificates.
961 There is no uninterpreted local-stability predicate for this particular problem.
962 The fixed depths and augmented-level occupancy remain explicit inputs.
963
964 The formalization specializes to the actual maps
965 $G_{\mathbb Q_p}\to G_{\mathbb Q}$ induced by the field embeddings and choices
966 of algebraic closures. A nontrivial continuous quadratic character of
967 $G_{\mathbb Q}$, constructed from its action on $i^2=-1$, gives the integral
968 $2$-adic actions
969 \[
970 \tau(\sigma)=\operatorname{diag}(1,-1),\quad
971 \rho(\sigma)=\begin{pmatrix}1&-1\\0&-1\end{pmatrix},\quad
972 P=\begin{pmatrix}1&1\\0&2\end{pmatrix}
973 \]
974 at a nonidentity quadratic element. The determinant $2$ is detected modulo $4$.
975 The representations are conjugate over $\mathbb Q_2$ but not integrally
976 conjugate. A separate $\mathbb Z_3$ example invokes simultaneous completion
977 and reconstructs a comparison which is an integral nonunit and a field unit.
978
979 The bound is substantive: for the unipotent actions
980 $\rho_a(g)=\begin{pmatrix}1&ag\\0&1\end{pmatrix}$, every integral intertwiner
981 with $\rho_1$ has determinant $aP_{22}^2$. Taking $a=\pi^n$ for a nonzero
982 $\pi\in I$ rules out every
983 fixed detecting depth, even though all the field-valued approximants are
984 isomorphic and their integral limit is trivial. This does not refute Claim 8.2,
985 which already assumes inverse-limit closure of its chosen local conditions.
986
987 Exact prescribed local Galois action is stronger than an inertial-type label.
988 The common arithmetic packet interpretation, its coefficient comparisons and
989 the actual Hodge--Tate/Weil--Deligne attachment remain separate. The new theorem
990 does not supply a uniform bound for all intended arithmetic packets. Those
991 arithmetic applications remain unfinished. The universal conditional implication
992 is checked in the \hyperref[book:x-construction-23]{conditional completion construction}.
993
994 \paragraph{Derived comparison bounds.}\phantomsection\label{book:x-construction-16}
995 For a finite group $\Gamma$ whose order is a unit in a commutative local
996 coefficient ring $R$, any prescribed equivariant residual isomorphism lifts to
997 an integral isomorphism. Lift its matrix to $A$ and define
998 \[
999 P=|\Gamma|^{-1}\sum_{g\in\Gamma}\rho(g)A\tau(g^{-1}).
1000 \]
1001 Reindexing proves equivariance, and reduction recovers the prescribed matrix.
1002 Its determinant is a unit. Complete local coefficients with finite quotients,
1003 occupied compatible finite conditions and this residual type therefore give
1004 actual integral completion with detector depth one. A fixed continuous map
1005 $G\to\Gamma$ permits pullback to infinite source groups. The finite-level
1006 representations must factor through the same map, and the residual type is
1007 imposed on their $\Gamma$-actions. No uniform determinant bound or augmented
1008 certificate occupancy is assumed in this sector.
1009
1010 For a second sector let $R$ be a DVR with uniformizer $\pi$, fraction field $K$
1011 and matrix rank $n$. If a fixed template $\tau$ has full $K$-linear action span,
1012 finite generation and denominator clearing give a fixed $c$ such that
1013 \[
1014 \pi^c M_n(R)\subseteq\operatorname{span}_R\{\tau(g):g\in G\}.
1015 \]
1016 Normalize a field comparison to an integral $P$ with a unit entry. The displayed
1017 span constructs an integral $B$ with $BP=\pi^cI$, so
1018 \[
1019 \det P\mid\pi^{cn},\qquad \det P\not\equiv0\pmod{\pi^{cn+1}}.
1020 \]
1021 One $c$ works for all integral representations in the fixed field-isomorphism
1022 class. Jacobson density derives full span from actual irreducibility and a
1023 scalar commutant. The formalization states these hypotheses directly and does
1024 not assume the DVR fraction field is algebraically closed.
1025
1026 If at every precision there is an integral representation of this rational
1027 type satisfying the finite conditions, the derived bound supplies the
1028 simultaneous certificates of the \hyperref[book:x-construction-15]{fixed-depth comparison-certificate construction} and preserves the type after completion.
1029 The integral approximants are not required to be coherent, but their existence
1030 is a substantive premise. Arbitrary torsion nodes are not asserted to lift.
1031
1032 Over $\mathbb Z_3$, the actual average corrects
1033 $A=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right)$ to
1034 $P=\left(\begin{smallmatrix}1&-1/2\\0&1\end{smallmatrix}\right)$ for the
1035 involutions $\rho(g)=\left(\begin{smallmatrix}1&1\\0&-1\end{smallmatrix}\right)$
1036 and $\tau(g)=\operatorname{diag}(1,-1)$. It preserves the residual comparison
1037 and has determinant one. Pullback through the quadratic character of the
1038 actual $G_{\mathbb Q}$ gives continuous arithmetic examples. In contrast, the
1039 identity and $\operatorname{diag}(1,\mathrm{sign})$ over $\mathbb Z/4$ agree
1040 modulo two but are not integrally conjugate. Their group order is not a unit.
1041 These restricted results do not supply general arithmetic packet attachment,
1042 all finite-level existence statements, or cross-coefficient compatibility.
1043
1044 \section{Compatible carriers and finite Frobenius separation}
1045
1046 One useful completion mechanism is available when the desired packet already occurs as a semisimple summand of a known compatible carrier.
1047
1048 \begin{theorem}[Finite Frobenius separation]\label{px:9.1}
1049 Let $\mathscr W_1,\ldots,\mathscr W_r$ be pairwise nonisomorphic strictly
1050 compatible systems whose members are absolutely irreducible, with common
1051 algebraic unramified trace values $t_i(v)$ in a number field $E$.
1052 There are $r$ distinct permitted unramified places $v_1,\ldots,v_r$ for which
1053 \[
1054 C=(t_i(v_j))_{j,i}\in M_r(E),\qquad \det C\ne0.
1055 \]
1056 Every coefficient-field embedding $\sigma_\lambda:E\hookrightarrow E_\lambda$
1057 therefore sends $C$ to an invertible matrix. Its entries agree with the
1058 ordinary representation traces
1059 $\operatorname{Tr}(W_{i,\lambda}(\operatorname{Frob}_{v_j}))$
1060 when the selected places satisfy the unramified compatibility convention
1061 for that coefficient prime. In particular, places above the residue
1062 characteristic of $\lambda$ are excluded from this ordinary trace comparison.
1063 \end{theorem}
1064
1065 \begin{proof}
1066 Fix one coefficient prime. The classical independence of the characters of
1067 pairwise nonisomorphic absolutely irreducible representations and the density
1068 of unramified Frobenius conjugacy classes give independent restricted trace
1069 functions. Density here concerns the union of the conjugacy classes, not an
1070 unsupported assertion about a set of chosen representatives.
1071
1072 For $r$ independent functions, their evaluation linear forms span the
1073 $r$-dimensional coefficient dual: a proper span would leave a nonzero
1074 coefficient vector annihilated by every evaluation, contradicting independence.
1075 Choose a basis from the evaluations. Its $r$ distinct sample points give an
1076 invertible square matrix. The common algebraic traces put that matrix over
1077 $E$. An injective field embedding reflects the nonvanishing of its determinant.
1078 All further field embeddings preserve the same nonvanishing.
1079 \end{proof}
1080
1081 \paragraph{Formalization boundary.}
1082 Characteristic-zero independence is now Lean-checked for actual finite-dimensional
1083 irreducible representations of arbitrary monoids. Finiteness of the group and
1084 algebraic closedness of the field are not needed for this result. The proof
1085 uses the actual monoid algebra and Jacobson density to select constituent
1086 actions. Jointly continuous coordinate actions have continuous characters.
1087 Coverage in every open normal quotient of a compact totally disconnected group
1088 implies density of the conjugacy-saturated samples and hence the finite separator.
1089 General arithmetic Frobenius coverage remains unformalized. The \hyperref[book:x-construction-25]{system-isomorphism and finite-cyclotomic comparison} now proves
1090 the bridge from componentwise nonisomorphic systems to nonisomorphic members
1091 at the selected coefficient prime, under density on the required good-place
1092 overlaps. It also proves the complete restricted separator for a fixed finite
1093 cyclotomic Galois group over $\Q$, with arithmetic coverage derived from the
1094 proved Dirichlet theorem. The full arithmetic theorem remains partial. Selection
1095 is existential and gives no effective upper bound on the selected primes.
1096 A common algebraic matrix is still distinct from an ordinary unramified trace
1097 comparison at all coefficient primes simultaneously.
1098
1099 \paragraph{System isomorphism and good-place overlaps.}\phantomsection\label{book:x-construction-25}
1100 The system equivalence used here is componentwise representation isomorphism:
1101 \[
1102 \mathscr W_i\simeq\mathscr W_j
1103 \quad\Longleftrightarrow\quad
1104 \forall\lambda,\ W_{i,\lambda}\simeq W_{j,\lambda}.
1105 \]
1106 For finite-dimensional irreducible representations of any monoid over a
1107 characteristic-zero field, the new character-rigidity theorem proves that
1108 equality of characters is equivalent to an actual equivariant linear isomorphism.
1109 Neither a finite group nor an algebraically closed coefficient field is needed.
1110
1111 Suppose two members are isomorphic at $\lambda_0$. Injectivity of the common
1112 coefficient embedding gives $t_i(v)=t_j(v)$ at every place good for $\lambda_0$.
1113 At another coefficient prime $\lambda$, this equality compares actual member
1114 traces on the intersection of the two good-place sets. Conjugacy density of
1115 that intersection and continuity extend the equality to the whole group.
1116 Character rigidity then gives an actual isomorphism at $\lambda$.
1117 Thus the nonisomorphism of systems supplies the required nonisomorphism of
1118 members. Equality of optional labels or record fields is not used as a
1119 substitute for representation equivalence.
1120
1121 The generic separator now derives this bridge and permits any additional finite
1122 set of excluded places. Its coverage premise retains every finite deletion:
1123 for each finite excluded set and each open normal quotient, every quotient
1124 class contains a conjugate of an allowed sample. This implies density on each
1125 pair of cofinite good-place sets. No all-coefficient-prime common ordinary-trace
1126 domain is assumed.
1127
1128 \paragraph{Arithmetic coverage for a fixed cyclotomic extension.}\phantomsection\label{book:x-construction-25-cyclotomic}
1129 Let $n>0$ and let $L=\Q(\zeta_n)$ be a cyclotomic number field. The canonical
1130 isomorphism
1131 \[
1132 \operatorname{Gal}(L/\Q)\simeq(\mathbb Z/n\mathbb Z)^\times
1133 \]
1134 defines $\sigma_p$ by $\sigma_p(\zeta_n)=\zeta_n^p$ when $p\nmid n$.
1135 For every automorphism $\sigma$, finite set $B\subset\mathbb N$ and bound $b$,
1136 Lean proves that there is a rational prime $p>b$, with $p\notin B$ and
1137 $p\nmid n$, such that $\sigma_p=\sigma$. The prime-existence step uses the
1138 proved Dirichlet theorem in the pinned Mathlib dependency.
1139
1140 The arithmetic attachment is checked in this finite cyclotomic case. There is
1141 an actual maximal prime $\mathfrak P$ of $\mathcal O_L$ above $(p)$, its
1142 ramification index is one, and $\sigma_p$ belongs to its decomposition group.
1143 For every integral $x\in\mathcal O_L$,
1144 \[
1145 \overline{\sigma_p(x)}=\overline{x}^{\,p}
1146 \quad\text{in }\mathcal O_L/\mathfrak P.
1147 \]
1148 The residue identity is proved on all integral elements using
1149 $\mathcal O_L=\mathbb Z[\zeta_n]$. Existence of $\mathfrak P$ is obtained by
1150 lying over, rather than assumed. This specifies arithmetic Frobenius, with
1151 $p$-power residue action. The action and unramifiedness statements also hold
1152 for every maximal prime above the selected $p$.
1153
1154 Consequently, for pairwise componentwise nonisomorphic compatible irreducible
1155 representation families of this fixed finite Galois group, the common algebraic
1156 trace matrix can be selected at distinct rational primes outside any prescribed
1157 finite set, with nonzero determinant. Every coefficient embedding preserves its
1158 nonvanishing. Actual member trace comparisons retain that member's good-prime
1159 condition. No coverage or character-continuity hypothesis is added in this
1160 cyclotomic specialization: the prime coverage is proved, and the finite
1161 extension's Krull topology is discrete. A concrete conductor-four instance uses
1162 the actual field $\Q(\zeta_4)$.
1163
1164 This is a complete restricted arithmetic case of Claim 9.1. It does not establish
1165 coverage in arbitrary finite quotients of the absolute Galois group, nor the
1166 Hodge--Tate and Weil--Deligne comparisons of Claim 9.2. The source-claim ledger
1167 therefore remains seventeen checked and three partial.
1168
1169 \paragraph{Absolute Galois restriction and arithmetic witnesses.}\phantomsection\label{book:x-construction-26}
1170 Fix a cyclotomic number field $L=\Q(\zeta_n)$ with $n>0$ and an embedding
1171 $j:L\hookrightarrow\overline{\Q}$. The new restriction map
1172 \[
1173 q_L:G_{\Q}\longrightarrow\operatorname{Gal}(L/\Q),\qquad
1174 j(q_L(\gamma)x)=\gamma(j(x)),
1175 \]
1176 is an actual continuous surjective homomorphism with open kernel. Surjectivity
1177 is derived by extending automorphisms to the algebraic closure. Pullback along
1178 a surjective homomorphism preserves and reflects equivariant linear
1179 isomorphisms, invariant subspaces, and irreducibility. These assertions keep
1180 the underlying linear maps and submodules and do not assume a finite acting
1181 group. In particular, the equivalence relation for systems is preserved and
1182 reflected componentwise.
1183
1184 The arithmetic witnesses use the integral closure
1185 $\mathcal A$ of $\mathbb Z$ in $\overline{\Q}$. For each rational prime $p$,
1186 Lean constructs a maximal ideal $\mathfrak Q$ of $\mathcal A$ above $(p)$ and
1187 an actual element $\gamma_p\in G_{\Q}$ such that
1188 \[
1189 \gamma_p\in\operatorname{Stab}_{G_{\Q}}(\mathfrak Q),\qquad
1190 \overline{\gamma_p(a)}=\overline a^{\,p}
1191 \quad(a\in\mathcal A).
1192 \]
1193 The existence argument applies Mathlib's proved profinite stabilizer-surjectivity
1194 theorem to this actual invariant ring. The residue $p$-power map is proved
1195 bijective by taking $p$-th roots in $\overline{\Q}$ and showing that they
1196 remain integral when their $p$-th powers are integral. This constructs an
1197 arithmetic Frobenius witness in the prime-ideal decomposition group. It does
1198 not assert that an arbitrary global lift belongs to that group.
1199
1200 When $p\nmid n$, the comparison with the finite cyclotomic sample is proved:
1201 \[
1202 q_L(\gamma_p)=\sigma_p,
1203 \qquad \sigma_p(\zeta_n)=\zeta_n^p.
1204 \]
1205 Reduction distinguishes $n$-th roots of unity at such a prime. Indeed, if
1206 $x^n=y^n=1$ and their reductions agree, the factorization of $x^n-y^n$ gives
1207 \[
1208 (x-y)\sum_{i=0}^{n-1}x^i y^{n-1-i}=0.
1209 \]
1210 The second factor reduces to $n\overline y^{\,n-1}\ne0$, so the domain
1211 property gives $x=y$. This proves both Frobenius recognition on the
1212 cyclotomic generator and triviality of its inertia action. Consequently,
1213 every representation pulled back through $q_L$ is unramified there.
1214
1215 The valuation formulation is checked separately. For any valuation subring
1216 $A\subset\overline{\Q}$ with residue characteristic $p\nmid n$, its actual
1217 residue-action kernel fixes every $n$-th root of unity. A supplied element of
1218 its decomposition subgroup with $p$-power residue action restricts to
1219 $\sigma_p$. These statements use Mathlib's valuation inertia and decomposition
1220 subgroups. No identification of the valuation and integral-closure prime
1221 models is assumed in the formal comparison.
1222
1223 For a compatible family $\rho_{i,\lambda}$ of representations of the fixed
1224 finite group, set $V_{i,\lambda}=\rho_{i,\lambda}\circ q_L$. Suppose the
1225 actual absolute-Galois members are irreducible and the systems are pairwise
1226 componentwise nonisomorphic. The finite prime separator now yields distinct
1227 permitted rational primes $p_j$, actual prime ideals $\mathfrak Q_j$ and
1228 arithmetic Frobenius witnesses $\gamma_j$ as above, outside any prescribed
1229 finite set, such that the common algebraic trace matrix has nonzero
1230 determinant. Every coefficient embedding preserves this nonvanishing, and
1231 \[
1232 \iota_\lambda(t_i(p_j))=
1233 \operatorname{tr}(V_{i,\lambda}(\gamma_j))
1234 \]
1235 whenever $p_j$ is good for that coefficient member. The operator and trace
1236 values agree for every global lift with the same cyclotomic restriction.
1237 Neither Frobenius-witness existence nor quotient coverage is a supplied
1238 hypothesis in this restricted arithmetic theorem. The common cyclotomic
1239 factorization and the compatible trace data remain explicit hypotheses.
1240
1241 This completes the passage to actual absolute-Galois Frobenius witnesses for
1242 the fixed cyclotomic class. It does not establish prime coverage for arbitrary
1243 finite Galois extensions. Claim 9.1 therefore remains partial, and the
1244 source ledger remains seventeen checked and three partial.
1245
1246 The boundaries are formalized as well. Pullback along a nonsurjective
1247 homomorphism can make inequivalent irreducible representations isomorphic.
1248 Samples can cover one quotient while missing an open quotient of the full
1249 group. Finally, in $\mathbb Z_2$, the distinct square roots $1$ and $-1$ have
1250 the same residue, so the condition that the root order be a unit cannot be
1251 discarded.
1252
1253 \paragraph{General finite-field Frobenius comparison.}\phantomsection\label{book:x-construction-27}
1254 Let $L/\Q$ now be any finite normal number field, with a chosen embedding
1255 $j:L\hookrightarrow\overline{\Q}$. Write $\mathcal A$ for the integral
1256 closure of $\mathbb Z$ in $\overline{\Q}$. The embedding restricts to an
1257 injective map $\mathcal O_L\to\mathcal A$ which intertwines the actual
1258 Galois actions. If $\mathfrak Q\subset\mathcal A$ is maximal above $(p)$,
1259 its contraction $\mathfrak P\subset\mathcal O_L$ is a nonzero maximal
1260 ideal above $(p)$, and the induced residue map is injective.
1261
1262 Restriction carries the actual decomposition group at $\mathfrak Q$ into
1263 that at $\mathfrak P$, carries ideal inertia into ideal inertia, and
1264 preserves the arithmetic $p$-power residue action. Thus the absolute
1265 Frobenius constructed in the \hyperref[book:x-construction-26]{absolute-Galois restriction construction} gives a simultaneous finite Frobenius
1266 at the contracted prime. This assertion applies to arbitrary finite normal
1267 number fields and does not require a cyclotomic generator.
1268
1269 The exceptional primes are controlled by the actual field discriminant:
1270 \[
1271 S_L=\{p\text{ rational prime}:p\mid\operatorname{disc}(L)\}.
1272 \]
1273 This set is finite. For $p\notin S_L$, every prime of $\mathcal O_L$
1274 above $(p)$ is unramified. Lean proves that the actual inertia cardinality
1275 is the ramification index. It follows that inertia is trivial and the
1276 arithmetic Frobenius at a fixed finite prime is unique as a field
1277 automorphism. Neither trivial inertia nor uniqueness is assumed in place
1278 of the arithmetic unramifiedness condition.
1279
1280 The choice of absolute prime and Frobenius lift is also controlled. Let
1281 $(\mathfrak Q_u,\gamma_u)$ and $(\mathfrak Q_v,\gamma_v)$ be any two
1282 actual arithmetic witnesses at the same rational prime. Transitivity on
1283 primes of $\mathcal A$ above $(p)$ gives $a\in G_{\Q}$ with
1284 \[
1285 \mathfrak Q_v=a\mathfrak Q_u,\qquad
1286 \gamma_v^{-1}a\gamma_u a^{-1}\in I_{\mathfrak Q_v}.
1287 \]
1288 Consequently, any representation trivial on $I_{\mathfrak Q_v}$ has the
1289 same trace on the two witnesses. For representations factoring through
1290 $L$, triviality on this actual absolute inertia is derived whenever
1291 $p\notin S_L$. The restrictions of all absolute witnesses at such a prime
1292 therefore form a single conjugacy class. This conclusion requires only
1293 the indicated finite factorization and the discriminant exclusion.
1294
1295 There is a final compatibility between embeddings. For a normal subfield
1296 $L\subset\overline{\Q}$, restriction defined through a chosen embedding
1297 is conjugate to canonical restriction by one fixed automorphism of $L$.
1298 This identifies their conjugacy classes and lets the arithmetic comparison
1299 apply directly to the fixed fields of open normal subgroups of $G_{\Q}$.
1300 Those fixed fields are proved to be finite Galois number fields, with the
1301 original open normal subgroup as the kernel of restriction.
1302
1303 The remaining prime-existence obligation now has a precise formulation.
1304 For every finite Galois subfield $L$, every finite set $B$ of rational
1305 primes, and every $\sigma\in\operatorname{Gal}(L/\Q)$, require a prime
1306 $p\notin B\cup S_L$ and an actual absolute arithmetic witness $\gamma_p$
1307 such that
1308 \[
1309 q_L(\gamma_p)\sim\sigma.
1310 \]
1311 Lean proves that this assertion is equivalent to the cofinite quotient
1312 coverage required by the general separator, for any fixed choice of actual
1313 Frobenius witnesses. The equivalence derives independence from the witness
1314 choices. It does not supply the displayed prime-existence assertion.
1315 Arbitrary finite exclusions absorb $S_L$, and the resulting conditional
1316 density theorem preserves the separate good-prime sets of coefficient
1317 members. General prime coverage remains unproved, so Claim 9.1 remains
1318 partial. The source ledger is still seventeen checked and three partial.
1319 This new arithmetic interface has base $\Q$. For the source's general-base
1320 instances involving $G_{F,S}$, the analogous actual-prime and norm-power
1321 Frobenius attachment and coverage over $F$, or a proved transfer to the
1322 rational-base result, also remain necessary.
1323
1324 \paragraph{Finite deletion can destroy density.}
1325 In the actual discrete group $C_2=\{1,a\}$, set $s(0)=a$ and $s(m+1)=1$.
1326 The original samples are surjective and satisfy quotient coverage. Removing
1327 index zero leaves only the identity, so both density and quotient coverage fail.
1328 The actual rational sign and trivial characters agree on the remaining samples
1329 but differ globally. This checked example explains why ordinary coverage alone
1330 cannot justify deleting the bad places in the system comparison.
1331
1332 \begin{theorem}[Compatible-carrier summand completion]\label{px:9.2}
1333 Suppose a semisimple strictly compatible carrier decomposes as
1334 \[
1335 \mathscr W
1336 \cong
1337 \bigoplus_{i=1}^{r}
1338 \mathscr W_i^{\oplus c_i},
1339 \]
1340 with the \(\mathscr W_i\) as above. At one coefficient prime \(\lambda_0\), suppose a semisimple summand has the form
1341 \[
1342 V_{\lambda_0}
1343 \cong
1344 \bigoplus_{i=1}^{r}
1345 W_{i,\lambda_0}^{\oplus m_i},
1346 \qquad
1347 0\le m_i\le c_i.
1348 \]
1349 Then
1350 \[
1351 \boxed{
1352 V_\lambda
1353 =
1354 \bigoplus_{i=1}^{r}
1355 W_{i,\lambda}^{\oplus m_i}
1356 }
1357 \]
1358 defines a strictly compatible summand at every coefficient prime. The vector \((m_i)\) is uniquely recoverable from finitely many Frobenius traces supplied by the separation theorem.
1359 \end{theorem}
1360
1361 \begin{proof}
1362 Use the same multiplicities in every member of the compatible carrier. Direct sums preserve strict compatibility, and \(m_i\le c_i\) makes \(V_\lambda\) a summand of \(W_\lambda\). At the separating places, the target trace vector is \(C\bm m\). Full column rank makes \(\bm m\) the unique solution.
1363 \end{proof}
1364
1365 \paragraph{Recovery and realization are different steps.}
1366 For a certified square separator the coefficient vector is $C^{-1}t$.
1367 This is a valid carrier multiplicity vector only when every entry is a
1368 nonnegative integer and satisfies its capacity bound $m_i\le c_i$.
1369 Those tests and uniqueness of natural multiplicities in characteristic zero
1370 are separately Lean-checked, as is transport through a field embedding.
1371 Reduction modulo a residue characteristic is not a field embedding and may
1372 lose rank. The representation construction and common-polynomial part are now
1373 Lean-checked as described below. The full strictly compatible arithmetic
1374 statement, including its local conditions, remains partially formalized.
1375
1376 \paragraph{Scope of the supplied-carrier hypothesis.}
1377 Claim 9.2 supplies the compatible carrier, its decomposition and the compatible
1378 constituent systems. Constructing unknown such objects is not required by that
1379 conditional theorem. The remaining formal obligation is that finite sums preserve
1380 the intended actual local arithmetic structures, together with the arithmetic
1381 separator input. The algebraic monodromy results below do not by themselves
1382 identify attached Weil--Deligne representations or Hodge--Tate comparison data.
1383
1384 \paragraph{Explicit summands inside a supplied decomposition.}
1385 Let $K$ be a field, let $G$ be a monoid, and let
1386 $\rho_i:G\to\operatorname{End}_K(W_i)$ be actual representations on
1387 finite-dimensional spaces, indexed by a finite set $I$. For natural numbers
1388 $m_i\le c_i$, set
1389 \[
1390 U_m=\prod_{i\in I}\prod_{k<m_i}W_i,
1391 \qquad U_c=\prod_{i\in I}\prod_{k<c_i}W_i.
1392 \]
1393 These finite products realize the corresponding finite direct sums. The
1394 representation on $U_m$ acts componentwise. Define $j:U_m\to U_c$ by retaining
1395 the first $m_i$ copies and filling every remaining coordinate with zero.
1396 Define $r:U_c\to U_m$ by restriction to the selected copies. Lean proves
1397 \[
1398 rj=1_{U_m},\qquad
1399 j\rho_m(g)=\rho_c(g)j,\qquad
1400 r\rho_c(g)=\rho_m(g)r.
1401 \]
1402 The image of $j$ is exactly the subspace whose unused coordinates vanish.
1403 Consequently $jr$ is an equivariant idempotent. A supplied equivariant
1404 isomorphism $D:W\xrightarrow{\sim}U_c$ gives the split maps
1405 $D^{-1}j$ and $rD$ inside the original carrier. The decomposition $D$ is an
1406 input. These statements do not construct a decomposition of an unknown
1407 arithmetic carrier.
1408
1409 The same formalization proves, for each $g\in G$,
1410 \[
1411 \det\bigl(XI-\rho_m(g)\bigr)
1412 =\prod_{i\in I}\det\bigl(XI-\rho_i(g)\bigr)^{m_i},
1413 \qquad
1414 \operatorname{Tr}\bigl(\rho_m(g)\bigr)
1415 =\sum_{i\in I}(m_i:K)\operatorname{Tr}\bigl(\rho_i(g)\bigr).
1416 \]
1417 Constituents may have different dimensions. Zero multiplicities, zero-dimensional
1418 constituents, and the empty index set are included. If at a permitted sample
1419 $g$ the constituent polynomials are the images of $P_{i,g}\in E[X]$ under a
1420 specified map $E\to K$, the summand polynomial is the image of
1421 $\prod_iP_{i,g}^{m_i}$. Applying this independently at each coefficient field
1422 preserves a supplied common polynomial family. This does not establish the
1423 Hodge--Tate or Weil--Deligne conditions in strict compatibility.
1424
1425 Joint continuity of the constituent actions implies joint continuity of the
1426 constructed action. The inclusion and retraction are continuous for the
1427 product topologies, and triviality on a supplied subgroup is preserved.
1428 Neither continuity nor triviality is inferred for a carrier whose corresponding
1429 hypothesis has not been supplied. The maps transported by $D$ are proved
1430 algebraically. Their topological interpretation additionally requires the
1431 appropriate continuity of $D$ and its inverse.
1432
1433 For the three-character example below, the construction produces an actual
1434 three-dimensional summand inside the carrier of dimension seven. At the sample
1435 $(0,1)$ its characteristic polynomial is $(X-1)^2(X+1)$. A separate checked
1436 counterexample uses the coordinate inclusion $\mathbf Q\to\mathbf Q^2$, its
1437 coordinate retraction, and the swap involution: the split law holds, but
1438 compression sends the swap to zero and therefore fails to preserve its square.
1439 Thus selecting whole constituent copies, with the proved equivariance, is
1440 essential to this construction.
1441
1442 \paragraph{Algebraic monodromy data on the selected copies.}
1443 Fix a field $K$ and a nonzero scalar $q\in K^\times$. On each constituent
1444 $W_i$, supply an automorphism $F_i$ and a nilpotent endomorphism $N_i$ with
1445 $F_iN_iF_i^{-1}=qN_i$. The scalar $q$ is common to this finite family.
1446 The componentwise operators $F_m,N_m$ on $U_m$ satisfy the same relation.
1447 $F_m$ is invertible and $N_m$ is nilpotent. The split maps constructed above
1448 intertwine both operators. The proof first identifies the independently defined
1449 kernel through an equivariant linear isomorphism
1450 \[
1451 \ker N_m\simeq\prod_{i\in I}\prod_{k<m_i}\ker N_i.
1452 \]
1453 The relation, with $q\ne0$, proves that both $F_i$ and its inverse preserve
1454 $\ker N_i$. Thus $F_i|_{\ker N_i}$ is an actual automorphism, and Lean proves
1455 \[
1456 \det(XI-F_m|_{\ker N_m})
1457 =\prod_{i\in I}\det(XI-F_i|_{\ker N_i})^{m_i}.
1458 \]
1459 The corresponding kernel dimensions and traces are additive with multiplicity.
1460 Common constituent kernel polynomials, when supplied through a coefficient-ring
1461 map, give the mapped product polynomial for the summand. Whole-space Frobenius
1462 polynomials are not substituted for these kernel polynomials.
1463
1464 The exact special chain has basis $e_0,\ldots,e_{n-1}$ and operators
1465 \[
1466 Ne_0=0,\qquad Ne_j=e_{j-1}\ (j>0),\qquad Fe_j=aq^{-j}e_j,
1467 \qquad a,q\in K^\times.
1468 \]
1469 Lean proves $N^n=0$, and for $n>0$ also $N^{n-1}\ne0$ and
1470 $\ker N=Ke_0$. Consequently its kernel polynomial is $X-a$, whereas its
1471 whole-space polynomial is $\prod_{j=0}^{n-1}(X-aq^{-j})$.
1472 The zero-length chain is included as a zero-dimensional space. The assertion
1473 $\ker N=Ke_0$ is made only for positive length.
1474
1475 For $n>1$, replacing $N$ by zero retains exactly the same $F$ and the same
1476 whole-space characteristic polynomial, while changing the degree of the kernel
1477 polynomial from one to $n$. Both pairs still satisfy the algebraic monodromy
1478 relation. This Lean-checked example shows that whole Frobenius data alone do
1479 not determine the monodromy kernel polynomial. It is not asserted to be a
1480 counterexample among the intended strictly compatible arithmetic systems.
1481
1482 These statements concern supplied algebraic pairs. No Weil-group or inertia
1483 action, Hodge--Tate object, arithmetic comparison, or realization of the pair
1484 from a Galois representation is constructed here. The polynomial convention is
1485 $\det(XI-F|_{\ker N})$. No identification with an inertia-dependent local
1486 Euler factor is asserted. Claim 9.2 remains partial at its full arithmetic scope.
1487
1488
1489 \paragraph{Checked group, inertia and monodromy finite sums.}\phantomsection\label{book:x-construction-12}
1490 Let $K$ be a field, $G$ a group, and $\nu:G\to K^\times$ a character.
1491 The new datum consists of an actual representation $r$ and nilpotent $N$ with
1492 $r(g)N=\nu(g)Nr(g)$ for every $g$. For a supplied subgroup $H$, define
1493 \[
1494 E(D,H)=\ker N\cap V^H.
1495 \]
1496 This is the intersection of independently defined kernel and actual invariant
1497 subspaces. For normal $H$, the restricted whole-group representation and its
1498 inverse automorphisms are constructed. A change from $\varphi$ to $\varphi h$,
1499 with $h\in H$, leaves the restricted operator itself unchanged.
1500
1501 For a finite family of finite-dimensional constituents and natural multiplicities,
1502 the actual local space of the constructed sum is linearly equivalent to the sum of the constituent local spaces, equivariantly
1503 for every group element. Its characteristic polynomials multiply, its dimensions
1504 and traces add, and maps intertwining both the group and $N$ restrict to the
1505 local spaces. The explicit bounded-copy inclusion and retraction still split
1506 there. Finite inertia image and an open inertia kernel are preserved.
1507
1508 Writing $Q_D(T)$ for the reversed local characteristic polynomial, Lean proves
1509 \[
1510 Q_D(T)=\det(1-T r(\varphi)\mid E(D,H)),\qquad Q_D(0)=1,
1511 \qquad
1512 Q_{\bigoplus_iD_i^{\oplus m_i}}(T)=\prod_iQ_{D_i}(T)^{m_i}.
1513 \]
1514 The abstract formulas do not need characteristic zero. Normality and finite
1515 dimension appear explicitly where used. Arithmetic identification of $G,H,\nu$
1516 and $\varphi$ remains separate. In the geometric-Frobenius convention,
1517 $\nu(\varphi)$ is the inverse residue cardinality. It is this unit, rather than
1518 the residue cardinality, that enters the earlier special-chain parameter.
1519
1520 An explicit action of $C_2\times\mathbb Z$ has $\nu(\varphi)=1/3$,
1521 $F=\operatorname{diag}(2,6,18)$ and $Ne_1=e_0$, $Ne_2=e_1$, $Ne_0=0$.
1522 Trivial inertia gives local dimension one and denominator $1-2T$. Scalar sign
1523 inertia gives dimension zero and denominator one. The entire $F$ and $N$ are
1524 equal in these two examples, and $N^2\ne0$. Thus inertia cannot be omitted.
1525 Conversely, unramified chains of lengths one and three have equal Euler
1526 denominators while only the first has $N=0$. Euler factors therefore do not
1527 identify complete monodromy data.
1528
1529 The remaining arithmetic comparison is
1530 $\operatorname{WD}(\bigoplus_i V_i^{\oplus m_i})\cong
1531 \bigoplus_i\operatorname{WD}(V_i)^{\oplus m_i}$ for the actual attached functor,
1532 intertwining the Weil action and monodromy, together with the intended coefficient
1533 and Hodge--Tate comparisons. These are not supplied by the abstract datum.
1534 Claim 9.2 remains partial at its full arithmetic scope.
1535
1536 Recovered multiplicities determine the semisimple isomorphism type relative
1537 to the specified constituents, not a canonical embedding or projector inside
1538 a repeated isotypic component. For example, the two projectors
1539 $\operatorname{diag}(1,0)$ and $\operatorname{diag}(0,1)$ on a two-dimensional
1540 trivial representation are distinct equivariant idempotents with trace one.
1541
1542 \begin{figure}[H]
1543 \centering
1544 \includegraphics[width=0.72\linewidth]{14_frobenius_separator_matrix.pdf}
1545 \caption{A finite set of trace evaluations separates three compatible constituents and recovers their multiplicities.}
1546 \end{figure}
1547
1548 \begin{numericalcertificate}[Multiplicity recovery]\label{px:9.3}
1549 The original companion matrix was not retrieved or rerun. A new exact
1550 realization uses the trivial character and two independent sign characters
1551 of $(\mathbf Z/2\mathbf Z)^2$, evaluated at $(0,0),(1,0),(0,1)$:
1552 \[
1553 C=\begin{pmatrix}1&1&1\\1&-1&1\\1&1&-1\end{pmatrix},
1554 \qquad \det C=4,
1555 \qquad C\begin{pmatrix}2\\0\\1\end{pmatrix}
1556 =\begin{pmatrix}3\\3\\1\end{pmatrix}.
1557 \]
1558 Lean checks that these are the traces of actual one-dimensional
1559 representations, recovers $(2,0,1)$ uniquely, rejects a target whose unique
1560 solution is $(1/2,0,0)$, and rejects $(4,0,1)$ under capacities $(3,2,2)$.
1561 The separator becomes singular modulo two. These are finite-image
1562 representation checks, not fabricated Frobenius data for an arithmetic carrier.
1563 \end{numericalcertificate}
1564
1565 The theorem is substantial only when a suitable compatible carrier and its irreducible compatible constituents are already known. It does not assert that every geometric representation embeds into such a carrier.
1566
1567
1568 \paragraph{Finite-exponential reconstruction and a cubic inverse.}\phantomsection\label{book:x-construction-13}
1569 Let $K$ be a characteristic-zero field and let $(r,N)$ be supplied group data
1570 with nilpotent $N$ and $r(g)N=\nu(g)Nr(g)$. For a supplied scalar map satisfying
1571 \[
1572 t(gh)=t(g)+\nu(g)t(h),
1573 \]
1574 the formalization constructs
1575 \[
1576 \rho(g)=\exp(t(g)N)r(g),\qquad
1577 \exp(aN)=\sum_{j=0}^{d-1}\frac{a^j}{j!}N^j\quad(N^d=0).
1578 \]
1579 Lean proves the representation laws, actual finite-copy and split-map
1580 compatibility, and joint continuity from continuity of $N$, $r$ and $t$ with
1581 the stated continuous vector-space operations. The monodromy fixed kernel
1582 intersected with subgroup invariants is unchanged by this twist. For normal
1583 inertia, its restricted action and finite-dimensional Euler denominator agree.
1584 Twisting again by $-t$ recovers the datum with $N$ still supplied.
1585
1586 The \hyperref[book:x-construction-13]{finite-exponential reconstruction} also established an extracted inverse on the explicit class $N^3=0$:
1587 \[
1588 \log_2 U=(U-I)-\tfrac12(U-I)^2,\qquad
1589 a^{-1}\log_2(\exp(aN))=N\quad(a\ne0).
1590 \]
1591 Both exponential/logarithmic inverse identities are checked on the cubic
1592 nilpotent and unipotent loci. If a supplied common sample $u$ has
1593 $r_D(u)=r_E(u)=I$ and $t(u)\ne0$, an intertwiner of the reconstructed cubic
1594 actions recovers both original group equivariance and monodromy equivariance.
1595 The general nilpotence exponential theorem is not restricted to this cubic
1596 class, but the extracted inverse in the \hyperref[book:x-construction-13]{finite-exponential reconstruction} was. The \hyperref[book:x-construction-20]{finite logarithmic recovery argument} below removes
1597 that restriction by using the full finite logarithm.
1598
1599 The rational affine-group example has $u=(1,1)$, $d=(0,1/3)$ and
1600 \[
1601 \rho(u)=\begin{pmatrix}1&1&1/2\\0&1&1\\0&0&1\end{pmatrix},
1602 \qquad \rho(d)=\operatorname{diag}(1,3,9).
1603 \]
1604 Reversing the factor order or dropping the quadratic term gives checked
1605 failures. For the length-four chain, the quadratic logarithm has erroneous
1606 $e_3$-to-$e_0$ coefficient $-1/3$, so its cubic restriction is substantive.
1607 A zero-parameter sample also fails to recover $N$.
1608
1609 No arithmetic group, tame cocycle or required sample is constructed by these
1610 statements. The attached comparison for every intended representation,
1611 coefficient comparisons and Hodge--Tate/period data remain separate. Finite
1612 inertia image and an open inertia kernel of $r$ are not asserted to persist
1613 under this twist to $\rho$. Claim 9.2 remains partial.
1614
1615 \section{Finite spectral occupancy}
1616
1617 System completion produces arithmetic members. It does not prove that a desired packet occurs in a global carrier. In a fixed finite-dimensional semisimple carrier, however, occupancy is an exact projector question.
1618
1619 Let \(E\) be a field of characteristic zero and let \(T_1,\ldots,T_N\) be commuting operators on a finite-dimensional \(E\)-vector space \(A\), each diagonalizable over \(E\). Thus the selected spectra split over the coefficient field. Let \(a_i\in E\) be a selected target scalar for \(T_i\), possibly absent from its spectrum. Define
1620 \[
1621 e_i
1622 =
1623 \prod_{\mu\in\Spec(T_i)\setminus\{a_i\}}
1624 \frac{T_i-\mu I}{a_i-\mu},
1625 \qquad
1626 e_T=\prod_{i=1}^{N}e_i,
1627 \]
1628 with \(e_i=0\) if \(a_i\) is absent.
1629
1630 \begin{theorem}[Exact finite occupancy trace]\label{px:10.1}
1631 The operator \(e_T\) is the projector onto the joint eigenspace
1632 \[
1633 A_T
1634 =
1635 \{v:T_iv=a_iv\text{ for every }i\}.
1636 \]
1637 Moreover,
1638 \[
1639 \boxed{
1640 \Tr(e_T)=\rank(e_T)=\dim A_T\in\Z_{\ge0}.
1641 }
1642 \]
1643 The trace is identified with its unique nonnegative integer preimage under \(\Z\hookrightarrow E\). Thus \(\Tr(e_T)>0\) refers to that integer, not to an ordering of an arbitrary field \(E\). The finite packet is occupied exactly when this integer is positive. In positive characteristic the field-valued trace can vanish for a nonzero projector. The rank test, not a positive field trace, must then be used.
1644 \end{theorem}
1645
1646 \begin{proof}
1647 For each operator, its finite set of actual eigenvalues is used without
1648 multiplicity. The polynomial
1649 \[
1650 p_{i,a}(X)=\prod_{\mu\in\Spec(T_i)\setminus\{a\}}
1651 (a-\mu)^{-1}(X-\mu)
1652 \]
1653 is used when $a$ occurs, and the zero polynomial otherwise. For an eigenvector
1654 $T_i v=bv$, evaluation gives
1655 \[
1656 p_{i,a}(T_i)v=\begin{cases}v&b=a,\\0&b\ne a.\end{cases}
1657 \]
1658 Because the eigenspaces span $A$, this proves that $e_i=p_{i,a_i}(T_i)$ maps
1659 all of $A$ into the selected eigenspace and fixes that eigenspace pointwise.
1660 It therefore proves the individual projector and image assertions, including
1661 an absent target.
1662
1663 Polynomials in commuting operators commute. If projections $P,Q$ onto
1664 $U,W$ commute, then $PQ$ maps into both $U$ and $W$, and fixes every vector
1665 in $U\cap W$. Induction proves that the actual ordered product $e_T$ is a
1666 projection onto $A_T$. Commutation also makes the result independent of the
1667 ordering. An empty list of conditions gives the identity.
1668
1669 For a projection onto a subspace, the direct sum of its image and kernel
1670 identifies it with $I\oplus0$. Thus its trace in $E$ is the natural dimension
1671 of its image cast into $E$. In characteristic zero this cast is injective,
1672 so there is a unique natural integer represented by the trace. That integer
1673 is positive exactly when the joint eigenspace contains a nonzero vector.
1674 \end{proof}
1675
1676 \paragraph{Naturality and finite hypotheses.}
1677 If $F T_i=U_i F$ and the source operators split, then
1678 $F e_{T,a}=e_{U,a}F$. This follows first on source eigenvectors and then on
1679 their span. In particular, a change of basis conjugates the constructed
1680 projector and preserves its trace. Adding conditions decreases the actual
1681 joint eigenspace and cannot increase its dimension. These statements do not
1682 assume an orthonormal basis or a positive definite inner product.
1683
1684 \paragraph{A specified finite realization.}
1685 On $\Q^4$, take the diagonal operators with diagonal lists
1686 \[
1687 (1,1,1,0),\quad(2,2,0,0),\quad(3,0,0,0),\quad(0,4,4,4)
1688 \]
1689 and target scalars $(1,2,3,4)$. All four targets occur individually. Imposing
1690 these conditions successively gives actual projector ranks $3,2,1,0$.
1691 The last packet is empty despite individual feasibility. The formal code
1692 checks these operators, projector formulas, traces and dimensions. This is
1693 a newly specified realization, not a claim to have recovered the original
1694 companion implementation.
1695
1696 \paragraph{Why the hypotheses cannot be omitted.}
1697 For
1698 \[
1699 P=\begin{pmatrix}1&0\\0&0\end{pmatrix},\qquad
1700 Q=\tfrac12\begin{pmatrix}1&1\\1&1\end{pmatrix},
1701 \]
1702 each operator is idempotent, but $PQ$ is not idempotent and has trace $1/2$.
1703 For the Jordan block $J=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right)$,
1704 the singleton-spectrum Lagrange polynomial is $1$, so the formula produces
1705 the identity although the eigenspace at $1$ is only a line. Both failures
1706 are exact formal counterexamples to dropping the corresponding hypotheses,
1707 not counterexamples to the theorem with those hypotheses retained.
1708
1709
1710 \begin{figure}[H]
1711 \centering
1712 \includegraphics[width=0.77\linewidth]{15_finite_occupancy_ranks.pdf}
1713 \caption{A consistent sequence of finite conditions narrows the carrier from ranks \(3\) to \(2\) to \(1\). One inconsistent condition forces the joint projector to zero.}
1714 \end{figure}
1715
1716 \begin{conjecture}[Universal occupancy]\label{px:10.2}
1717 For every admissible finite arithmetic packet in the intended global class, there exists a finite-dimensional carrier in which the associated joint projector has positive trace.
1718 \end{conjecture}
1719
1720 This conjecture is not a consequence of the projector formula. The formula measures occupancy exactly once the carrier is fixed. It cannot force the trace to be positive.
1721
1722 \section{A conditional system-completion criterion}
1723
1724 The preceding results can be assembled without promoting their missing hypotheses to theorems.
1725
1726 \begin{theorem}[Residual-system completion criterion]\label{px:11.1}
1727 Fix an admissible arithmetic class. Suppose:
1728 \begin{enumerate}
1729 \item every object has a unique residual root in an exhaustive residual moduli space;
1730 \item a common algebraic spine is defined for the desired system;
1731 \item every coefficient-prime residual companion exists;
1732 \item every companion forest has nonempty finite levels, finite branching, and inverse-limit closed local conditions;
1733 \item the required horizontal transports preserve the common spine and the selected local deformation conditions.
1734 \end{enumerate}
1735 Then the desired strictly compatible arithmetic system exists. If, in addition, the system is a summand of a known compatible carrier, the summand is recovered at every coefficient prime by finitely many Frobenius traces.
1736 \end{theorem}
1737
1738 \begin{proof}
1739 The first four hypotheses give the system by adelic finite-depth completion. The transport hypothesis identifies any roots that are meant to be generated horizontally without changing the prescribed spine. The final assertion is the compatible-carrier summand theorem.
1740 \end{proof}
1741
1742 \begin{corollary}[Exact location of the remaining existence problem]\label{px:11.2}
1743 Inverse-limit reconstruction alone is not a nonemptiness theorem. The existence requirements must retain both residual companions and liftability through every finite depth:
1744 \[
1745 \boxed{
1746 \begin{aligned}
1747 \text{companion existence: }&X_{\lambda,1}(\Compat)\ne\varnothing
1748 \text{ for every }\lambda;\\
1749 \text{finite-depth liftability: }&X_{\lambda,m}(\Compat)\ne\varnothing
1750 \text{ for every }\lambda,m\ge2;\\
1751 \text{finite occupancy: }&\Tr(e_T)>0
1752 \text{ for every required global packet.}
1753 \end{aligned}}
1754 \]
1755 Formal reconstruction does not create a missing residual root, repair an empty higher level, or force global occupancy. Nonempty finite levels with finite branching supply a branch, after which inverse-limit closure reconstructs an admissible object.
1756 \end{corollary}
1757
1758
1759 \paragraph{An occupied node can have no child.}
1760 The actual order-two representation with generator
1761 \[
1762 A=\begin{pmatrix}1&2\\2&3\end{pmatrix}\pmod4
1763 \]
1764 satisfies $A^2=I$ and $\det(XI-A)=X^2-1$. It has no lift modulo $8$ with
1765 the same characteristic polynomial. Indeed, every lift has entries congruent
1766 to $1,2,2,3$ modulo $4$. Trace zero then forces its determinant to be $3$
1767 modulo $8$, whereas $X^2-1$ requires determinant $-1=7$ modulo $8$.
1768 Both the occupied node and the absence of any next-level matrix or representation
1769 with the prescribed polynomial are Lean-checked. Other branches of the same
1770 unrestricted involution forest survive, so this example does not contradict
1771 finite-branch compactness.
1772
1773 \paragraph{Local properties need their own limit argument.}
1774 Over a domain, for a nonzero $\pi\in I$, the representations of the additive
1775 integer group given by
1776 \[
1777 \rho_n(g)=\begin{pmatrix}1&\pi^n g\\0&1\end{pmatrix}
1778 \]
1779 are all nontrivial and converge pointwise in the ideal-adic topology to the
1780 trivial representation. The convergence and the failure of limit preservation
1781 for nontriviality are formally checked. Thus not every property of approximating
1782 integral representations can be asserted for a limit. This example is not
1783 claimed to disprove stability for any particular intended Galois local condition.
1784
1785 \paragraph{Complete conditional existence boundary.}\phantomsection\label{book:x-construction-24}
1786 The eleventh block established the corresponding conditional matrix criterion.
1787 The \hyperref[book:x-construction-24]{conditional existence-boundary argument} now uses the complete common-spine conclusion of Claim 8.2: the returned
1788 coefficient-field representations are continuous, have the prescribed common
1789 polynomials and coefficient-specific determinants, and satisfy every selected
1790 local realization relation under the stated inverse-limit closure hypothesis.
1791 All finite reductions belong to the admissible classes.
1792
1793 For each supplied required packet $p$, let $A_p$ be its finite-dimensional carrier
1794 over a characteristic-zero field $E_p$, and let $e_p$ be the actual joint spectral
1795 projector for its finite list of split commuting conditions. No order on $E_p$
1796 is assumed. The source notation $\Tr(e_p)>0$ means that the unique natural number
1797 $n_p$ with $\Tr(e_p)=(n_p:E_p)$ is positive. The checked projector formula identifies
1798 $n_p$ with the dimension of the actual joint eigenspace.
1799
1800 An admissible realization here includes continuous coefficient-field members and
1801 membership of every finite reduction in its designated admissible class.
1802 Under the completion hypotheses and these supplied carrier hypotheses, Lean proves
1803 \[
1804 \begin{aligned}
1805 &\exists\,\rho,\ (x_p)_p:\quad
1806 \rho\text{ is an admissible realization of the full chosen spine},\quad
1807 0\ne x_p\in\operatorname{im}(e_p)\text{ for every }p\\
1808 &\quad\Longleftrightarrow\quad
1809 \bigl(\forall\lambda,\ X_{\lambda,1}(\Compat)\ne\varnothing\bigr)
1810 \ \land\ \bigl(\forall\lambda,\ \forall m\ge2,
1811 X_{\lambda,m}(\Compat)\ne\varnothing\bigr)
1812 \ \land\ \bigl(\forall p,\ n_p>0\bigr).
1813 \end{aligned}
1814 \]
1815 The packet index may be infinite. Each $x_p$ belongs to its own supplied carrier.
1816 No common vector across distinct carriers or embedding of the reconstructed
1817 system into those carriers is asserted. Neither an unknown carrier nor positive
1818 trace is constructed without the corresponding hypotheses.
1819
1820 This completes Claim 11.2 at its conditional source scope, on the same counting
1821 basis used for Claim 8.2 in the \hyperref[book:x-construction-23]{conditional completion construction}. The full arithmetic application premises
1822 remain separate. In particular, the criterion does not prove universal occupancy,
1823 Hodge--Tate or Weil--Deligne attachment, or the Frobenius recovery clause of
1824 Claim 11.1. The latter still depends on the partial Claims 9.1 and 9.2.
1825
1826 \paragraph{Every required packet is necessary.}
1827 For each omitted index $N\in\mathbb N$, consider one-dimensional rational carriers
1828 with the identity operator, requiring eigenvalue $0$ at $N$ and eigenvalue $1$
1829 at every other index. The actual spectral projector has trace $0$ at $N$ and
1830 trace $1$ elsewhere. Lean proves that any predetermined finite sample of packet
1831 indices can miss an empty required packet: choose $N$ outside that sample.
1832 The family depends on the omitted index. This does not assert that one fixed
1833 family passes every finite prefix while failing global occupancy.
1834
1835 \begin{conjecture}[Natural finite seed rank]\label{px:11.3}
1836 For the admissible residual transport category attached to a fixed arithmetic class, the directed seed rank is finite. A one-seed theorem additionally requires a source component from which every required object is reachable and transports preserving deformation and occupancy data. For a finite condensation DAG, having exactly one source implies that reachability condition. For an infinite category, the existence of a unique source alone does not establish it.
1837 \end{conjecture}
1838
1839 \section{Worked finite models}
1840
1841 \subsection{Smooth branch}
1842
1843 For \(q=3\) and formal dimension \(d=2\), the finite levels have cardinalities
1844 \[
1845 1,9,81,729,6561,\ldots.
1846 \]
1847 The seed zeta function is
1848 \[
1849 Z(T)=\frac{T}{1-9T}.
1850 \]
1851
1852 \subsection{Weighted dyadic chart}
1853
1854 For weights \((1,2,4)\), the counts are
1855 \[
1856 1,2,8,32,256,2048,\ldots.
1857 \]
1858 The first coordinate is active immediately, the second one level later, and the third at depth five. The exact rational function generated by the code is
1859 \[
1860 Z_{(1,2,4)}(T)
1861 =
1862 \frac{T(1-6T-8T^2-32T^3)}{1-8T}.
1863 \]
1864 The negative signs in this presentation arise from moving the denominator to \(1-8T\). Every power-series coefficient is positive.
1865
1866 \subsection{Singular branch}
1867
1868 For \(x^2=0\) over a residue field of size three, the counts are
1869 \[
1870 1,3,3,9,9,27,27,81,\ldots,
1871 \]
1872 and
1873 \[
1874 Z(T)=\frac{T+3T^2}{1-3T^2}.
1875 \]
1876 The exact branching dimension is \(1/2\).
1877
1878 \subsection{Directed transport}
1879
1880 The finite graph in \cref{fig:transport-graph} has three source components. The source-component theorem and brute-force enumeration both return the minimum seed count three.
1881
1882 \begin{figure}[H]
1883 \centering
1884 \includegraphics[width=0.84\linewidth]{16_proof_status.pdf}
1885 \caption{The finite and formal statements proved in this chapter are separated from the two remaining universal existence assertions.}
1886 \label{fig:proof-status}
1887 \end{figure}
1888
1889 \section{Computational certificates}
1890
1891 The code uses exact integer, rational, symbolic, and modular arithmetic for all mathematical identities. Floating-point arithmetic is used only to render the figures and to report a regression estimate alongside an exact branching dimension.
1892
1893 \begin{table}[H]
1894 \centering
1895 \caption{Selected exact certificates.}
1896 \begin{tabular}{lr}
1897 \toprule
1898 Certificate & Result\\
1899 \midrule
1900 Residual packet count in the mod-three model & 3\\
1901 Compatible base-five inverse-limit branch & yes\\
1902 First dyadic sign separation depth & 2\\
1903 Source strongly connected components & 3\\
1904 Brute-force minimum directed seed count & 3\\
1905 Cohomology packet reconstruction residual & 0\\
1906 Compatible common-spine test & passed\\
1907 Inconsistent spine detected & yes\\
1908 Recovered carrier multiplicities & \((2,0,1)\)\\
1909 Finite occupancy ranks & \((3,2,1,0)\)\\
1910 \bottomrule
1911 \end{tabular}
1912 \end{table}
1913
1914 The complete automated suite contains \(28\) tests. They cover residual partition, no crossing, inverse-limit digits, weighted and singular zeta coefficients, directed source components, cohomology packets, companion forests, common-spine consistency, finite Frobenius separation, multiplicity recovery, and exact occupancy projectors.
1915
1916 \section{Claim ledger}
1917
1918 \begin{longtable}{p{0.34\linewidth}p{0.18\linewidth}p{0.40\linewidth}}
1919 \toprule
1920 Statement & Status & Scope or boundary\\
1921 \midrule
1922 \endfirsthead
1923 \toprule
1924 Statement & Status & Scope or boundary\\
1925 \midrule
1926 \endhead
1927 Residual partition & proved & any moduli functor with well-defined reduction\\
1928 No crossing & proved & operations trivial at residual depth\\
1929 Inverse-limit reconstruction & proved & represented complete deformation problem\\
1930 Finite-branch compactness & proved & finite nonempty levels and finite branching\\
1931 Smooth and weighted seed zeta formulas & proved & stated formal coordinate models\\
1932 Singular power zeta and dimension & proved & scalar equation \(x^e=0\)\\
1933 Cohomology packet decomposition & proved & chain projectors commuting with the differential\\
1934 Directed minimum-seed theorem & proved & finite directed transport graph\\
1935 Adelic finite-depth completion & proved & common spine, all finite levels occupied, closed local conditions\\
1936 Compatible-carrier summand completion & proved & known semisimple compatible carrier and finite separation\\
1937 Finite occupancy trace & Lean checked & supplied commuting split operators and a characteristic-zero trace criterion\\
1938 Universal residual companions & not proved & requires nonempty root at every coefficient prime\\
1939 Universal compatible-system completion & not proved & algebraic spine and companion occupancy remain necessary\\
1940 Universal automorphic occupancy & not proved & requires positive global packet traces\\
1941 Unrestricted reciprocity & not claimed & belongs to later local and global chapters\\
1942 \bottomrule
1943 \end{longtable}
1944
1945 \section{Conclusion}
1946
1947 The residual seed theory becomes precise once vertical and horizontal generation are separated. Positive-depth perturbations can be complete within one formal component. They cannot change the residual root. The universal arithmetic seed is therefore a forest rather than one branch:
1948 \[
1949 \boxed{
1950 \text{residual roots}
1951 \longrightarrow
1952 \text{finite deformation levels}
1953 \longrightarrow
1954 \text{inverse-limit branches}.
1955 }
1956 \]
1957
1958 Projectors add three useful structures to this forest. They split tangent and obstruction complexes into exact subproblems, they measure delayed dyadic visibility through weights, and they turn finite carrier occupancy into an integer trace. Directed transport adds a fourth: it converts the informal question ``how many seeds are needed?'' into the source-component count of a condensation graph.
1959
1960 The system-level boundary is now narrow enough to state without ambiguity. One must construct a common algebraic spine, populate every residual companion forest, lift those companions through all depths, and prove positive occupancy of the required global packets. The present chapter proves the formal reconstruction, counting, transport, compactness, carrier, and finite-projector theorems used in that reduction. It does not assert the missing universal existence statements.
1961
1962 \appendix
1963
1964 \section{Algorithms implemented in the companion package}
1965
1966 \subsection{Residual towers}
1967
1968 The residual module partitions coordinates modulo \(p\), verifies compatibility
1969 \[
1970 x_{m+1}\equiv x_m\pmod{p^m},
1971 \]
1972 and reconstructs the digit \(a_{m-1}\) by
1973 \[
1974 a_{m-1}=\left\lfloor\frac{x_m}{p^{m-1}}\right\rfloor\pmod p.
1975 \]
1976
1977 For canonical representatives $0\le x_m<p^m$, set $x_0=0$. Compatibility also gives
1978 $a_{m-1}=(x_m-x_{m-1})/p^{m-1}\in\{0,\ldots,p-1\}$.
1979 The floor in the first formula is essential. For example, the compatible
1980 base-five residues $4,19$ give the second digit $3$, not the rational number $19/5$.
1981 The executable companion uses the same integer floor division.
1982
1983 \subsection{Transport condensation}
1984
1985 The transport module computes strongly connected components by two depth-first passes, forms the condensation graph, finds all source components, and selects one representative from each. A brute-force subset search is included only as an independent finite certificate.
1986
1987 \subsection{Companion forests}
1988
1989 For an integral polynomial \(f\), the finite root forest is obtained by exact enumeration of
1990 \[
1991 f(x)\equiv0\pmod{p^m}
1992 \]
1993 and by connecting a child \(x_{m+1}\) to its reduction modulo \(p^m\). This is intended for small exact examples, not large deformation rings.
1994
1995 \subsection{Cohomology packets}
1996
1997 Modular Gaussian elimination computes the ranks of the differentials. For
1998 \[
1999 C^{i-1}\xrightarrow{d_{i-1}}C^i\xrightarrow{d_i}C^{i+1},
2000 \]
2001 the finite dimension is evaluated as
2002 \[
2003 \dim H^i
2004 =
2005 \dim C^i-\rank d_i-\rank d_{i-1}.
2006 \]
2007 Packet subcomplexes are computed separately and checked against the total.
2008
2009 \subsection{Finite occupancy}
2010
2011 For each commuting semisimple operator, a Lagrange polynomial constructs the exact spectral idempotent. Their product gives the joint packet projector. Symbolic rational arithmetic verifies idempotence and the equality of trace and rank.
2012
2013 \section{Reproducibility boundary}
2014
2015 The companion code is a finite certificate library. It does not construct universal Galois deformation rings, compute general continuous group cohomology, prove representability, discover compatible systems, or evaluate automorphic trace formulas. Those are mathematical inputs or later existence problems. The source package makes the finite examples and displayed counts reproducible. Their computational checks remain distinct from universal proofs.
2016
2017
2018 \section*{Further construction details}
2019 The following constructions explain the representation, comparison and local
2020 arithmetic steps used in the chapter. Appendix~\ref{sec:conditional-final}
2021 assembles their conditional endpoint. The formal companion keeps the distinct
2022 source contracts and verification records separate.
2023
2024 \paragraph{The formal model and its hypotheses.}
2025
2026 The smooth formal-model classification, its finite point count, its integral digit streams, and its rational seed zeta identity are now checked in Lean. The actual representing-ring algebra isomorphism remains a supplied hypothesis. Neither smoothness nor Galois representability is inferred from numerical counts. All local maps are included in the classification, and locality and actual maximal-ideal-adic continuity are separately proved. Arbitrary choices of parameter representatives do not add phantom maps.
2027
2028 General prescribed-conjugacy prime coverage remains an input. Claims 8.2
2029 and 11.2 retain their conditional hypotheses, including the required residual
2030 levels, higher depths and supplied packets. Their nonemptiness and positive
2031 trace are not unconditional conclusions. The finite cyclotomic comparison and
2032 the fixed quadratic packet give restricted arithmetic realizations. In the
2033 latter, the packet characters are trivial on actual valuation inertia at odd
2034 primes. Identifying the decomposition group with the full local Galois group
2035 remains a separate obligation, and ramification at two is not claimed.
2036 The constructions do not identify every packet in the common arithmetic spine
2037 or attach all Hodge--Tate and Weil--Deligne invariants. Universal occupancy and
2038 natural finite seed rank remain conjectural.
2039
2040 \paragraph{Finite-group comparison with precision loss.}\phantomsection\label{book:x-construction-17}
2041 Let $R$ be a commutative domain, $\Gamma$ a finite group, and $\rho,\tau$
2042 actual integral matrix representations. Suppose $a=|\Gamma|\ne0$ in $R$ and
2043 $a\mid\pi^e$. An equivariant matrix modulo $(\pi)^{e+k}$ lifts to an
2044 integral equivariant matrix with the prescribed reduction modulo $(\pi)^k$.
2045 Indeed, lift its entries to $A$ and form
2046 \[
2047 S=\sum_{g\in\Gamma}\rho(g)A\tau(g^{-1}).
2048 \]
2049 The finite equations imply $S-aA=\pi^{e+k}E$ with $E$ integral. Choose $b$
2050 with $\pi^e=ab$ and put $P=A+b\pi^kE$. Then $aP=S$, so cancellation of
2051 $a\ne0$ proves equivariance. Over a local ring, if $\pi$ is a nonunit,
2052 $k>0$ and the supplied comparison is invertible, $P$ is an integral unit.
2053 Neither completeness nor a finite residue field is needed for this step.
2054
2055 For a DVR, $e=v_\pi(|\Gamma|)$ is derived from the actual group order.
2056 The single precision $e+1$, independent of rank, detects integral
2057 isomorphism. It makes reduction injective on integral isomorphism classes,
2058 and finite coefficient quotients give finitely many integral classes in
2059 fixed rank. This is a formalization of classical finite-group rigidity
2060 (Maranda, 1953, Theorem~2), with an explicit proof of the comparison's
2061 precision loss.
2062
2063 For complete local coefficients with finite quotients, downward-compatible
2064 allowed representations occupied at every precision, and the required
2065 finite-group type at depth $e+1$, reconstruction followed by this comparison
2066 produces the required integral representation. Continuity is proved for a
2067 finite discrete source and for pullback through a fixed continuous map to
2068 that source. Occupancy at only one precision is insufficient. The result
2069 lifts comparisons between actual integral representations. It does not lift
2070 arbitrary quotient representations or supply the missing arithmetic packet
2071 interpretation.
2072
2073 For $C_2$ over $\mathbb Z_2$, take
2074 \[
2075 \tau(g)=\begin{pmatrix}1&0\\0&-1\end{pmatrix},\qquad
2076 \rho(g)=\begin{pmatrix}1&2\\0&-1\end{pmatrix},\qquad
2077 A=\begin{pmatrix}1&1\\0&1\end{pmatrix}.
2078 \]
2079 The matrix $A$ intertwines modulo $4$ and its average is
2080 $P=\left(\begin{smallmatrix}1&-1\\0&1\end{smallmatrix}\right)$.
2081 No exact intertwiner can retain $A$ modulo $4$, although $P$ retains it
2082 modulo $2$. The actual trivial and sign representations also agree modulo
2083 $2$ but are not integrally isomorphic. These checked examples show why
2084 residual-only detection and full preservation of the input precision cannot
2085 be asserted here.
2086
2087
2088 \paragraph{Lifting a summand inside a supplied finite-group carrier.}\phantomsection\label{book:x-construction-18}
2089 Let $R$ be a commutative integral domain complete and separated for the
2090 $(\pi)$-adic filtration. Let $\Gamma$ be a finite group, and let
2091 $\rho:\Gamma\to\mathrm{GL}_n(R)$ be an actual integral representation.
2092 Assume that $a=|\Gamma|\ne0$ in $R$ and $a\mid\pi^e$. For $k>0$, suppose
2093 \[
2094 \bar E\in M_n\bigl(R/(\pi)^{e+k}\bigr),\qquad
2095 \bar E^2=\bar E,\qquad
2096 \bar\rho(g)\bar E=\bar E\bar\rho(g)\quad(g\in\Gamma).
2097 \]
2098 There is an actual integral matrix $E$ satisfying
2099 \[
2100 E^2=E,\qquad \rho(g)E=E\rho(g),\qquad
2101 E\bmod(\pi)^k=\bar E\bmod(\pi)^k.
2102 \]
2103 No integral summand or coherent family of quotient projectors is assumed.
2104 No local-ring assumption or finiteness of the residue field is needed.
2105
2106 To prove this, apply the preceding averaging correction with both
2107 representations equal to $\rho$. This produces an exact equivariant matrix
2108 $A$ with the prescribed reduction at depth $k$, so that
2109 $A^2-A\in(\pi)^kM_n(R)$. Averaging alone need not preserve idempotence.
2110 Use the integral polynomial
2111 \[
2112 f(A)=3A^2-2A^3.
2113 \]
2114 The identities
2115 \[
2116 f(A)-A=(1-2A)(A^2-A),\qquad
2117 f(A)^2-f(A)=(A^2-A)^2(4A^2-4A-3)
2118 \]
2119 show that successive corrections preserve the retained reduction and improve
2120 the idempotence defect. In these formulas scalar constants denote scalar
2121 matrices. The Lean proof establishes at least one additional ideal digit at
2122 each step, constructs the resulting compatible family of finite-level matrices, and uses
2123 completeness and separatedness to recover $E$. Every matrix commuting with
2124 $A$ commutes with $E$. There is no division by $2$, so the correction also
2125 works in residue characteristic $2$.
2126
2127 The actual submodules $U=\operatorname{im}E$ and $W=\ker E$ are invariant,
2128 and addition gives an equivariant isomorphism
2129 \[
2130 U\oplus W\simeq R^n.
2131 \]
2132 The inclusion $i:U\hookrightarrow R^n$ and retraction $r(v)=Ev$ are
2133 constructed as linear maps and satisfy $ri=1_U$ and $ir=E$. Their
2134 equivariance is proved. Coordinatewise reduction maps $U$ onto
2135 $\operatorname{im}(\bar E\bmod(\pi)^k)$ and maps $W$ onto
2136 $\ker(\bar E\bmod(\pi)^k)$. Both equalities are surjectivity statements
2137 onto the actual submodules over the finite-level quotient, not merely containment. The same
2138 projector defines a summand after pullback through any group homomorphism
2139 to $\Gamma$.
2140
2141 For $R=\mathbb Z_2$ and the sign carrier
2142 $\rho(s)=\operatorname{diag}(1,-1)$, the projector
2143 \[
2144 \bar E=\begin{pmatrix}1&2\\0&0\end{pmatrix}\pmod4
2145 \]
2146 is equivariant and the theorem constructs a nonzero proper equivariant
2147 projector retaining its reduction modulo $2$. No exact equivariant
2148 endomorphism retains this prescribed matrix modulo $4$. At the insufficient
2149 input depth $1$, the projector
2150 $\left(\begin{smallmatrix}1&1\\0&0\end{smallmatrix}\right)\pmod2$
2151 has no exact equivariant lift retaining its reduction. These are statements
2152 about the supplied carrier and prescribed projectors, not about nonexistence
2153 of all integral summands.
2154
2155 This construction gives one summand and its complement inside a supplied
2156 finite-group carrier. It advances the carrier step in Claim 9.2. It does
2157 not identify the intended arithmetic packets, construct the arithmetic
2158 Weil--Deligne attachment, establish the Hodge--Tate comparisons, or prove
2159 universal occupancy.
2160
2161
2162 \paragraph{Simultaneous projector-family lifting and rigidity.}\phantomsection\label{book:x-construction-19}
2163 Keep the complete domain, supplied finite-group carrier and group-order
2164 hypotheses of the \hyperref[book:x-construction-18]{supplied-carrier summand-lifting construction}. Let $J$ be any finite label set and $k>0$. Suppose
2165 $(\bar E_i)_{i\in J}$ is a complete orthogonal family of equivariant
2166 idempotents modulo $(\pi)^{e+k}$. There exists an integral equivariant
2167 family $(E_i)_{i\in J}$ satisfying
2168 \[
2169 E_i^2=E_i,\qquad E_iE_j=0\ (i\ne j),\qquad
2170 \sum_{i\in J}E_i=1,\qquad
2171 E_i\bmod(\pi)^k=\bar E_i\bmod(\pi)^k.
2172 \]
2173 The loss is at most $e$, independent of $|J|$ and the ambient matrix rank.
2174 There is no local-ring or finite-residue-field hypothesis for existence.
2175 The formal theorem also treats empty label sets whenever their input
2176 equations can hold.
2177
2178 Average every supplied matrix once. Inductively let $C$ be the complement
2179 of the previously lifted projectors and correct the next averaged matrix
2180 inside the corner defined by $C$. The integral polynomial correction
2181 preserves the retained reduction and commutation with $C$ and the carrier.
2182 Multiplication by $C$ gives the required supported projector. This consumes
2183 no further precision. Once every label has been lifted, the complementary
2184 idempotent reduces to zero at positive depth. Adic separatedness forces it
2185 to vanish, proving the sum-to-identity equation.
2186
2187 The actual invariant images $U_i=\operatorname{im}E_i$ give an equivariant
2188 linear isomorphism
2189 \[
2190 \bigoplus_{i\in J}U_i\simeq R^n,
2191 \qquad (v_i)_i\longmapsto\sum_i v_i,
2192 \qquad v\longmapsto(E_iv)_i.
2193 \]
2194 Lean represents the finite direct sum by the finite product of the image
2195 submodules. The existing coordinatewise reduction theorem maps every
2196 $U_i$ onto the corresponding reduced projector image. No chosen bases or
2197 unproved freeness of the images are used.
2198
2199 For rigidity alone, let $R$ be a commutative local ring, let $\pi$ be a
2200 nonunit, and let $E,F$ be complete equivariant families on the same carrier
2201 with $E_i\equiv F_i\pmod{(\pi)^k}$ for every label and $k>0$. Then
2202 \[
2203 U=\sum_{i\in J}F_iE_i,\qquad
2204 U\equiv1\pmod{(\pi)^k},\qquad UE_i=F_iU.
2205 \]
2206 Reduction reflects invertibility in this setting, so $U$ is an integral
2207 unit and $UE_iU^{-1}=F_i$. It commutes with the carrier and induces actual
2208 equivariant isomorphisms $\operatorname{im}E_i\simeq\operatorname{im}F_i$.
2209 This rigidity theorem requires neither a finite acting group, a domain,
2210 nor completeness. More generally a unit-reflecting coefficient map suffices.
2211 The combined result proves existence and uniqueness up to this labeled
2212 conjugacy. Exact uniqueness of the matrices is false.
2213
2214 For the continuous $\mathbb Z_2$ carrier
2215 $\rho(s)=\operatorname{diag}(1,-1,1)$, conjugate the three coordinate
2216 projectors by $1+2e_{01}$ and reduce modulo $4$. They form a complete
2217 equivariant family. The general theorem constructs three nonzero integral
2218 summands retaining this family modulo $2$. No exact equivariant family
2219 retains the whole prescribed family modulo $4$. Separate checked examples
2220 show that independent equivariant idempotent lifts can lose orthogonality,
2221 and that distinct complete families with the same reduction can be related
2222 by the asserted identity-congruent conjugacy.
2223
2224 The \hyperref[book:x-construction-19]{simultaneous projector-family lifting construction} completes this finite-group projector-family step. The actual
2225 arithmetic packets, Galois-to-Weil--Deligne attachment, coefficient and
2226 Hodge--Tate/period comparisons, and arithmetic Frobenius coverage remain
2227 outside this result. Universal occupancy remains conjectural.
2228
2229
2230 \paragraph{General finite logarithmic recovery.}\phantomsection\label{book:x-construction-20}
2231 Let $A$ be a rational algebra, without any commutativity assumption on $A$.
2232 For a unipotent element $U$ and a positive integer $d$ satisfying
2233 $(U-1)^d=0$, put
2234 \[
2235 L_d(U)=\sum_{j=1}^{d-1}\frac{(-1)^{j+1}}{j}(U-1)^j.
2236 \]
2237 The value is independent of the chosen annihilating exponent. The finite
2238 logarithm and the nilpotent exponential satisfy
2239 \[
2240 L(\exp N)=N,\qquad \exp(L(U))=U.
2241 \]
2242 Both maps preserve every annihilating exponent, and hence preserve the
2243 exact nilpotency class of $N$ and $\exp(N)-1$, or of $U-1$ and $L(U)$.
2244 The Lean finite sum includes its zero-index term with coefficient zero.
2245 The displayed mathematical sum starts at one. The formal statements also
2246 handle the zero algebra and the exponent-zero case.
2247
2248 The proof evaluates Mathlib's formal power-series inverse identities at
2249 constant nilpotent series. Such evaluation is exactly a finite polynomial.
2250 For an arbitrary noncommutative ambient algebra, perform the calculation
2251 inside the commutative subalgebra generated by the element and then apply
2252 its inclusion. No analytic convergence or topology is assumed. The
2253 finite logarithm commutes with ring homomorphisms between rational algebras.
2254
2255 Let $K$ be a characteristic-zero field and $N$ an endomorphism with
2256 $N^d=0$. For $t\ne0$ the actual recovery formula is
2257 \[
2258 N=\frac1t\sum_{j=1}^{d-1}\frac{(-1)^{j+1}}{j}
2259 \bigl(\exp(tN)-1\bigr)^j.
2260 \]
2261 All coefficients lie in $K$. The vector spaces need not be finite
2262 dimensional, but nilpotence still means that some finite power of the
2263 whole operator is zero. A linear map intertwines two nilpotent operators exactly
2264 when it intertwines their exponential samples at a common nonzero
2265 parameter. Also
2266 \[
2267 \ker\bigl(\exp(tN)-1\bigr)=\ker N.
2268 \]
2269
2270 For supplied covariance data and the twisted cocycle of the \hyperref[book:x-construction-13]{finite-exponential reconstruction}, let
2271 $\rho_D(g)=\exp(t(g)N_D)r_D(g)$. If a common element $u$ satisfies
2272 $r_D(u)=r_E(u)=1$ and $t(u)\ne0$, every intertwiner of $\rho_D$ and
2273 $\rho_E$ recovers both the original $r$-intertwiner and the $N$-intertwiner.
2274 There is no cubic nilpotence restriction. This recovers equivariant
2275 projectors for both original components. Reconstructed-action isomorphisms
2276 induce actual isomorphisms of the inertia-fixed monodromy kernels. Their local characteristic polynomials
2277 agree under the existing finite-dimensional and normal-subgroup hypotheses.
2278
2279 For actual finite original inertia images the common kernel sample is
2280 derived. Suppose $u\in H$ satisfies $\nu(u)=1$ and $t(u)\ne0$ and both
2281 $r_D(H)$ and $r_E(H)$ are finite. Their sampled actions have positive
2282 finite orders $a,b$. At $u^{ab}$ both original actions are trivial, and
2283 \[
2284 t(u^{ab})=(ab)t(u)\ne0
2285 \]
2286 by the cocycle identity and characteristic zero. Thus the same full
2287 intertwiner equivalence holds using the actual finite-image hypotheses,
2288 without a separately supplied common trivial-action sample. The initial
2289 nonzero cocycle sample and the arithmetic interpretation of the data
2290 remain requirements.
2291
2292 Actual affine representations with monodromy chains of every finite
2293 length invoke these theorems. In particular a length-six example has
2294 $N^5\ne0$ and $N^6=0$ and is recovered from its actual reconstructed action.
2295 The length-four example still defeats the old quadratic logarithm, while
2296 the full finite logarithm recovers it.
2297
2298 The sample hypotheses retain substantive content. A zero parameter loses
2299 $N$. For unrestricted supplied algebraic data, one can also absorb
2300 $\exp(tN)$ into $r$ and set the new monodromy to zero. The reconstructed
2301 representation is unchanged. The absorbed original action fails the
2302 required trivial-action sample condition. This is a counterexample in the
2303 algebraic datum class, not a failure of uniqueness of arithmetic
2304 Weil--Deligne attachment with finite original inertia action.
2305
2306 The \hyperref[book:x-construction-20]{finite logarithmic recovery argument} removes the general logarithmic-extraction gap from the local
2307 algebraic comparison. It does not construct the actual arithmetic
2308 attachment, identify every intended packet, prove the coefficient and
2309 Hodge--Tate/period comparisons, or prove arithmetic Frobenius coverage.
2310
2311
2312
2313 \paragraph{Interpreted quadratic arithmetic completion.}\phantomsection\label{book:x-construction-21}
2314 Fix the continuous quotient
2315 \[
2316 q:G_{\Q}\longrightarrow C_2
2317 \]
2318 obtained by the action on a chosen square root $i$ of $-1$ in the algebraic
2319 closure. Its surjectivity and the equivalence
2320 \[
2321 q(\sigma)=1\quad\Longleftrightarrow\quad\sigma(i)=i
2322 \]
2323 are proved using the existing actual quadratic Galois construction.
2324 For a commutative ring $B$, define the arithmetic packet
2325 \[
2326 \mathcal P_q(B)=
2327 \{\chi:G_{\Q}\longrightarrow B^\times\mid\ker q\subseteq\ker\chi\},
2328 \]
2329 where the maps are group homomorphisms. Unique descent through the actual
2330 surjective map $q$ is derived, rather than supplied. Every member has finite
2331 image and is continuous for the coefficient topology, since its descent
2332 has the finite discrete domain $C_2$.
2333
2334 Let $R$ be any commutative ring and $B$ any commutative $R$-algebra. The
2335 coordinate ring $A_R=R[X]/(X^2-1)$ represents precisely this specified
2336 packet:
2337 \[
2338 \Hom_{R\text{-alg}}(A_R,B)
2339 \simeq\{x\in B:x^2=1\}
2340 \simeq\Hom(C_2,B^\times)
2341 \simeq\mathcal P_q(B).
2342 \]
2343 The first map evaluates the coordinate. Its inverse is the quotient
2344 universal property. A root is a unit with itself as inverse and determines
2345 a character by its value on the generator of $C_2$. Finally pull back
2346 along $q$. All inverse identities and naturality under coefficient
2347 homomorphisms are proved. In particular, the point reductions and actual
2348 arithmetic character reductions coincide. There is no invertibility-of-two,
2349 reducedness or nontriviality hypothesis on $B$. No smoothness or
2350 \'{e}taleness statement at two is used or asserted.
2351
2352 Let $I\subseteq R$ and suppose that $R$ is $I$-adically complete. Using
2353 the checked ring-map reconstruction on the quadratic coordinate ring,
2354 Lean proves
2355 \[
2356 \mathcal P_q(R)\simeq\varprojlim_{m\ge0}\mathcal P_q(R/I^m).
2357 \]
2358 The zero-precision quotient is included only for the formal indexing.
2359 The inverse constructs an actual arithmetic character, with exactly the
2360 prescribed reductions. It is unique, and its continuity is derived from
2361 its factorization through the same finite quotient.
2362
2363 There is also a completion theorem without chosen compatible characters.
2364 Suppose that $R/I^m$ is finite for every $m\ge1$, and that
2365 $C_m\subseteq\mathcal P_q(R/I^m)$ are allowed subsets such that every
2366 reduction of an allowed member is allowed. Then
2367 \[
2368 \begin{split}
2369 &\exists\chi\in\mathcal P_q(R),\quad
2370 \chi\text{ is continuous and }\chi\bmod I^m\in C_m
2371 \text{ for all }m\ge1\\
2372 &\hspace{3em}\Longleftrightarrow\quad
2373 C_m\ne\varnothing\text{ for all }m\ge1.
2374 \end{split}
2375 \]
2376 The root interpretation makes the allowed finite levels genuinely finite.
2377 Finite-branch compactness chooses the compatible roots, and the ring
2378 reconstruction gives their integral root. Naturality turns this into the
2379 required arithmetic character. Surjectivity of transitions and individual
2380 liftability of every finite node are not assumed. The root-level theorem
2381 needs only the allowed root subsets to be finite.
2382
2383 For $R=\Z_2$, Lean derives finiteness of all positive maximal-ideal
2384 quotients and applies this completion theorem. Since $\Z_2$ is a domain,
2385 its only roots of $X^2-1$ are $1$ and $-1$. Thus the integral packet has
2386 exactly two distinct characters: the trivial character and the sign
2387 character describing the action on $i$. They have the same reduction
2388 modulo two and distinct reductions modulo four.
2389
2390 The distinction between finite occupancy and continuation is witnessed
2391 by an actual finite arithmetic character. The roots modulo eight are
2392 $1,3,5,7$. The root $3$ defines a member of
2393 $\mathcal P_q(\Z/8\Z)$, but no member of
2394 $\mathcal P_q(\Z/16\Z)$ reduces to it. Indeed the only scalar lifts of
2395 $3$ are $3$ and $11$, and both square to $9$ modulo sixteen. The formal
2396 proof also classifies all roots modulo sixteen and the reductions with
2397 children. Consequently a nonempty finite node need not lie on an
2398 infinite branch, even in this explicitly interpreted arithmetic packet.
2399
2400 The \hyperref[book:x-construction-21]{fixed-quadratic-packet interpretation} completes this restricted arithmetic interpretation and its
2401 conditional completion. The packet is defined by one fixed quotient. It
2402 is not the collection of all quadratic characters of $G_{\Q}$. No local
2403 ramification criterion, Hodge--Tate weight, Weil--Deligne attachment, or
2404 cross-coefficient local invariant was established by the \hyperref[book:x-construction-21]{fixed-quadratic-packet interpretation}. The full
2405 manuscript still requires its remaining packet identifications and
2406 arithmetic comparisons. Universal positive occupancy remains conjectural.
2407
2408 \paragraph{Actual quadratic local conditions and completion.}\phantomsection\label{book:x-construction-22}
2409 Continue with the fixed packet $\mathcal P_q$ above. For a
2410 characteristic-zero field $K$, let
2411 \[
2412 j_K:G_K\longrightarrow G_{\Q}
2413 \]
2414 be the actual field-induced homomorphism between absolute Galois groups.
2415 It includes a chosen embedding of algebraic closures. Let $i_K$ be the
2416 image of the chosen square root $i$ under that embedding. Lean proves
2417 compatibility with the Galois actions and hence
2418 \[
2419 (q\circ j_K)(\sigma)=1
2420 \quad\Longleftrightarrow\quad \sigma(i_K)=i_K.
2421 \]
2422 The fixed-field theorem for the algebraic closure then gives
2423 \[
2424 q\circ j_K=1
2425 \quad\Longleftrightarrow\quad
2426 \exists x\in K,\ x^2=-1.
2427 \]
2428 If no such root exists, the local quotient is surjective onto $C_2$.
2429 These are statements about the actual local Galois map, not a supplied
2430 arithmetic interpretation of a scalar label.
2431
2432 For every commutative coefficient ring $B$ and $\chi\in\mathcal P_q(B)$,
2433 define $\chi_K=\chi\circ j_K$. The local character is continuous and
2434 commutes with coefficient change. The precise local admissibility
2435 condition is
2436 \[
2437 \operatorname{LocallyTrivial}_K(\chi)
2438 \quad\Longleftrightarrow\quad \chi_K=1.
2439 \]
2440 Descent through the fixed quadratic quotient proves
2441 \[
2442 \operatorname{LocallyTrivial}_K(\chi)
2443 \quad\Longleftrightarrow\quad
2444 \bigl(\exists x\in K,\ x^2=-1\bigr)\ \lor\ \chi=1.
2445 \]
2446 No reducedness, characteristic-zero or domain hypothesis is imposed on
2447 $B$. In particular, the formula applies to the finite coefficient
2448 quotients used in completion.
2449
2450 The p-adic square-root criterion is proved for every prime:
2451 \[
2452 \bigl(\exists x\in\Q_p,\ x^2=-1\bigr)
2453 \quad\Longleftrightarrow\quad p\equiv1\pmod4.
2454 \]
2455 A root satisfies $\lvert x\rvert_p^2=1$ and is therefore integral.
2456 Reduction modulo three rules out a root in $\Q_3$, and reduction modulo
2457 four rules out a root in $\Q_2$. At an odd prime, any residue root of
2458 $X^2+1$ has nonzero derivative and lifts by the pinned Mathlib Hensel
2459 theorem. The finite-field square criterion then gives the stated
2460 congruence. An explicit Hensel application at the residue root $2$ modulo $5$ supplies
2461 a root in $\Z_5$. Consequently
2462 \[
2463 \boxed{
2464 \operatorname{LocallyTrivial}_{\Q_p}(\chi)
2465 \quad\Longleftrightarrow\quad p\equiv1\pmod4\ \lor\ \chi=1.
2466 }
2467 \]
2468 The arithmetic prime $p$ is independent of the coefficient prime. For
2469 the two integral $\Z_2$-valued characters, the sign character is locally
2470 trivial exactly at primes congruent to one modulo four. Both distinct
2471 global characters are locally trivial at five, while the sign character
2472 is nontrivial on the full local Galois groups at three and two.
2473
2474 The inertia theorem uses actual residue actions. For a valuation subring
2475 $A$ of an extension field $L/K$, let $D_A$ be its decomposition subgroup
2476 in $\operatorname{Aut}_K(L)$ and put
2477 \[
2478 I_A=\ker\bigl(D_A\longrightarrow\operatorname{Aut}(k_A)\bigr),
2479 \]
2480 where $k_A$ is the residue field. If $2$ is a unit in $A$, every member
2481 of $I_A$ fixes every $y\in L$ with $y^2=-1$. Indeed $y^{-1}=-y$, so
2482 $y$ belongs to $A$ and is a unit there. An automorphism sends $y$ to
2483 $y$ or $-y$. Their residues are distinct because $2$ and $y$ are units,
2484 whereas inertia fixes residues. The second possibility is excluded.
2485
2486 For every prime $p$, Lean constructs a valuation subring
2487 $A\subseteq\overline{\Q_p}$ containing the integral image of $\Z_p$
2488 such that the induced map $\Z_p\to A$ is local. For odd $p$, two is
2489 a unit. The preceding argument applies to every valuation subring
2490 containing that integral image, and hence every member of
2491 $\mathcal P_q(B)$ is trivial on its inertia subgroup after actual local
2492 restriction. The existence theorem supplies a locally dominating choice,
2493 so this assertion is not vacuous.
2494
2495 This inertia is the actual residue-action kernel inside $D_A$. No equality
2496 $D_A=G_{\Q_p}$ is established in this block. Nor is ramification at two
2497 proved: the nontrivial full local character there is a separate result.
2498 At three the $\Z_2$-valued sign character is nontrivial on the full local
2499 Galois group but trivial on every inertia subgroup covered by the theorem.
2500 Thus local triviality and the stated inertia triviality are distinguished
2501 by checked arithmetic examples.
2502
2503 The local conditions survive coefficient completion by a proved theorem.
2504 For an $I$-adically separated commutative ring $R$,
2505 \[
2506 \operatorname{LocallyTrivial}_K(\chi)
2507 \quad\Longleftrightarrow\quad
2508 \operatorname{LocallyTrivial}_K(\chi\bmod I^m)
2509 \text{ for every }m\ge1.
2510 \]
2511 If $-1$ has a square root in $K$, every packet member satisfies the
2512 condition. Otherwise the condition says that the character is globally
2513 trivial, and separatedness detects that equality through all reductions.
2514 This proves the closure statement for the independently defined arithmetic
2515 property.
2516
2517 Suppose now that $R$ is $I$-adically complete and that every positive
2518 quotient $R/I^m$ is finite. Let $C_m\subseteq\mathcal P_q(R/I^m)$ be
2519 allowed subsets preserved by reduction, and let $(p_s)_{s\in S}$ be any
2520 indexed family of arithmetic primes. The index set $S$ need not be finite.
2521 Lean proves the simultaneous arithmetic completion criterion
2522 \[
2523 \begin{split}
2524 &\exists\chi\in\mathcal P_q(R),\quad
2525 \chi\text{ continuous},\quad
2526 \chi\bmod I^m\in C_m\ (m\ge1),\quad
2527 \chi_{\Q_{p_s}}=1\ (s\in S)\\
2528 &\quad\Longleftrightarrow\quad
2529 \forall m\ge1,\ \exists\psi\in C_m,\quad
2530 \forall s\in S,\ p_s\equiv1\pmod4\ \lor\ \psi=1.
2531 \end{split}
2532 \]
2533 The constructed character also satisfies every odd-prime valuation-inertia
2534 condition stated above. Finite-branch compactness selects all finite
2535 characters together. No coherent branch or surjective transition maps
2536 are assumed. The new local-closure implication is proved, not supplied.
2537 Every-level occupancy remains a substantive hypothesis. One nonsplit
2538 selected prime forces the completed global character to be trivial.
2539
2540 For the integral dyadic packet, a single detecting precision is also
2541 proved: reduction modulo four detects local triviality uniformly in the
2542 arithmetic prime. Modulo two does not suffice. The sign character is
2543 nontrivial locally at three, while its reduction modulo two is trivial.
2544 This is a coefficient-depth failure, distinct from splitting of the
2545 arithmetic field.
2546
2547 The \hyperref[book:x-construction-22]{quadratic local-condition construction} finishes this actual local admissibility and completion step for
2548 the fixed quadratic packet. It does not identify all packets in the
2549 manuscript's common arithmetic spine, attach Weil--Deligne objects, or
2550 prove coefficient and Hodge--Tate/period comparisons. Identifying the decomposition group
2551 with the full local Galois group remains a separate inertia
2552 obligation, and ramification at two is not claimed. Universal occupancy and natural finite seed rank remain conjectures.
2553
2554 \input{residue_continuation_body.tex}
2555 \input{conditional_completion.tex}
2556 \clearpage
2557 \phantomsection
2558 \addcontentsline{toc}{section}{References}
2559 \input{references.tex}
2560 \clearpage
2561 \section{Worked visual atlas}\label{sec:atlas}
2562 Plates X.1--X.30 form the worked visual atlas. Their labels, qualified by chapter, identify the same examples throughout the collection.
2563
2564 The atlas develops exact finite models, not substitutes for universal proofs.
2565 Its first part separates residual roots, coherent branches, and occupied carrier
2566 packets. Its second part studies residue norms, cancellation, Mellin estimates,
2567 and the boundary between a finite calculation and arithmetic occurrence.
2568 The final plate distinguishes the three source contracts and their
2569 mathematical boundaries.
2570
2571 The visual studies connect these examples to the mathematical arguments
2572 and to the formal companion.
2573 \end{document}
Other PDFs for this work
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: b05114a096133f7259b0a1dd85d587db327c9451f5a2c2228e600d77d86aafbf