Paper X: Universal Residual Seeds and Conditional Occupied-System Completion

Download original file

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

Included manuscript sections

• conditional_completion.tex
• historical_checkpoint_frontmatter.tex
• reading_contract.tex
• references.tex
• residue_continuation_body.tex

Read the typeset paper

Read this chapter with formatted equations

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}{Core series X}
116 \renewcommand{\KomorebiKind}{Traditional monograph}
117 \renewcommand{\KomorebiShortTitle}{Paper X}
118 \renewcommand{\KomorebiTitleSize}{36}
119 \renewcommand{\KomorebiTitleLeading}{41}
120 \renewcommand{\KomorebiEdition}{Verification edition / 20 October 2026}
121 \KomorebiSetup
122 \begin{document}
123 \KomorebiCover
124 \KomorebiOpeningNote{This reading edition joins the preserved Block 27 manuscript, the subsequent residue-counting continuation, and the final checked conditional occupied-system completion. The live internal ledger is 20/20 at the explicitly amended conditional scope. Historical checkpoint totals remain dated evidence of their own source revisions. Universal companion existence, carrier existence, and nonzero occupancy are not inferred. The final assembly and its exact inputs are in Section~\ref{sec:conditional-final}.}
125 
126 
127 
128 \begin{abstract}
129 A residual representation is a genuine 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 paper 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 paper 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 papers 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 
Statement: Residual seed system161 \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 paper 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 
Statement: Residual partition · Go to proof · Read statement and proof side by side197 \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 
Proof block: Residual partition · Go to statement · Read statement and proof side by side209 \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 
Statement: No crossing under positive-depth perturbation · Go to proof · Read statement and proof side by side213 \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 
Proof block: No crossing under positive-depth perturbation · Go to statement · Read statement and proof side by side221 \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 
Statement: Zeroth-order obstruction225 \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 
Statement: Exact residual partition235 \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 
Statement: Represented complete deformation problems258 \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 
Statement: Formal inverse-limit reconstruction · Go to proof · Read statement and proof side by side262 \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 
Proof block: Formal inverse-limit reconstruction · Go to statement · Read statement and proof side by side274 \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 
Statement: Finite-branch compactness · Go to proof · Read statement and proof side by side282 \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 
Proof block: Finite-branch compactness · Go to statement · Read statement and proof side by side286 \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 
Statement: Smooth formal branch count · Go to proof · Read statement and proof side by side292 \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 
Proof block: Smooth formal branch count · Go to statement · Read statement and proof side by side310 \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 
Statement: Tangent and obstruction spaces338 \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 
Statement: Cohomology packet decomposition · Go to proof · Read statement and proof side by side355 \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 
Proof block: Cohomology packet decomposition · Go to statement · Read statement and proof side by side373 \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 
Statement: Finite packet complex432 \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{New checked realization of the finite pattern.}
447 The Block 04 implementation separately 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 is a new specified
457 realization of the displayed dimension pattern, not a claimed rerun of
458 the original companion implementation.
459 
460 
461 \begin{figure}[H]
462 \centering
463 \includegraphics[width=0.78\linewidth]{11_tangent_obstruction_packets.pdf}
464 \caption{A finite chain-projector model.  Tangent and obstruction dimensions are carried by one packet and reconstruct exactly.}
465 \end{figure}
466 
467 \section{The weighted dyadic residual forest}
468 
469 At an odd prime, distinct sign characters remain distinct in the residue field.  At the coefficient prime two,
470 \[
471 1\equiv-1\pmod2.
472 \]
473 Thus distinct characteristic-zero packets can share one residual root and separate only after more precision is retained.
474 
Statement: Visibility weight475 \begin{definition}[Visibility weight]\label{px:5.1}
476 For two integral packet coordinates \(a,b\in\Ocal\), define their separation depth
477 \[
478 w(a,b)=\min\{m\ge1:a\not\equiv b\pmod{\varpi^m}\},
479 \]
480 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.
481 \end{definition}
482 
483 \begin{example}[The two sign branches]\label{px:5.2}
484 The characters \(\chi_+(g)=1\) and \(\chi_-(g)=-1\) have the same reduction modulo \(2\), but
485 \[
486 1\not\equiv-1\pmod4.
487 \]
488 Their first separation depth is therefore \(2\).  One mod-two root contains two branches that become distinct at the next level.
489 \end{example}
490 
491 \begin{figure}[H]
492 \centering
493 \includegraphics[width=0.82\linewidth]{05_dyadic_delayed_separation.pdf}
494 \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.}
495 \end{figure}
496 
497 A simple weighted formal model already captures delayed visibility.  Let \(w_i\ge1\) and constrain
498 \[
499 t_i\in(\varpi^{w_i}\Ocal+\varpi^m\Ocal)/\varpi^m\Ocal.
500 \]
501 Then coordinate \(i\) is invisible until \(m>w_i\).
502 
Statement: Weighted smooth-chart count · Go to proof · Read statement and proof side by side503 \begin{proposition}[Weighted smooth-chart count]\label{px:5.3}
504 For weights \(\bm w=(w_1,\ldots,w_d)\),
505 \[
506 \boxed{
507 N_{\bm w}(m)
508 =
509 q^{\sum_{i=1}^d\max(m-w_i,0)}.
510 }
511 \]
512 \end{proposition}
513 
Proof block: Weighted smooth-chart count · Go to statement · Read statement and proof side by side514 \begin{proof}
515 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.
516 \end{proof}
517 
518 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.
519 
520 \begin{figure}[H]
521 \centering
522 \includegraphics[width=0.82\linewidth]{07_weighted_formal_chart.pdf}
523 \caption{Weights delay finite-depth visibility.  Once all coordinates are active, the asymptotic slope equals the ordinary formal dimension.}
524 \end{figure}
525 
526 \section{Seed zeta functions and branching dimensions}
527 
528 Finite-depth counts record more than the existence of a branch.  They distinguish smooth, weighted, and singular local geometry.
529 
Statement: Seed zeta function530 \begin{definition}[Seed zeta function]\label{px:6.1}
531 For a residual root \(\bar x\) with finite levels, define
532 \[
533 \boxed{
534 Z_{\bar x}(T)
535 =
536 \sum_{m\ge1}\#X_m(\bar x)T^m.
537 }
538 \]
539 When a weighted chart is specified, write \(Z_{\bm w}(T)\).
540 \end{definition}
541 
Statement: Smooth seed zeta function · Go to proof · Read statement and proof side by side542 \begin{theorem}[Smooth seed zeta function]\label{px:6.2}
543 For a smooth formal component of dimension \(d\),
544 \[
545 \boxed{
546 Z_d(T)=\frac{T}{1-q^dT}.
547 }
548 \]
549 \end{theorem}
550 
Proof block: Smooth seed zeta function · Go to statement · Read statement and proof side by side551 \begin{proof}
552 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.
553 \end{proof}
554 
Statement: Weighted seed zeta function · Go to proof · Read statement and proof side by side555 \begin{theorem}[Weighted seed zeta function]\label{px:6.3}
556 Let \(1\le w_1\le\cdots\le w_d\), put \(W=\sum_iw_i\), and let
557 \[
558 a_m=q^{\sum_i\max(m-w_i,0)}.
559 \]
560 Then
561 \[
562 \boxed{
563 Z_{\bm w}(T)
564 =
565 \sum_{m=1}^{w_d}a_mT^m
566 +
567 q^{-W}\frac{(q^dT)^{w_d+1}}{1-q^dT}.
568 }
569 \]
570 In particular, every weighted smooth chart has a rational seed zeta function.
571 \end{theorem}
572 
Proof block: Weighted seed zeta function · Go to statement · Read statement and proof side by side573 \begin{proof}
574 The finite sum records the depths before all coordinates are active.  For \(m\ge w_d+1\),
575 \[
576 a_m=q^{dm-W},
577 \]
578 so the remaining terms form one geometric series.
579 \end{proof}
580 
Statement: Singular power seed · Go to proof · Read statement and proof side by side581 \begin{theorem}[Singular power seed]\label{px:6.4}
582 For integers \(e\ge1\) and \(m\ge1\), in \(\Ocal/\varpi^m\) the equation
583 \[
584 x^e=0
585 \]
586 has exactly
587 \[
588 \boxed{
589 q^{m-\lceil m/e\rceil}
590 }
591 \]
592 solutions.  Its seed zeta function is
593 \[
594 \boxed{
595 Z_e(T)
596 =
597 \frac{\sum_{r=1}^{e}q^{r-1}T^r}
598 {1-q^{e-1}T^e}.
599 }
600 \]
601 \end{theorem}
602 
Proof block: Singular power seed · Go to statement · Read statement and proof side by side603 \begin{proof}
604 The congruence is equivalent to
605 \[
606 e\,v_\varpi(x)\ge m,
607 \]
608 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.
609 \end{proof}
610 
Statement: Branching dimension611 \begin{definition}[Branching dimension]\label{px:6.5}
612 When the limit exists, define the finite-level counting exponent
613 \[
614 \dim_{\mathrm{seed}}(\bar x)
615 =
616 \lim_{m\to\infty}
617 \frac{\log_q\#X_m(\bar x)}{m}.
618 \]
619 A limsup may be used in general.
620 \end{definition}
621 
Statement: Fractional singular dimension622 \begin{corollary}[Fractional singular dimension]\label{px:6.6}
623 For \(x^e=0\),
624 \[
625 \boxed{
626 \dim_{\mathrm{seed}}=1-\frac1e.
627 }
628 \]
629 In particular, \(x^2=0\) has branching dimension \(1/2\).
630 
631 \paragraph{Counting exponent versus compatible branches.}
632 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. This observation and the real logarithmic limit are both formalized in Block 02.
633 
634 \end{corollary}
635 
636 \begin{figure}[H]
637 \centering
638 \includegraphics[width=0.83\linewidth]{06_smooth_singular_counts.pdf}
639 \caption{A smooth two-dimensional formal chart and the singular equation \(x^2=0\) have visibly different exponential growth.}
640 \end{figure}
641 
642 \begin{figure}[H]
643 \centering
644 \includegraphics[width=0.78\linewidth]{08_fractional_seed_dimension.pdf}
645 \caption{The finite-depth branching dimension of \(x^e=0\) is \(1-1/e\), giving a family of fractional local growth exponents.}
646 \end{figure}
647 
648 \section{Residual transport categories}
649 
650 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.
651 
Statement: Admissible residual transport652 \begin{definition}[Admissible residual transport]\label{px:7.1}
653 An admissible transport from \(\bar\rho\) to \(\bar\rho'\) consists of
654 \[
655 \mathcal T:\bar\rho\longmapsto\bar\rho'
656 \]
657 together with natural maps
658 \[
659 \mathcal T_A:\Def_{\bar\rho}(A)\longrightarrow\Def_{\bar\rho'}(A)
660 \]
661 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.
662 \end{definition}
663 
664 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\).
665 
Statement: Directed seed rank666 \begin{definition}[Directed seed rank]\label{px:7.2}
667 For a directed transport graph \(G\), define
668 \[
669 \srank_G
670 =
671 \min\{|S|:\Cl_G(S)=V(G)\},
672 \]
673 where \(\Cl_G(S)\) is the set of vertices reachable from \(S\).
674 \end{definition}
675 
Statement: Directed minimum-seed theorem · Go to proof · Read statement and proof side by side676 \begin{theorem}[Directed minimum-seed theorem]\label{px:7.3}
677 Let \(G\) be a finite directed graph.  Collapse every strongly connected component to one vertex, obtaining the condensation DAG.  Then
678 \[
679 \boxed{
680 \srank_G
681 =
682 \#\{\text{source strongly connected components of }G\}.
683 }
684 \]
685 One representative from each source component is a minimum seed set.
686 \end{theorem}
687 
Proof block: Directed minimum-seed theorem · Go to statement · Read statement and proof side by side688 \begin{proof}
689 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.
690 
691 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.
692 \end{proof}
693 
694 For reversible transports the condensation has one vertex per connected component, recovering the undirected minimum-seed theorem.
695 
696 \paragraph{Formal scope and propagation.}
697 Reachability is the reflexive-transitive closure of the supplied directed edge
698 relation, and a strongly connected component is the actual quotient by mutual
699 reachability. The minimum seed count is defined independently as the least
700 cardinality of a set that reaches all vertices. Every covering set must meet
701 every source component; conversely, meeting every source component suffices
702 in a finite graph. Thus any choice of one representative from each source is
703 optimal. Empty graphs have rank zero, and self-loops are permitted. Adding
704 admissible edges cannot increase the minimum seed count.
705 
706 If a property $P$ propagates along every supplied edge and holds at all selected
707 seeds, it holds at every reached vertex. These are explicit hypotheses. The
708 minimum-seed theorem does not construct valid arithmetic edges or supply
709 initial occupancy.
710 
711 \paragraph{Why the finite hypothesis cannot be dropped.}
712 Take vertices $\{*\}\sqcup\{v_n:n\in\mathbf N\}$, with $*$ isolated and
713 edges $v_{n+1}\to v_n$. Every strongly connected component is a singleton,
714 and $\{*\}$ is the unique source component. No finite seed set covers all
715 vertices: it can reach only indices no larger than the largest chosen index.
716 Both the unique-source statement and the failure of every finite cover are
717 checked in Lean. Hence one source component in an infinite condensation does
718 not imply that one seed reaches all objects.
719 
720 
721 \begin{figure}[H]
722 \centering
723 \includegraphics[width=0.91\linewidth]{09_directed_transport_graph.pdf}
724 \caption{A finite directed transport model.  The components \(\{A,B\}\), \(\{D,E\}\), and \(\{G\}\) are sources; \(C\) and \(F\) are reached downstream.}
725 \label{fig:transport-graph}
726 \end{figure}
727 
728 \begin{figure}[H]
729 \centering
730 \includegraphics[width=0.86\linewidth]{10_source_scc_condensation.pdf}
731 \caption{The condensation DAG makes the minimum seed count visible without searching every subset of roots.}
732 \end{figure}
733 
Statement: Directed seed count734 \begin{numericalcertificate}[Directed seed count]\label{px:7.4}
735 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.
736 
737 \paragraph{New explicit checked realization.}
738 Separately from the unretrieved original companion implementation, Block 05
739 specifies vertices $A,B,C,D,E,F,G$ and the eight edges
740 \[
741  A\to B,\ B\to A,\ B\to C,\ C\to F,\ D\to E,\ E\to D,\ E\to F,\ G\to F.
742 \]
743 The source components are $\{A,B\}$, $\{D,E\}$, and $\{G\}$; the other
744 components are $\{C\}$ and $\{F\}$. A bounded path search to length three
745 is proved closed under every original edge, which certifies equality with
746 unbounded reachability. The resulting label certificate is identified with
747 the actual quotient by mutual reachability. Lean checks seed rank three and
748 exactly the four minimum sets
749 \[
750  \{A,D,G\},\quad\{A,E,G\},\quad\{B,D,G\},\quad\{B,E,G\}.
751 \]
752 Independent exact tests enumerate every directed graph on zero through four
753 vertices, including loops, and every seed subset. These finite tests audit the
754 implementation; the universal theorem is a separate formal proof.
755 
756 \end{numericalcertificate}
757 
758 \section{Prime-independent system seeds}
759 
760 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.
761 
Statement: Common arithmetic spine762 \begin{definition}[Common arithmetic spine]\label{px:8.1}
763 Let \(M\) be a number field.  A common spine \(\Compat\) consists of:
764 \begin{itemize}
765 \item characteristic polynomials \(P_v(X)\in M[X]\) at almost all places;
766 \item coefficient-prime independent weight and determinant data;
767 \item prescribed local Weil--Deligne or inertial packet labels at the ramified places.
768 \end{itemize}
769 For each finite place \(\lambda\) of \(M\), let
770 \[
771 X_{\lambda,m}(\Compat)
772 \]
773 be the finite set of admissible objects modulo \(\varpi_\lambda^m\) realizing the reduction of this spine.
774 \end{definition}
775 
776 The system seed is the fibered object
777 \[
778 \boxed{
779 \Sys_{\mathrm{sys}}
780 =
781 \Sys_2^{\mathrm{wt}}
782 \times_{\Compat}
783 \prod_{\lambda\nmid2}'\Sys_\lambda.
784 }
785 \]
786 The fiber product notation states a compatibility requirement.  It does not prove that every fiber is nonempty.
787 
Statement: Adelic finite-depth completion · Go to proof · Read statement and proof side by side788 \begin{theorem}[Adelic finite-depth completion]\label{px:8.2}
789 Assume:
790 \begin{enumerate}
791 \item an algebraic common spine \(\Compat\) over a number field \(M\) is fixed;
792 \item for every finite place \(\lambda\) of \(M\) and every \(m\ge1\), the companion level \(X_{\lambda,m}(\Compat)\) is finite and nonempty;
793 \item the reduction forests are finitely branching;
794 \item the selected local conditions are closed under inverse limits.
795 \end{enumerate}
796 Then for every \(\lambda\) there is an infinite compatible branch
797 \[
798 \rho_\lambda\in\varprojlim_mX_{\lambda,m}(\Compat),
799 \]
800 and the collection \(\{\rho_\lambda\}_\lambda\) realizes the prescribed strictly compatible spine.
801 \end{theorem}
802 
Proof block: Adelic finite-depth completion · Go to statement · Read statement and proof side by side803 \begin{proof}
804 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.
805 \end{proof}
806 
Statement: Residual companion obstruction807 \begin{corollary}[Residual companion obstruction]\label{px:8.3}
808 If
809 \[
810 X_{\lambda,1}(\Compat)=\varnothing
811 \]
812 for one coefficient prime \(\lambda\), no compatible completion with spine \(\Compat\) exists.  Deeper perturbations at other primes cannot create the missing residual companion.
813 \end{corollary}
814 
815 \begin{figure}[H]
816 \centering
817 \includegraphics[width=0.82\linewidth]{13_common_system_spine.pdf}
818 \caption{The local members are coordinates of one system only after their finite data descend to a common algebraic spine.}
819 \end{figure}
820 
821 \begin{example}[A scalar companion failure]\label{px:8.4}
822 For
823 \[
824 f(x)=x^2+1,
825 \]
826 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.
827 \end{example}
828 
829 \begin{figure}[H]
830 \centering
831 \includegraphics[width=0.79\linewidth]{12_companion_forest_occupancy.pdf}
832 \caption{Finite companion levels for \(x^2+1=0\).  The obstruction at \(2,3,7\) is visible before any deep lifting argument begins.}
833 \end{figure}
834 
835 
836 \paragraph{Conditional scope and complete assembly (Block 23).}
837 The theorem above is conditional on the chosen spine and the stated local
838 inverse-limit closure. In the fixed-rank integral representation setting,
839 ``closed under inverse limits'' means that every compatible family of admissible
840 finite representation classes, after coherent matrix framing and reconstruction,
841 satisfies the full selected local realization relations. It is not merely
842 closedness of an unrelated label space. Weight and packet relations retain their
843 supplied arithmetic meaning; they are parameters of the universal theorem.
844 For a general moduli functor, effectivity requires its own reconstruction
845 hypothesis or the corresponding full meaning of admissible inverse-limit closure.
846 
847 The complete Lean assembly now includes the common polynomials, good-place sets
848 with finite complements, coefficient-specific prescribed determinants, and every
849 selected weight and packet relation. Determinants are recovered from their
850 actual finite-class determinants. A single common field-valued character on the
851 whole Galois group is not assumed. The returned representations are continuous,
852 and their reductions form the actual compatible branches. Their common
853 polynomial identities hold at every declared good place, hence almost everywhere
854 for each coefficient prime.
855 
856 This checks Claim 8.2 as the universal conditional source theorem. The previous
857 partial status also demanded proofs that particular intended arithmetic packets
858 satisfy its premises; that stronger application target is not a conclusion of
859 the theorem. The Block 23 source-claim count was therefore sixteen checked and four partial.
860 Concrete Hodge--Tate and Weil--Deligne attachments, torsion interpretations,
861 closure instances, and companion nonemptiness remain obligations of arithmetic
862 applications. Inertial-type labels are not upgraded to full Weil--Deligne data.
863 
864 \paragraph{Checked representation-level completion and its arithmetic boundary.}
865 The eighth formalization block works with actual matrix representations of a
866 fixed group, not only with underlying sets. For a complete separated ring $R$
867 and ideal $I$, compatible maps
868 $\rho_m:G\to\operatorname{GL}_d(R/I^m)$ reconstruct a unique integral
869 representation for that fixed compatible family. Multiplication and inverses
870 are verified after every reduction. If all finite representations are continuous
871 for the discrete quotient topology, the integral representation is continuous
872 for the ideal-adic topology. This does not assert uniqueness among all possible
873 branches of the allowed forest.
874 
875 The forest has as its level the actual subtype of representations satisfying
876 the declared finite conditions. Those conditions must be preserved by reduction.
877 Finiteness and nonemptiness at every level give an infinite branch and hence an
878 actual continuous representation. Finiteness of the coefficient quotient alone
879 is not a substitute for finiteness of the allowed representation set for an
880 arbitrary source group. Surjectivity of the reductions is not required.
881 
882 All coefficients of the characteristic polynomial commute with reduction.
883 Consequently, prescribed integral characteristic polynomials at every precision
884 hold exactly in the reconstructed representation. For a common coefficient field
885 $E$, local integral polynomials lie in $\Ocal_\lambda[X]$ and are compared with
886 $P_v\in E[X]$ only after mapping both into the local coefficient field. No field
887 embedding $E\to\Ocal_\lambda$ is assumed. The allowed-place predicate is explicit
888 and may depend on $\lambda$. Trivial action on a supplied subgroup is likewise
889 detected at every precision; identifying that subgroup with arithmetic inertia
890 is a separate input.
891 
892 The eleventh block assembles continuous coefficient-field representations, exact
893 common polynomials and the prescribed local predicate from positive finite
894 depths. Depth-zero finiteness and nonemptiness are derived. Claims 8.2 and 11.1
895 already assume inverse-limit closure of the selected local conditions; an
896 unconditional closure theorem is not a missing hypothesis of their conditional
897 proofs. Their conditional matrix core is checked. The remaining full arithmetic
898 interpretation must identify the admissible finite objects and the actual local
899 invariants with these data. The coherent-framing obligation is resolved by Block 14
900 below. An arbitrary local
901 predicate is not being renamed Hodge--Tate or Weil--Deligne compatibility.
902 
903 
904 \paragraph{Completion from conjugacy classes (Block 14).}
905 Over an $I$-adically complete separated commutative coefficient ring $R$,
906 for a fixed finite rank, the formalization now takes finite-level objects to be
907 actual matrix representations modulo conjugation by an invertible matrix.
908 Assume the coefficient quotients $R/I^k$ are finite.
909 Conjugation commutes with coefficient reduction, and each conjugacy class has
910 finitely many frames over a finite coefficient ring. Thus finite allowed class
911 levels give finite full preimages of allowed matrix representations. Downward
912 admissibility and positive-depth nonemptiness yield an exactly compatible
913 matrix branch and an actual integral representation. More strongly, every
914 prescribed compatible class branch has such representatives, using finite
915 nonempty fibers over that branch. No surjectivity of reductions or lifting of
916 prescribed change-of-basis matrices is assumed. This does not assert uniqueness
917 up to integral conjugacy.
918 
919 For finitely generated $I$ with finite $R/I$, finiteness of $R/I^k$ is derived.
920 One continuous representative per allowed class suffices, because continuity
921 is proved invariant under conjugation. Characteristic polynomials, determinants
922 and trivial action on a supplied subgroup are likewise actual invariants.
923 The unframed common-spine theorem constructs continuous coefficient-field
924 representations with the prescribed whole polynomials and the explicitly
925 supplied inverse-limit-closed local predicate.
926 
927 An actual $\mathbb Z_3$ example applies the class-level completion theorem
928 for the cyclic group of order two and polynomial $X^2-1$, producing a nonidentity generator. Another
929 checked example has compatible classes represented by
930 $\operatorname{diag}(1,-1)$ modulo $3$ and
931 $\operatorname{diag}(-1,1)$ modulo $9$: these chosen matrices disagree under
932 reduction, and an actual swap of basis repairs them. Arbitrary independent
933 representatives therefore do not replace the framing argument.
934 
935 The framing obligation is finished. Identifying the manuscript's arithmetic
936 admissible objects, actual local invariants and finite-level packet reductions
937 with this interface remains separate. An uninterpreted local predicate is not
938 a construction of Hodge--Tate or Weil--Deligne compatibility. The source's local
939 closure hypothesis remains explicit. Block 23 completes the universal
940 conditional implication; these particular arithmetic applications remain
941 unproved.
942 
943 
944 \paragraph{Actual local comparisons from fixed-depth certificates (Block 15).}
945 Let $R$ be an $I$-adically complete separated commutative ring with finite
946 coefficient quotients and an injective map into a field $K$. Fix a finite matrix
947 rank. For finitely many
948 local group maps $\phi_s:H_s\to G$ and integral template representations
949 $\tau_s$, fix detecting depths $d_s$. At precision $m$ retain matrices $P_{s,m}$
950 as part of the admissible object and require
951 \[
952 \rho_m(\phi_s(h))P_{s,m}=P_{s,m}\tau_{s,m}(h).
953 \]
954 For $m\ge d_s$ require their determinants to remain nonzero after reduction to
955 $R/I^{d_s}$. Earlier levels omit that test. Finite occupied augmented levels
956 give a compatible branch of both representations and comparisons. The integral
957 limits satisfy the actual equations and have nonzero determinants, so the
958 comparisons are units over $K$. A converse supplies all finite nodes from any
959 integral realization with these detectors. Finite-level invertibility and
960 compatible prior choices of comparisons are not assumed.
961 
962 The unframed positive-depth version also retains continuity and whole common
963 polynomials. Its actual local isomorphisms are derived from the certificates;
964 there is no uninterpreted local-stability predicate for this particular problem.
965 The fixed depths and augmented-level occupancy remain explicit inputs.
966 
967 The formalization specializes to the actual maps
968 $G_{\mathbb Q_p}\to G_{\mathbb Q}$ induced by the field embeddings and choices
969 of algebraic closures. A nontrivial continuous quadratic character of
970 $G_{\mathbb Q}$, constructed from its action on $i^2=-1$, gives the integral
971 $2$-adic actions
972 \[
973 \tau(\sigma)=\operatorname{diag}(1,-1),\quad
974 \rho(\sigma)=\begin{pmatrix}1&-1\\0&-1\end{pmatrix},\quad
975 P=\begin{pmatrix}1&1\\0&2\end{pmatrix}
976 \]
977 at a nonidentity quadratic element. The determinant $2$ is detected modulo $4$.
978 The representations are conjugate over $\mathbb Q_2$ but not integrally
979 conjugate. A separate $\mathbb Z_3$ example invokes simultaneous completion
980 and reconstructs a comparison which is an integral nonunit and a field unit.
981 
982 The bound is substantive: for the unipotent actions
983 $\rho_a(g)=\begin{pmatrix}1&ag\\0&1\end{pmatrix}$, every integral intertwiner
984 with $\rho_1$ has determinant $aP_{22}^2$. Taking $a=\pi^n$ for a nonzero
985 $\pi\in I$ rules out every
986 fixed detecting depth, even though all the field-valued approximants are
987 isomorphic and their integral limit is trivial. This does not refute Claim 8.2,
988 which already assumes inverse-limit closure of its chosen local conditions.
989 
990 Exact prescribed local Galois action is stronger than an inertial-type label.
991 The common arithmetic packet interpretation, its coefficient comparisons and
992 the actual Hodge--Tate/Weil--Deligne attachment remain separate. The new theorem
993 does not supply a uniform bound for all intended arithmetic packets. Those
994 arithmetic applications remain unfinished; the universal conditional implication
995 is checked in Block 23.
996 
997 \paragraph{Derived comparison bounds (Block 16).}
998 For a finite group $\Gamma$ whose order is a unit in a commutative local
999 coefficient ring $R$, any prescribed equivariant residual isomorphism lifts to
1000 an integral isomorphism. Lift its matrix to $A$ and define
1001 \[
1002 P=|\Gamma|^{-1}\sum_{g\in\Gamma}\rho(g)A\tau(g^{-1}).
1003 \]
1004 Reindexing proves equivariance, and reduction recovers the prescribed matrix.
1005 Its determinant is a unit. Complete local coefficients with finite quotients,
1006 occupied compatible finite conditions and this residual type therefore give
1007 actual integral completion with detector depth one. A fixed continuous map
1008 $G\to\Gamma$ permits pullback to infinite source groups. The finite-level
1009 representations must factor through the same map, and the residual type is
1010 imposed on their $\Gamma$-actions. No uniform determinant bound or augmented
1011 certificate occupancy is assumed in this sector.
1012 
1013 For a second sector let $R$ be a DVR with uniformizer $\pi$, fraction field $K$
1014 and matrix rank $n$. If a fixed template $\tau$ has full $K$-linear action span,
1015 finite generation and denominator clearing give a fixed $c$ such that
1016 \[
1017 \pi^c M_n(R)\subseteq\operatorname{span}_R\{\tau(g):g\in G\}.
1018 \]
1019 Normalize a field comparison to an integral $P$ with a unit entry. The displayed
1020 span constructs an integral $B$ with $BP=\pi^cI$, so
1021 \[
1022 \det P\mid\pi^{cn},\qquad \det P\not\equiv0\pmod{\pi^{cn+1}}.
1023 \]
1024 One $c$ works for all integral representations in the fixed field-isomorphism
1025 class. Jacobson density derives full span from actual irreducibility and a
1026 scalar commutant. The formalization states these hypotheses directly and does
1027 not assume the DVR fraction field is algebraically closed.
1028 
1029 If at every precision there is an integral representation of this rational
1030 type satisfying the finite conditions, the derived bound supplies the
1031 simultaneous certificates of Block 15 and preserves the type after completion.
1032 The integral approximants are not required to be coherent, but their existence
1033 is a substantive premise. Arbitrary torsion nodes are not asserted to lift.
1034 
1035 Over $\mathbb Z_3$, the actual average corrects
1036 $A=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right)$ to
1037 $P=\left(\begin{smallmatrix}1&-1/2\\0&1\end{smallmatrix}\right)$ for the
1038 involutions $\rho(g)=\left(\begin{smallmatrix}1&1\\0&-1\end{smallmatrix}\right)$
1039 and $\tau(g)=\operatorname{diag}(1,-1)$. It preserves the residual comparison
1040 and has determinant one. Pullback through the quadratic character of the
1041 actual $G_{\mathbb Q}$ gives continuous arithmetic examples. In contrast, the
1042 identity and $\operatorname{diag}(1,\mathrm{sign})$ over $\mathbb Z/4$ agree
1043 modulo two but are not integrally conjugate. Their group order is not a unit.
1044 These restricted results do not supply general arithmetic packet attachment,
1045 all finite-level existence statements, or cross-coefficient compatibility.
1046 
1047 \section{Compatible carriers and finite Frobenius separation}
1048 
1049 One useful completion mechanism is available when the desired packet already occurs as a semisimple summand of a known compatible carrier.
1050 
Statement: Finite Frobenius separation · Go to proof · Read statement and proof side by side1051 \begin{theorem}[Finite Frobenius separation]\label{px:9.1}
1052 Let $\mathscr W_1,\ldots,\mathscr W_r$ be pairwise nonisomorphic strictly
1053 compatible systems whose members are absolutely irreducible, with common
1054 algebraic unramified trace values $t_i(v)$ in a number field $E$.
1055 There are $r$ distinct permitted unramified places $v_1,\ldots,v_r$ for which
1056 \[
1057  C=(t_i(v_j))_{j,i}\in M_r(E),\qquad \det C\ne0.
1058 \]
1059 Every coefficient-field embedding $\sigma_\lambda:E\hookrightarrow E_\lambda$
1060 therefore sends $C$ to an invertible matrix. Its entries agree with the
1061 ordinary representation traces
1062 $\operatorname{Tr}(W_{i,\lambda}(\operatorname{Frob}_{v_j}))$
1063 when the selected places satisfy the unramified compatibility convention
1064 for that coefficient prime. In particular, places above the residue
1065 characteristic of $\lambda$ are excluded from this ordinary trace comparison.
1066 \end{theorem}
1067 
Proof block: Finite Frobenius separation · Go to statement · Read statement and proof side by side1068 \begin{proof}
1069 Fix one coefficient prime. The classical independence of the characters of
1070 pairwise nonisomorphic absolutely irreducible representations and the density
1071 of unramified Frobenius conjugacy classes give independent restricted trace
1072 functions. Density here concerns the union of the conjugacy classes, not an
1073 unsupported assertion about a set of chosen representatives.
1074 
1075 For $r$ independent functions, their evaluation linear forms span the
1076 $r$-dimensional coefficient dual: a proper span would leave a nonzero
1077 coefficient vector annihilated by every evaluation, contradicting independence.
1078 Choose a basis from the evaluations. Its $r$ distinct sample points give an
1079 invertible square matrix. The common algebraic traces put that matrix over
1080 $E$; an injective field embedding reflects the nonvanishing of its determinant.
1081 All further field embeddings preserve the same nonvanishing.
1082 \end{proof}
1083 
1084 \paragraph{Formalization boundary.}
1085 Characteristic-zero independence is now Lean-checked for actual finite-dimensional
1086 irreducible representations of arbitrary monoids. Finiteness of the group and
1087 algebraic closedness of the field are not needed for this result. The proof
1088 uses the actual monoid algebra and Jacobson density to select constituent
1089 actions. Jointly continuous coordinate actions have continuous characters.
1090 Coverage in every open normal quotient of a compact totally disconnected group
1091 implies density of the conjugacy-saturated samples and hence the finite separator.
1092 General arithmetic Frobenius coverage remains unformalized. Block 25 now proves
1093 the bridge from componentwise nonisomorphic systems to nonisomorphic members
1094 at the selected coefficient prime, under density on the required good-place
1095 overlaps. It also proves the complete restricted separator for a fixed finite
1096 cyclotomic Galois group over $\Q$, with arithmetic coverage derived from the
1097 proved Dirichlet theorem. The full arithmetic theorem remains partial. Selection
1098 is existential and gives no effective upper bound on the selected primes.
1099 A common algebraic matrix is still distinct from an ordinary unramified trace
1100 comparison at all coefficient primes simultaneously.
1101 
1102 \paragraph{System isomorphism and good-place overlaps (Block 25).}
1103 The system equivalence used here is componentwise representation isomorphism:
1104 \[
1105  \mathscr W_i\simeq\mathscr W_j
1106  \quad\Longleftrightarrow\quad
1107  \forall\lambda,\ W_{i,\lambda}\simeq W_{j,\lambda}.
1108 \]
1109 For finite-dimensional irreducible representations of any monoid over a
1110 characteristic-zero field, the new character-rigidity theorem proves that
1111 equality of characters is equivalent to an actual equivariant linear isomorphism.
1112 Neither a finite group nor an algebraically closed coefficient field is needed.
1113 
1114 Suppose two members are isomorphic at $\lambda_0$. Injectivity of the common
1115 coefficient embedding gives $t_i(v)=t_j(v)$ at every place good for $\lambda_0$.
1116 At another coefficient prime $\lambda$, this equality compares actual member
1117 traces on the intersection of the two good-place sets. Conjugacy density of
1118 that intersection and continuity extend the equality to the whole group;
1119 character rigidity then gives an actual isomorphism at $\lambda$.
1120 Thus the nonisomorphism of systems supplies the required nonisomorphism of
1121 members. Equality of optional labels or record fields is not used as a
1122 substitute for representation equivalence.
1123 
1124 The generic separator now derives this bridge and permits any additional finite
1125 set of excluded places. Its coverage premise retains every finite deletion:
1126 for each finite excluded set and each open normal quotient, every quotient
1127 class contains a conjugate of an allowed sample. This implies density on each
1128 pair of cofinite good-place sets; no all-coefficient-prime common ordinary-trace
1129 domain is assumed.
1130 
1131 \paragraph{Arithmetic coverage for a fixed cyclotomic extension (Block 25).}
1132 Let $n>0$ and let $L=\Q(\zeta_n)$ be a cyclotomic number field. The canonical
1133 isomorphism
1134 \[
1135  \operatorname{Gal}(L/\Q)\simeq(\mathbb Z/n\mathbb Z)^\times
1136 \]
1137 defines $\sigma_p$ by $\sigma_p(\zeta_n)=\zeta_n^p$ when $p\nmid n$.
1138 For every automorphism $\sigma$, finite set $B\subset\mathbb N$ and bound $b$,
1139 Lean proves that there is a rational prime $p>b$, with $p\notin B$ and
1140 $p\nmid n$, such that $\sigma_p=\sigma$. The prime-existence step uses the
1141 proved Dirichlet theorem in the pinned Mathlib dependency.
1142 
1143 The arithmetic attachment is checked in this finite cyclotomic case. There is
1144 an actual maximal prime $\mathfrak P$ of $\mathcal O_L$ above $(p)$, its
1145 ramification index is one, and $\sigma_p$ belongs to its decomposition group.
1146 For every integral $x\in\mathcal O_L$,
1147 \[
1148  \overline{\sigma_p(x)}=\overline{x}^{\,p}
1149  \quad\text{in }\mathcal O_L/\mathfrak P.
1150 \]
1151 The residue identity is proved on all integral elements using
1152 $\mathcal O_L=\mathbb Z[\zeta_n]$. Existence of $\mathfrak P$ is obtained by
1153 lying over, rather than assumed. This specifies arithmetic Frobenius, with
1154 $p$-power residue action. The action and unramifiedness statements also hold
1155 for every maximal prime above the selected $p$.
1156 
1157 Consequently, for pairwise componentwise nonisomorphic compatible irreducible
1158 representation families of this fixed finite Galois group, the common algebraic
1159 trace matrix can be selected at distinct rational primes outside any prescribed
1160 finite set, with nonzero determinant. Every coefficient embedding preserves its
1161 nonvanishing; actual member trace comparisons retain that member's good-prime
1162 condition. No coverage or character-continuity hypothesis is added in this
1163 cyclotomic specialization: the prime coverage is proved, and the finite
1164 extension's Krull topology is discrete. A concrete conductor-four instance uses
1165 the actual field $\Q(\zeta_4)$.
1166 
1167 This is a complete restricted arithmetic case of Claim 9.1. It does not establish
1168 coverage in arbitrary finite quotients of the absolute Galois group, nor the
1169 Hodge--Tate and Weil--Deligne comparisons of Claim 9.2. The source-claim ledger
1170 therefore remains seventeen checked and three partial.
1171 
1172 \paragraph{Absolute Galois restriction and arithmetic witnesses (Block 26).}
1173 Fix a cyclotomic number field $L=\Q(\zeta_n)$ with $n>0$ and an embedding
1174 $j:L\hookrightarrow\overline{\Q}$. The new restriction map
1175 \[
1176  q_L:G_{\Q}\longrightarrow\operatorname{Gal}(L/\Q),\qquad
1177  j(q_L(\gamma)x)=\gamma(j(x)),
1178 \]
1179 is an actual continuous surjective homomorphism with open kernel. Surjectivity
1180 is derived by extending automorphisms to the algebraic closure. Pullback along
1181 a surjective homomorphism preserves and reflects equivariant linear
1182 isomorphisms, invariant subspaces, and irreducibility. These assertions keep
1183 the underlying linear maps and submodules and do not assume a finite acting
1184 group. In particular, the equivalence relation for systems is preserved and
1185 reflected componentwise.
1186 
1187 The arithmetic witnesses use the integral closure
1188 $\mathcal A$ of $\mathbb Z$ in $\overline{\Q}$. For each rational prime $p$,
1189 Lean constructs a maximal ideal $\mathfrak Q$ of $\mathcal A$ above $(p)$ and
1190 an actual element $\gamma_p\in G_{\Q}$ such that
1191 \[
1192  \gamma_p\in\operatorname{Stab}_{G_{\Q}}(\mathfrak Q),\qquad
1193  \overline{\gamma_p(a)}=\overline a^{\,p}
1194  \quad(a\in\mathcal A).
1195 \]
1196 The existence argument applies Mathlib's proved profinite stabilizer-surjectivity
1197 theorem to this actual invariant ring. The residue $p$-power map is proved
1198 bijective by taking $p$-th roots in $\overline{\Q}$ and showing that they
1199 remain integral when their $p$-th powers are integral. This constructs an
1200 arithmetic Frobenius witness in the prime-ideal decomposition group; it does
1201 not assert that an arbitrary global lift belongs to that group.
1202 
1203 When $p\nmid n$, the comparison with the finite cyclotomic sample is proved:
1204 \[
1205  q_L(\gamma_p)=\sigma_p,
1206  \qquad \sigma_p(\zeta_n)=\zeta_n^p.
1207 \]
1208 Reduction distinguishes $n$-th roots of unity at such a prime. Indeed, if
1209 $x^n=y^n=1$ and their reductions agree, the factorization of $x^n-y^n$ gives
1210 \[
1211  (x-y)\sum_{i=0}^{n-1}x^i y^{n-1-i}=0.
1212 \]
1213 The second factor reduces to $n\overline y^{\,n-1}\ne0$, so the domain
1214 property gives $x=y$. This proves both Frobenius recognition on the
1215 cyclotomic generator and triviality of its inertia action. Consequently,
1216 every representation pulled back through $q_L$ is unramified there.
1217 
1218 The valuation formulation is checked separately. For any valuation subring
1219 $A\subset\overline{\Q}$ with residue characteristic $p\nmid n$, its actual
1220 residue-action kernel fixes every $n$-th root of unity. A supplied element of
1221 its decomposition subgroup with $p$-power residue action restricts to
1222 $\sigma_p$. These statements use Mathlib's valuation inertia and decomposition
1223 subgroups. No identification of the valuation and integral-closure prime
1224 models is assumed in the formal comparison.
1225 
1226 For a compatible family $\rho_{i,\lambda}$ of representations of the fixed
1227 finite group, set $V_{i,\lambda}=\rho_{i,\lambda}\circ q_L$. Suppose the
1228 actual absolute-Galois members are irreducible and the systems are pairwise
1229 componentwise nonisomorphic. The finite prime separator now yields distinct
1230 permitted rational primes $p_j$, actual prime ideals $\mathfrak Q_j$ and
1231 arithmetic Frobenius witnesses $\gamma_j$ as above, outside any prescribed
1232 finite set, such that the common algebraic trace matrix has nonzero
1233 determinant. Every coefficient embedding preserves this nonvanishing, and
1234 \[
1235  \iota_\lambda(t_i(p_j))=
1236  \operatorname{tr}(V_{i,\lambda}(\gamma_j))
1237 \]
1238 whenever $p_j$ is good for that coefficient member. The operator and trace
1239 values agree for every global lift with the same cyclotomic restriction.
1240 Neither Frobenius-witness existence nor quotient coverage is a supplied
1241 hypothesis in this restricted arithmetic theorem. The common cyclotomic
1242 factorization and the compatible trace data remain explicit hypotheses.
1243 
1244 This completes the passage to actual absolute-Galois Frobenius witnesses for
1245 the fixed cyclotomic class. It does not establish prime coverage for arbitrary
1246 finite Galois extensions. Claim 9.1 therefore remains partial, and the
1247 source ledger remains seventeen checked and three partial.
1248 
1249 The boundaries are formalized as well. Pullback along a nonsurjective
1250 homomorphism can make inequivalent irreducible representations isomorphic.
1251 Samples can cover one quotient while missing an open quotient of the full
1252 group. Finally, in $\mathbb Z_2$, the distinct square roots $1$ and $-1$ have
1253 the same residue, so the condition that the root order be a unit cannot be
1254 discarded.
1255 
1256 \paragraph{General finite-field Frobenius comparison (Block 27).}
1257 Let $L/\Q$ now be any finite normal number field, with a chosen embedding
1258 $j:L\hookrightarrow\overline{\Q}$. Write $\mathcal A$ for the integral
1259 closure of $\mathbb Z$ in $\overline{\Q}$. The embedding restricts to an
1260 injective map $\mathcal O_L\to\mathcal A$ which intertwines the actual
1261 Galois actions. If $\mathfrak Q\subset\mathcal A$ is maximal above $(p)$,
1262 its contraction $\mathfrak P\subset\mathcal O_L$ is a nonzero maximal
1263 ideal above $(p)$, and the induced residue map is injective.
1264 
1265 Restriction carries the actual decomposition group at $\mathfrak Q$ into
1266 that at $\mathfrak P$, carries ideal inertia into ideal inertia, and
1267 preserves the arithmetic $p$-power residue action. Thus the absolute
1268 Frobenius constructed in Block 26 gives a simultaneous finite Frobenius
1269 at the contracted prime. This assertion applies to arbitrary finite normal
1270 number fields and does not require a cyclotomic generator.
1271 
1272 The exceptional primes are controlled by the actual field discriminant:
1273 \[
1274  S_L=\{p\text{ rational prime}:p\mid\operatorname{disc}(L)\}.
1275 \]
1276 This set is finite. For $p\notin S_L$, every prime of $\mathcal O_L$
1277 above $(p)$ is unramified. Lean proves that the actual inertia cardinality
1278 is the ramification index. It follows that inertia is trivial and the
1279 arithmetic Frobenius at a fixed finite prime is unique as a field
1280 automorphism. Neither trivial inertia nor uniqueness is assumed in place
1281 of the arithmetic unramifiedness condition.
1282 
1283 The choice of absolute prime and Frobenius lift is also controlled. Let
1284 $(\mathfrak Q_u,\gamma_u)$ and $(\mathfrak Q_v,\gamma_v)$ be any two
1285 actual arithmetic witnesses at the same rational prime. Transitivity on
1286 primes of $\mathcal A$ above $(p)$ gives $a\in G_{\Q}$ with
1287 \[
1288  \mathfrak Q_v=a\mathfrak Q_u,\qquad
1289  \gamma_v^{-1}a\gamma_u a^{-1}\in I_{\mathfrak Q_v}.
1290 \]
1291 Consequently, any representation trivial on $I_{\mathfrak Q_v}$ has the
1292 same trace on the two witnesses. For representations factoring through
1293 $L$, triviality on this actual absolute inertia is derived whenever
1294 $p\notin S_L$. The restrictions of all absolute witnesses at such a prime
1295 therefore form a single conjugacy class. This conclusion requires only
1296 the indicated finite factorization and the discriminant exclusion.
1297 
1298 There is a final compatibility between embeddings. For a normal subfield
1299 $L\subset\overline{\Q}$, restriction defined through a chosen embedding
1300 is conjugate to canonical restriction by one fixed automorphism of $L$.
1301 This identifies their conjugacy classes and lets the arithmetic comparison
1302 apply directly to the fixed fields of open normal subgroups of $G_{\Q}$.
1303 Those fixed fields are proved to be finite Galois number fields, with the
1304 original open normal subgroup as the kernel of restriction.
1305 
1306 The remaining prime-existence obligation now has a precise formulation.
1307 For every finite Galois subfield $L$, every finite set $B$ of rational
1308 primes, and every $\sigma\in\operatorname{Gal}(L/\Q)$, require a prime
1309 $p\notin B\cup S_L$ and an actual absolute arithmetic witness $\gamma_p$
1310 such that
1311 \[
1312  q_L(\gamma_p)\sim\sigma.
1313 \]
1314 Lean proves that this assertion is equivalent to the cofinite quotient
1315 coverage required by the general separator, for any fixed choice of actual
1316 Frobenius witnesses. The equivalence derives independence from the witness
1317 choices; it does not supply the displayed prime-existence assertion.
1318 Arbitrary finite exclusions absorb $S_L$, and the resulting conditional
1319 density theorem preserves the separate good-prime sets of coefficient
1320 members. General prime coverage remains unproved, so Claim 9.1 remains
1321 partial. The source ledger is still seventeen checked and three partial.
1322 This new arithmetic interface has base $\Q$. For the source's general-base
1323 instances involving $G_{F,S}$, the analogous actual-prime and norm-power
1324 Frobenius attachment and coverage over $F$, or a proved transfer to the
1325 rational-base result, also remain necessary.
1326 
1327 \paragraph{Finite deletion can destroy density.}
1328 In the actual discrete group $C_2=\{1,a\}$, set $s(0)=a$ and $s(m+1)=1$.
1329 The original samples are surjective and satisfy quotient coverage. Removing
1330 index zero leaves only the identity, so both density and quotient coverage fail.
1331 The actual rational sign and trivial characters agree on the remaining samples
1332 but differ globally. This checked example explains why ordinary coverage alone
1333 cannot justify deleting the bad places in the system comparison.
1334 
Statement: Compatible-carrier summand completion · Go to proof · Read statement and proof side by side1335 \begin{theorem}[Compatible-carrier summand completion]\label{px:9.2}
1336 Suppose a semisimple strictly compatible carrier decomposes as
1337 \[
1338 \mathscr W
1339 \cong
1340 \bigoplus_{i=1}^{r}
1341 \mathscr W_i^{\oplus c_i},
1342 \]
1343 with the \(\mathscr W_i\) as above.  At one coefficient prime \(\lambda_0\), suppose a semisimple summand has the form
1344 \[
1345 V_{\lambda_0}
1346 \cong
1347 \bigoplus_{i=1}^{r}
1348 W_{i,\lambda_0}^{\oplus m_i},
1349 \qquad
1350 0\le m_i\le c_i.
1351 \]
1352 Then
1353 \[
1354 \boxed{
1355 V_\lambda
1356 =
1357 \bigoplus_{i=1}^{r}
1358 W_{i,\lambda}^{\oplus m_i}
1359 }
1360 \]
1361 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.
1362 \end{theorem}
1363 
Proof block: Compatible-carrier summand completion · Go to statement · Read statement and proof side by side1364 \begin{proof}
1365 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.
1366 \end{proof}
1367 
1368 \paragraph{Recovery and realization are different steps.}
1369 For a certified square separator the coefficient vector is $C^{-1}t$.
1370 This is a valid carrier multiplicity vector only when every entry is a
1371 nonnegative integer and satisfies its capacity bound $m_i\le c_i$.
1372 Those tests and uniqueness of natural multiplicities in characteristic zero
1373 are separately Lean-checked, as is transport through a field embedding.
1374 Reduction modulo a residue characteristic is not a field embedding and may
1375 lose rank. The representation construction and common-polynomial part are now
1376 Lean-checked as described below. The full strictly compatible arithmetic
1377 statement, including its local conditions, remains partially formalized.
1378 
1379 \paragraph{Scope of the supplied-carrier hypothesis.}
1380 Claim 9.2 supplies the compatible carrier, its decomposition and the compatible
1381 constituent systems. Constructing unknown such objects is not required by that
1382 conditional theorem. The remaining formal obligation is that finite sums preserve
1383 the intended actual local arithmetic structures, together with the arithmetic
1384 separator input. The algebraic monodromy results below do not by themselves
1385 identify attached Weil--Deligne representations or Hodge--Tate comparison data.
1386 
1387 \paragraph{Explicit summands inside a supplied decomposition.}
1388 Let $K$ be a field, let $G$ be a monoid, and let
1389 $\rho_i:G\to\operatorname{End}_K(W_i)$ be actual representations on
1390 finite-dimensional spaces, indexed by a finite set $I$. For natural numbers
1391 $m_i\le c_i$, set
1392 \[
1393  U_m=\prod_{i\in I}\prod_{k<m_i}W_i,
1394  \qquad U_c=\prod_{i\in I}\prod_{k<c_i}W_i.
1395 \]
1396 These finite products realize the corresponding finite direct sums. The
1397 representation on $U_m$ acts componentwise. Define $j:U_m\to U_c$ by retaining
1398 the first $m_i$ copies and filling every remaining coordinate with zero.
1399 Define $r:U_c\to U_m$ by restriction to the selected copies. Lean proves
1400 \[
1401  rj=1_{U_m},\qquad
1402  j\rho_m(g)=\rho_c(g)j,\qquad
1403  r\rho_c(g)=\rho_m(g)r.
1404 \]
1405 The image of $j$ is exactly the subspace whose unused coordinates vanish.
1406 Consequently $jr$ is an equivariant idempotent. A supplied equivariant
1407 isomorphism $D:W\xrightarrow{\sim}U_c$ gives the split maps
1408 $D^{-1}j$ and $rD$ inside the original carrier. The decomposition $D$ is an
1409 input; these statements do not construct a decomposition of an unknown
1410 arithmetic carrier.
1411 
1412 The same formalization proves, for each $g\in G$,
1413 \[
1414  \det\bigl(XI-\rho_m(g)\bigr)
1415  =\prod_{i\in I}\det\bigl(XI-\rho_i(g)\bigr)^{m_i},
1416  \qquad
1417  \operatorname{Tr}\bigl(\rho_m(g)\bigr)
1418  =\sum_{i\in I}(m_i:K)\operatorname{Tr}\bigl(\rho_i(g)\bigr).
1419 \]
1420 Constituents may have different dimensions. Zero multiplicities, zero-dimensional
1421 constituents, and the empty index set are included. If at a permitted sample
1422 $g$ the constituent polynomials are the images of $P_{i,g}\in E[X]$ under a
1423 specified map $E\to K$, the summand polynomial is the image of
1424 $\prod_iP_{i,g}^{m_i}$. Applying this independently at each coefficient field
1425 preserves a supplied common polynomial family. This does not establish the
1426 Hodge--Tate or Weil--Deligne conditions in strict compatibility.
1427 
1428 Joint continuity of the constituent actions implies joint continuity of the
1429 constructed action. The inclusion and retraction are continuous for the
1430 product topologies, and triviality on a supplied subgroup is preserved.
1431 Neither continuity nor triviality is inferred for a carrier whose corresponding
1432 hypothesis has not been supplied. The maps transported by $D$ are proved
1433 algebraically; their topological interpretation additionally requires the
1434 appropriate continuity of $D$ and its inverse.
1435 
1436 For the three-character example below, the construction produces an actual
1437 three-dimensional summand inside the carrier of dimension seven. At the sample
1438 $(0,1)$ its characteristic polynomial is $(X-1)^2(X+1)$. A separate checked
1439 counterexample uses the coordinate inclusion $\mathbf Q\to\mathbf Q^2$, its
1440 coordinate retraction, and the swap involution: the split law holds, but
1441 compression sends the swap to zero and therefore fails to preserve its square.
1442 Thus selecting whole constituent copies, with the proved equivariance, is
1443 essential to this construction.
1444 
1445 \paragraph{Algebraic monodromy data on the selected copies.}
1446 Fix a field $K$ and a nonzero scalar $q\in K^\times$. On each constituent
1447 $W_i$, supply an automorphism $F_i$ and a nilpotent endomorphism $N_i$ with
1448 $F_iN_iF_i^{-1}=qN_i$. The scalar $q$ is common to this finite family.
1449 The componentwise operators $F_m,N_m$ on $U_m$ satisfy the same relation;
1450 $F_m$ is invertible and $N_m$ is nilpotent. The split maps constructed above
1451 intertwine both operators. The proof first identifies the independently defined
1452 kernel through an equivariant linear isomorphism
1453 \[
1454  \ker N_m\simeq\prod_{i\in I}\prod_{k<m_i}\ker N_i.
1455 \]
1456 The relation, with $q\ne0$, proves that both $F_i$ and its inverse preserve
1457 $\ker N_i$. Thus $F_i|_{\ker N_i}$ is an actual automorphism, and Lean proves
1458 \[
1459  \det(XI-F_m|_{\ker N_m})
1460    =\prod_{i\in I}\det(XI-F_i|_{\ker N_i})^{m_i}.
1461 \]
1462 The corresponding kernel dimensions and traces are additive with multiplicity.
1463 Common constituent kernel polynomials, when supplied through a coefficient-ring
1464 map, give the mapped product polynomial for the summand. Whole-space Frobenius
1465 polynomials are not substituted for these kernel polynomials.
1466 
1467 The exact special chain has basis $e_0,\ldots,e_{n-1}$ and operators
1468 \[
1469  Ne_0=0,\qquad Ne_j=e_{j-1}\ (j>0),\qquad Fe_j=aq^{-j}e_j,
1470  \qquad a,q\in K^\times.
1471 \]
1472 Lean proves $N^n=0$, and for $n>0$ also $N^{n-1}\ne0$ and
1473 $\ker N=Ke_0$. Consequently its kernel polynomial is $X-a$, whereas its
1474 whole-space polynomial is $\prod_{j=0}^{n-1}(X-aq^{-j})$.
1475 The zero-length chain is included as a zero-dimensional space; the assertion
1476 $\ker N=Ke_0$ is made only for positive length.
1477 
1478 For $n>1$, replacing $N$ by zero retains exactly the same $F$ and the same
1479 whole-space characteristic polynomial, while changing the degree of the kernel
1480 polynomial from one to $n$. Both pairs still satisfy the algebraic monodromy
1481 relation. This Lean-checked example shows that whole Frobenius data alone do
1482 not determine the monodromy kernel polynomial. It is not asserted to be a
1483 counterexample among the intended strictly compatible arithmetic systems.
1484 
1485 These statements concern supplied algebraic pairs. No Weil-group or inertia
1486 action, Hodge--Tate object, arithmetic comparison, or realization of the pair
1487 from a Galois representation is constructed here. The polynomial convention is
1488 $\det(XI-F|_{\ker N})$; no identification with an inertia-dependent local
1489 Euler factor is asserted. Claim 9.2 remains partial at its full arithmetic scope.
1490 
1491 
1492 \paragraph{Checked group, inertia and monodromy finite sums (Block 12).}
1493 Let $K$ be a field, $G$ a group, and $\nu:G\to K^\times$ a character.
1494 The new datum consists of an actual representation $r$ and nilpotent $N$ with
1495 $r(g)N=\nu(g)Nr(g)$ for every $g$. For a supplied subgroup $H$, define
1496 \[
1497  E(D,H)=\ker N\cap V^H.
1498 \]
1499 This is the intersection of independently defined kernel and actual invariant
1500 subspaces. For normal $H$, the restricted whole-group representation and its
1501 inverse automorphisms are constructed. A change from $\varphi$ to $\varphi h$,
1502 with $h\in H$, leaves the restricted operator itself unchanged.
1503 
1504 For a finite family of finite-dimensional constituents and natural multiplicities,
1505 the actual local space of the constructed sum is linearly equivalent to the sum of the constituent local spaces, equivariantly
1506 for every group element. Its characteristic polynomials multiply, its dimensions
1507 and traces add, and maps intertwining both the group and $N$ restrict to the
1508 local spaces. The explicit bounded-copy inclusion and retraction still split
1509 there. Finite inertia image and an open inertia kernel are preserved.
1510 
1511 Writing $Q_D(T)$ for the reversed local characteristic polynomial, Lean proves
1512 \[
1513  Q_D(T)=\det(1-T r(\varphi)\mid E(D,H)),\qquad Q_D(0)=1,
1514  \qquad
1515  Q_{\bigoplus_iD_i^{\oplus m_i}}(T)=\prod_iQ_{D_i}(T)^{m_i}.
1516 \]
1517 The abstract formulas do not need characteristic zero. Normality and finite
1518 dimension appear explicitly where used. Arithmetic identification of $G,H,\nu$
1519 and $\varphi$ remains separate. In the geometric-Frobenius convention,
1520 $\nu(\varphi)$ is the inverse residue cardinality; it is this unit, rather than
1521 the residue cardinality, that enters the earlier special-chain parameter.
1522 
1523 An explicit action of $C_2\times\mathbb Z$ has $\nu(\varphi)=1/3$,
1524 $F=\operatorname{diag}(2,6,18)$ and $Ne_1=e_0$, $Ne_2=e_1$, $Ne_0=0$.
1525 Trivial inertia gives local dimension one and denominator $1-2T$; scalar sign
1526 inertia gives dimension zero and denominator one. The entire $F$ and $N$ are
1527 equal in these two examples, and $N^2\ne0$. Thus inertia cannot be omitted.
1528 Conversely, unramified chains of lengths one and three have equal Euler
1529 denominators while only the first has $N=0$. Euler factors therefore do not
1530 identify complete monodromy data.
1531 
1532 The remaining arithmetic comparison is
1533 $\operatorname{WD}(\bigoplus_i V_i^{\oplus m_i})\cong
1534 \bigoplus_i\operatorname{WD}(V_i)^{\oplus m_i}$ for the actual attached functor,
1535 intertwining the Weil action and monodromy, together with the intended coefficient
1536 and Hodge--Tate comparisons. These are not supplied by the abstract datum.
1537 Claim 9.2 remains partial at its full arithmetic scope.
1538 
1539 Recovered multiplicities determine the semisimple isomorphism type relative
1540 to the specified constituents, not a canonical embedding or projector inside
1541 a repeated isotypic component. For example, the two projectors
1542 $\operatorname{diag}(1,0)$ and $\operatorname{diag}(0,1)$ on a two-dimensional
1543 trivial representation are distinct equivariant idempotents with trace one.
1544 
1545 \begin{figure}[H]
1546 \centering
1547 \includegraphics[width=0.72\linewidth]{14_frobenius_separator_matrix.pdf}
1548 \caption{A finite set of trace evaluations separates three compatible constituents and recovers their multiplicities.}
1549 \end{figure}
1550 
Statement: Multiplicity recovery1551 \begin{numericalcertificate}[Multiplicity recovery]\label{px:9.3}
1552 The original companion matrix was not retrieved or rerun. A new exact
1553 realization uses the trivial character and two independent sign characters
1554 of $(\mathbf Z/2\mathbf Z)^2$, evaluated at $(0,0),(1,0),(0,1)$:
1555 \[
1556  C=\begin{pmatrix}1&1&1\\1&-1&1\\1&1&-1\end{pmatrix},
1557  \qquad \det C=4,
1558  \qquad C\begin{pmatrix}2\\0\\1\end{pmatrix}
1559        =\begin{pmatrix}3\\3\\1\end{pmatrix}.
1560 \]
1561 Lean checks that these are the traces of actual one-dimensional
1562 representations, recovers $(2,0,1)$ uniquely, rejects a target whose unique
1563 solution is $(1/2,0,0)$, and rejects $(4,0,1)$ under capacities $(3,2,2)$.
1564 The separator becomes singular modulo two. These are finite-image
1565 representation checks, not fabricated Frobenius data for an arithmetic carrier.
1566 \end{numericalcertificate}
1567 
1568 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.
1569 
1570 
1571 \paragraph{Finite-exponential reconstruction and a cubic inverse (Block 13).}
1572 Let $K$ be a characteristic-zero field and let $(r,N)$ be supplied group data
1573 with nilpotent $N$ and $r(g)N=\nu(g)Nr(g)$. For a supplied scalar map satisfying
1574 \[
1575 t(gh)=t(g)+\nu(g)t(h),
1576 \]
1577 the formalization constructs
1578 \[
1579 \rho(g)=\exp(t(g)N)r(g),\qquad
1580 \exp(aN)=\sum_{j=0}^{d-1}\frac{a^j}{j!}N^j\quad(N^d=0).
1581 \]
1582 Lean proves the representation laws, actual finite-copy and split-map
1583 compatibility, and joint continuity from continuity of $N$, $r$ and $t$ with
1584 the stated continuous vector-space operations. The monodromy fixed kernel
1585 intersected with subgroup invariants is unchanged by this twist. For normal
1586 inertia, its restricted action and finite-dimensional Euler denominator agree.
1587 Twisting again by $-t$ recovers the datum with $N$ still supplied.
1588 
1589 Block 13 also established an extracted inverse on the explicit class $N^3=0$:
1590 \[
1591 \log_2 U=(U-I)-\tfrac12(U-I)^2,\qquad
1592  a^{-1}\log_2(\exp(aN))=N\quad(a\ne0).
1593 \]
1594 Both exponential/logarithmic inverse identities are checked on the cubic
1595 nilpotent and unipotent loci. If a supplied common sample $u$ has
1596 $r_D(u)=r_E(u)=I$ and $t(u)\ne0$, an intertwiner of the reconstructed cubic
1597 actions recovers both original group equivariance and monodromy equivariance.
1598 The general nilpotence exponential theorem is not restricted to this cubic
1599 class, but the extracted inverse in Block 13 was. Block 20 below removes
1600 that restriction by using the full finite logarithm.
1601 
1602 The rational affine-group example has $u=(1,1)$, $d=(0,1/3)$ and
1603 \[
1604 \rho(u)=\begin{pmatrix}1&1&1/2\\0&1&1\\0&0&1\end{pmatrix},
1605 \qquad \rho(d)=\operatorname{diag}(1,3,9).
1606 \]
1607 Reversing the factor order or dropping the quadratic term gives checked
1608 failures. For the length-four chain, the quadratic logarithm has erroneous
1609 $e_3$-to-$e_0$ coefficient $-1/3$, so its cubic restriction is substantive.
1610 A zero-parameter sample also fails to recover $N$.
1611 
1612 No arithmetic group, tame cocycle or required sample is constructed by these
1613 statements. The attached comparison for every intended representation,
1614 coefficient comparisons and Hodge--Tate/period data remain separate. Finite
1615 inertia image and an open inertia kernel of $r$ are not asserted to persist
1616 under this twist to $\rho$. Claim 9.2 remains partial.
1617 
1618 \section{Finite spectral occupancy}
1619 
1620 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.
1621 
1622 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
1623 \[
1624 e_i
1625 =
1626 \prod_{\mu\in\Spec(T_i)\setminus\{a_i\}}
1627 \frac{T_i-\mu I}{a_i-\mu},
1628 \qquad
1629 e_T=\prod_{i=1}^{N}e_i,
1630 \]
1631 with \(e_i=0\) if \(a_i\) is absent.
1632 
Statement: Exact finite occupancy trace · Go to proof · Read statement and proof side by side1633 \begin{theorem}[Exact finite occupancy trace]\label{px:10.1}
1634 The operator \(e_T\) is the projector onto the joint eigenspace
1635 \[
1636 A_T
1637 =
1638 \{v:T_iv=a_iv\text{ for every }i\}.
1639 \]
1640 Moreover,
1641 \[
1642 \boxed{
1643 \Tr(e_T)=\rank(e_T)=\dim A_T\in\Z_{\ge0}.
1644 }
1645 \]
1646 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.
1647 \end{theorem}
1648 
Proof block: Exact finite occupancy trace · Go to statement · Read statement and proof side by side1649 \begin{proof}
1650 For each operator, its finite set of actual eigenvalues is used without
1651 multiplicity. The polynomial
1652 \[
1653  p_{i,a}(X)=\prod_{\mu\in\Spec(T_i)\setminus\{a\}}
1654  (a-\mu)^{-1}(X-\mu)
1655 \]
1656 is used when $a$ occurs, and the zero polynomial otherwise. For an eigenvector
1657 $T_i v=bv$, evaluation gives
1658 \[
1659  p_{i,a}(T_i)v=\begin{cases}v&b=a,\\0&b\ne a.\end{cases}
1660 \]
1661 Because the eigenspaces span $A$, this proves that $e_i=p_{i,a_i}(T_i)$ maps
1662 all of $A$ into the selected eigenspace and fixes that eigenspace pointwise.
1663 It therefore proves the individual projector and image assertions, including
1664 an absent target.
1665 
1666 Polynomials in commuting operators commute. If projections $P,Q$ onto
1667 $U,W$ commute, then $PQ$ maps into both $U$ and $W$, and fixes every vector
1668 in $U\cap W$. Induction proves that the actual ordered product $e_T$ is a
1669 projection onto $A_T$; commutation also makes the result independent of the
1670 ordering. An empty list of conditions gives the identity.
1671 
1672 For a projection onto a subspace, the direct sum of its image and kernel
1673 identifies it with $I\oplus0$. Thus its trace in $E$ is the natural dimension
1674 of its image cast into $E$. In characteristic zero this cast is injective,
1675 so there is a unique natural integer represented by the trace. That integer
1676 is positive exactly when the joint eigenspace contains a nonzero vector.
1677 \end{proof}
1678 
1679 \paragraph{Naturality and finite hypotheses.}
1680 If $F T_i=U_i F$ and the source operators split, then
1681 $F e_{T,a}=e_{U,a}F$. This follows first on source eigenvectors and then on
1682 their span. In particular, a change of basis conjugates the constructed
1683 projector and preserves its trace. Adding conditions decreases the actual
1684 joint eigenspace and cannot increase its dimension. These statements do not
1685 assume an orthonormal basis or a positive definite inner product.
1686 
1687 \paragraph{A specified finite realization.}
1688 On $\Q^4$, take the diagonal operators with diagonal lists
1689 \[
1690 (1,1,1,0),\quad(2,2,0,0),\quad(3,0,0,0),\quad(0,4,4,4)
1691 \]
1692 and target scalars $(1,2,3,4)$. All four targets occur individually. Imposing
1693 these conditions successively gives actual projector ranks $3,2,1,0$.
1694 The last packet is empty despite individual feasibility. The formal code
1695 checks these operators, projector formulas, traces and dimensions. This is
1696 a newly specified realization, not a claim to have recovered the original
1697 companion implementation.
1698 
1699 \paragraph{Why the hypotheses cannot be omitted.}
1700 For
1701 \[
1702  P=\begin{pmatrix}1&0\\0&0\end{pmatrix},\qquad
1703  Q=\tfrac12\begin{pmatrix}1&1\\1&1\end{pmatrix},
1704 \]
1705 each operator is idempotent, but $PQ$ is not idempotent and has trace $1/2$.
1706 For the Jordan block $J=\left(\begin{smallmatrix}1&1\\0&1\end{smallmatrix}\right)$,
1707 the singleton-spectrum Lagrange polynomial is $1$, so the formula produces
1708 the identity although the eigenspace at $1$ is only a line. Both failures
1709 are exact formal counterexamples to dropping the corresponding hypotheses,
1710 not counterexamples to the theorem with those hypotheses retained.
1711 
1712 
1713 \begin{figure}[H]
1714 \centering
1715 \includegraphics[width=0.77\linewidth]{15_finite_occupancy_ranks.pdf}
1716 \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.}
1717 \end{figure}
1718 
Statement: Universal occupancy1719 \begin{conjecture}[Universal occupancy]\label{px:10.2}
1720 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.
1721 \end{conjecture}
1722 
1723 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.
1724 
1725 \section{A conditional system-completion criterion}
1726 
1727 The preceding results can be assembled without promoting their missing hypotheses to theorems.
1728 
Statement: Residual-system completion criterion · Go to proof · Read statement and proof side by side1729 \begin{theorem}[Residual-system completion criterion]\label{px:11.1}
1730 Fix an admissible arithmetic class.  Suppose:
1731 \begin{enumerate}
1732 \item every object has a unique residual root in an exhaustive residual moduli space;
1733 \item a common algebraic spine is defined for the desired system;
1734 \item every coefficient-prime residual companion exists;
1735 \item every companion forest has nonempty finite levels, finite branching, and inverse-limit closed local conditions;
1736 \item the required horizontal transports preserve the common spine and the selected local deformation conditions.
1737 \end{enumerate}
1738 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.
1739 \end{theorem}
1740 
Proof block: Residual-system completion criterion · Go to statement · Read statement and proof side by side1741 \begin{proof}
1742 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.
1743 \end{proof}
1744 
Statement: Exact location of the remaining existence problem1745 \begin{corollary}[Exact location of the remaining existence problem]\label{px:11.2}
1746 Inverse-limit reconstruction alone is not a nonemptiness theorem.  The existence requirements must retain both residual companions and liftability through every finite depth:
1747 \[
1748 \boxed{
1749 \begin{aligned}
1750 \text{companion existence: }&X_{\lambda,1}(\Compat)\ne\varnothing
1751 \text{ for every }\lambda;\\
1752 \text{finite-depth liftability: }&X_{\lambda,m}(\Compat)\ne\varnothing
1753 \text{ for every }\lambda,m\ge2;\\
1754 \text{finite occupancy: }&\Tr(e_T)>0
1755 \text{ for every required global packet.}
1756 \end{aligned}}
1757 \]
1758 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.
1759 \end{corollary}
1760 
1761 
1762 \paragraph{An occupied node can have no child.}
1763 The actual order-two representation with generator
1764 \[
1765  A=\begin{pmatrix}1&2\\2&3\end{pmatrix}\pmod4
1766 \]
1767 satisfies $A^2=I$ and $\det(XI-A)=X^2-1$. It has no lift modulo $8$ with
1768 the same characteristic polynomial. Indeed, every lift has entries congruent
1769 to $1,2,2,3$ modulo $4$. Trace zero then forces its determinant to be $3$
1770 modulo $8$, whereas $X^2-1$ requires determinant $-1=7$ modulo $8$.
1771 Both the occupied node and the absence of any next-level matrix or representation
1772 with the prescribed polynomial are Lean-checked. Other branches of the same
1773 unrestricted involution forest survive, so this example does not contradict
1774 finite-branch compactness.
1775 
1776 \paragraph{Local properties need their own limit argument.}
1777 Over a domain, for a nonzero $\pi\in I$, the representations of the additive
1778 integer group given by
1779 \[
1780  \rho_n(g)=\begin{pmatrix}1&\pi^n g\\0&1\end{pmatrix}
1781 \]
1782 are all nontrivial and converge pointwise in the ideal-adic topology to the
1783 trivial representation. The convergence and the failure of limit preservation
1784 for nontriviality are formally checked. Thus not every property of approximating
1785 integral representations can be asserted for a limit. This example is not
1786 claimed to disprove stability for any particular intended Galois local condition.
1787 
1788 \paragraph{Complete conditional existence boundary (Block 24).}
1789 The eleventh block established the corresponding conditional matrix criterion.
1790 Block 24 now uses the complete common-spine conclusion of Claim 8.2: the returned
1791 coefficient-field representations are continuous, have the prescribed common
1792 polynomials and coefficient-specific determinants, and satisfy every selected
1793 local realization relation under the stated inverse-limit closure hypothesis.
1794 All finite reductions belong to the admissible classes.
1795 
1796 For each supplied required packet $p$, let $A_p$ be its finite-dimensional carrier
1797 over a characteristic-zero field $E_p$, and let $e_p$ be the actual joint spectral
1798 projector for its finite list of split commuting conditions. No order on $E_p$
1799 is assumed. The source notation $\Tr(e_p)>0$ means that the unique natural number
1800 $n_p$ with $\Tr(e_p)=(n_p:E_p)$ is positive. The checked projector formula identifies
1801 $n_p$ with the dimension of the actual joint eigenspace.
1802 
1803 An admissible realization here includes continuous coefficient-field members and
1804 membership of every finite reduction in its designated admissible class.
1805 Under the completion hypotheses and these supplied carrier hypotheses, Lean proves
1806 \[
1807 \begin{aligned}
1808 &\exists\,\rho,\ (x_p)_p:\quad
1809   \rho\text{ is an admissible realization of the full chosen spine},\quad
1810   0\ne x_p\in\operatorname{im}(e_p)\text{ for every }p\\
1811 &\quad\Longleftrightarrow\quad
1812  \bigl(\forall\lambda,\ X_{\lambda,1}(\Compat)\ne\varnothing\bigr)
1813  \ \land\ \bigl(\forall\lambda,\ \forall m\ge2,
1814                X_{\lambda,m}(\Compat)\ne\varnothing\bigr)
1815  \ \land\ \bigl(\forall p,\ n_p>0\bigr).
1816 \end{aligned}
1817 \]
1818 The packet index may be infinite. Each $x_p$ belongs to its own supplied carrier;
1819 no common vector across distinct carriers or embedding of the reconstructed
1820 system into those carriers is asserted. Neither an unknown carrier nor positive
1821 trace is constructed without the corresponding hypotheses.
1822 
1823 This completes Claim 11.2 at its conditional source scope, on the same counting
1824 basis used for Claim 8.2 in Block 23. The full arithmetic application premises
1825 remain separate. In particular, the criterion does not prove universal occupancy,
1826 Hodge--Tate or Weil--Deligne attachment, or the Frobenius recovery clause of
1827 Claim 11.1. The latter still depends on the partial Claims 9.1 and 9.2.
1828 
1829 \paragraph{Every required packet is necessary.}
1830 For each omitted index $N\in\mathbb N$, consider one-dimensional rational carriers
1831 with the identity operator, requiring eigenvalue $0$ at $N$ and eigenvalue $1$
1832 at every other index. The actual spectral projector has trace $0$ at $N$ and
1833 trace $1$ elsewhere. Lean proves that any predetermined finite sample of packet
1834 indices can miss an empty required packet: choose $N$ outside that sample.
1835 The family depends on the omitted index. This does not assert that one fixed
1836 family passes every finite prefix while failing global occupancy.
1837 
Statement: Natural finite seed rank1838 \begin{conjecture}[Natural finite seed rank]\label{px:11.3}
1839 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.
1840 \end{conjecture}
1841 
1842 \section{Worked finite models}
1843 
1844 \subsection{Smooth branch}
1845 
1846 For \(q=3\) and formal dimension \(d=2\), the finite levels have cardinalities
1847 \[
1848 1,9,81,729,6561,\ldots.
1849 \]
1850 The seed zeta function is
1851 \[
1852 Z(T)=\frac{T}{1-9T}.
1853 \]
1854 
1855 \subsection{Weighted dyadic chart}
1856 
1857 For weights \((1,2,4)\), the counts are
1858 \[
1859 1,2,8,32,256,2048,\ldots.
1860 \]
1861 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
1862 \[
1863 Z_{(1,2,4)}(T)
1864 =
1865 \frac{T(1-6T-8T^2-32T^3)}{1-8T}.
1866 \]
1867 The negative signs in this presentation arise from moving the denominator to \(1-8T\); every power-series coefficient is positive.
1868 
1869 \subsection{Singular branch}
1870 
1871 For \(x^2=0\) over a residue field of size three, the counts are
1872 \[
1873 1,3,3,9,9,27,27,81,\ldots,
1874 \]
1875 and
1876 \[
1877 Z(T)=\frac{T+3T^2}{1-3T^2}.
1878 \]
1879 The exact branching dimension is \(1/2\).
1880 
1881 \subsection{Directed transport}
1882 
1883 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.
1884 
1885 \begin{figure}[H]
1886 \centering
1887 \includegraphics[width=0.84\linewidth]{16_proof_status.pdf}
1888 \caption{The finite and formal statements proved in this paper are separated from the two remaining universal existence assertions.}
1889 \label{fig:proof-status}
1890 \end{figure}
1891 
1892 \section{Computational certificates}
1893 
1894 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.
1895 
1896 \begin{table}[H]
1897 \centering
1898 \caption{Selected exact certificates.}
1899 \begin{tabular}{lr}
1900 \toprule
1901 Certificate & Result\\
1902 \midrule
1903 Residual packet count in the mod-three model & 3\\
1904 Compatible base-five inverse-limit branch & yes\\
1905 First dyadic sign separation depth & 2\\
1906 Source strongly connected components & 3\\
1907 Brute-force minimum directed seed count & 3\\
1908 Cohomology packet reconstruction residual & 0\\
1909 Compatible common-spine test & passed\\
1910 Inconsistent spine detected & yes\\
1911 Recovered carrier multiplicities & \((2,0,1)\)\\
1912 Finite occupancy ranks & \((3,2,1,0)\)\\
1913 \bottomrule
1914 \end{tabular}
1915 \end{table}
1916 
1917 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.
1918 
1919 \section{Claim ledger}
1920 
1921 \begin{longtable}{p{0.34\linewidth}p{0.18\linewidth}p{0.40\linewidth}}
1922 \toprule
1923 Statement & Status & Scope or boundary\\
1924 \midrule
1925 \endfirsthead
1926 \toprule
1927 Statement & Status & Scope or boundary\\
1928 \midrule
1929 \endhead
1930 Residual partition & proved & any moduli functor with well-defined reduction\\
1931 No crossing & proved & operations trivial at residual depth\\
1932 Inverse-limit reconstruction & proved & represented complete deformation problem\\
1933 Finite-branch compactness & proved & finite nonempty levels and finite branching\\
1934 Smooth and weighted seed zeta formulas & proved & stated formal coordinate models\\
1935 Singular power zeta and dimension & proved & scalar equation \(x^e=0\)\\
1936 Cohomology packet decomposition & proved & chain projectors commuting with the differential\\
1937 Directed minimum-seed theorem & proved & finite directed transport graph\\
1938 Adelic finite-depth completion & proved & common spine, all finite levels occupied, closed local conditions\\
1939 Compatible-carrier summand completion & proved & known semisimple compatible carrier and finite separation\\
1940 Finite occupancy trace & Lean checked & supplied commuting split operators; characteristic-zero trace criterion\\
1941 Universal residual companions & not proved & requires nonempty root at every coefficient prime\\
1942 Universal compatible-system completion & not proved & algebraic spine and companion occupancy remain necessary\\
1943 Universal automorphic occupancy & not proved & requires positive global packet traces\\
1944 Unrestricted reciprocity & not claimed & belongs to later local and global papers\\
1945 \bottomrule
1946 \end{longtable}
1947 
1948 \section{Conclusion}
1949 
1950 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:
1951 \[
1952 \boxed{
1953 \text{residual roots}
1954 \longrightarrow
1955 \text{finite deformation levels}
1956 \longrightarrow
1957 \text{inverse-limit branches}.
1958 }
1959 \]
1960 
1961 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.
1962 
1963 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 paper 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.
1964 
1965 \appendix
1966 
1967 \section{Algorithms implemented in the companion package}
1968 
1969 \subsection{Residual towers}
1970 
1971 The residual module partitions coordinates modulo \(p\), verifies compatibility
1972 \[
1973 x_{m+1}\equiv x_m\pmod{p^m},
1974 \]
1975 and reconstructs the digit \(a_{m-1}\) by
1976 \[
1977 a_{m-1}=\left\lfloor\frac{x_m}{p^{m-1}}\right\rfloor\pmod p.
1978 \]
1979 
1980 For canonical representatives $0\le x_m<p^m$, set $x_0=0$. Compatibility also gives
1981 $a_{m-1}=(x_m-x_{m-1})/p^{m-1}\in\{0,\ldots,p-1\}$.
1982 The floor in the first formula is essential. For example, the compatible
1983 base-five residues $4,19$ give the second digit $3$, not the rational number $19/5$.
1984 The executable companion already uses integer floor division. This edition
1985 corrects the displayed algorithm, not the implementation.
1986 
1987 \subsection{Transport condensation}
1988 
1989 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.
1990 
1991 \subsection{Companion forests}
1992 
1993 For an integral polynomial \(f\), the finite root forest is obtained by exact enumeration of
1994 \[
1995 f(x)\equiv0\pmod{p^m}
1996 \]
1997 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.
1998 
1999 \subsection{Cohomology packets}
2000 
2001 Modular Gaussian elimination computes the ranks of the differentials.  For
2002 \[
2003 C^{i-1}\xrightarrow{d_{i-1}}C^i\xrightarrow{d_i}C^{i+1},
2004 \]
2005 the finite dimension is evaluated as
2006 \[
2007 \dim H^i
2008 =
2009 \dim C^i-\rank d_i-\rank d_{i-1}.
2010 \]
2011 Packet subcomplexes are computed separately and checked against the total.
2012 
2013 \subsection{Finite occupancy}
2014 
2015 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.
2016 
2017 \section{Reproducibility boundary}
2018 
2019 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 release is designed to make every finite example and every displayed count independently reproducible without confusing computation with proof.
2020 
2021 
2022 \section*{Historical Block 27 formalization boundary}
2023 The following checkpoint discussion belongs to the Block 27 source. Its statements
2024 of partial status are not the live ledger of this edition. The later conditional
2025 contract is stated in Appendix~\ref{sec:conditional-final}. The original frontmatter
2026 for that checkpoint is preserved here before the detailed development.
2027 \input{historical_checkpoint_frontmatter.tex}
2028 \paragraph{Retained checkpoint discussion.}
2029 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.
2030 
2031 The cumulative ledger contains seventeen checked source proof claims and three partial claims, with no untouched proof claims. Block 27 removes the finite-number-field restriction and Frobenius-choice attachment gaps, while general prescribed-conjugacy prime coverage remains unproved. Exact finite occupancy is checked. Claims 8.2 and 11.2 are complete at their conditional source scope, with arithmetic application premises still unproved in general. Claim 11.2 retains every residual level, every higher depth, and every required supplied packet; it does not prove their nonemptiness or positive trace unconditionally. Claims 9.1, 9.2, and 11.1 retain the gaps recorded in the current ledger. Block 25 proves the general system-to-member bridge under overlap density and the full finite cyclotomic arithmetic separation case, with actual unramified Frobenius primes supplied. General absolute-Galois Frobenius coverage remains unfinished. Blocks 21--22 identify one actual quadratic arithmetic packet with its coordinate-ring points and prove its conditional finite-depth completion with actual simultaneous local-triviality conditions. The p-adic criterion is proved at every arithmetic prime. The packet characters are trivial on actual valuation inertia at odd primes; identification of its decomposition group with the full local Galois group remains open here, and ramification at two is not proved. These results do not identify every packet in the common arithmetic spine or attach Hodge--Tate and Weil--Deligne invariants. General nilpotent logarithmic recovery remains checked under its stated sample hypotheses. Universal occupancy and natural finite seed rank remain conjectures. The original companion package has not been rerun. The release provides separate exact checks and cumulative compiler evidence. No new PDF was typeset.
2032 
2033 
2034 \paragraph{Finite-group comparison with precision loss (Block 17).}
2035 Let $R$ be a commutative domain, $\Gamma$ a finite group, and $\rho,\tau$
2036 actual integral matrix representations. Suppose $a=|\Gamma|\ne0$ in $R$ and
2037 $a\mid\pi^e$. An equivariant matrix modulo $(\pi)^{e+k}$ lifts to an
2038 integral equivariant matrix with the prescribed reduction modulo $(\pi)^k$.
2039 Indeed, lift its entries to $A$ and form
2040 \[
2041 S=\sum_{g\in\Gamma}\rho(g)A\tau(g^{-1}).
2042 \]
2043 The finite equations imply $S-aA=\pi^{e+k}E$ with $E$ integral. Choose $b$
2044 with $\pi^e=ab$ and put $P=A+b\pi^kE$. Then $aP=S$, so cancellation of
2045 $a\ne0$ proves equivariance. Over a local ring, if $\pi$ is a nonunit,
2046 $k>0$ and the supplied comparison is invertible, $P$ is an integral unit.
2047 Neither completeness nor a finite residue field is needed for this step.
2048 
2049 For a DVR, $e=v_\pi(|\Gamma|)$ is derived from the actual group order.
2050 The single precision $e+1$, independent of rank, detects integral
2051 isomorphism. It makes reduction injective on integral isomorphism classes,
2052 and finite coefficient quotients give finitely many integral classes in
2053 fixed rank. This is a formalization of classical finite-group rigidity
2054 (Maranda, 1953, Theorem~2), with an explicit proof of the comparison's
2055 precision loss.
2056 
2057 For complete local coefficients with finite quotients, downward-compatible
2058 allowed representations occupied at every precision, and the required
2059 finite-group type at depth $e+1$, reconstruction followed by this comparison
2060 produces the required integral representation. Continuity is proved for a
2061 finite discrete source and for pullback through a fixed continuous map to
2062 that source. Occupancy at only one precision is insufficient. The result
2063 lifts comparisons between actual integral representations; it does not lift
2064 arbitrary quotient representations or supply the missing arithmetic packet
2065 interpretation.
2066 
2067 For $C_2$ over $\mathbb Z_2$, take
2068 \[
2069 \tau(g)=\begin{pmatrix}1&0\\0&-1\end{pmatrix},\qquad
2070 \rho(g)=\begin{pmatrix}1&2\\0&-1\end{pmatrix},\qquad
2071 A=\begin{pmatrix}1&1\\0&1\end{pmatrix}.
2072 \]
2073 The matrix $A$ intertwines modulo $4$ and its average is
2074 $P=\left(\begin{smallmatrix}1&-1\\0&1\end{smallmatrix}\right)$.
2075 No exact intertwiner can retain $A$ modulo $4$, although $P$ retains it
2076 modulo $2$. The actual trivial and sign representations also agree modulo
2077 $2$ but are not integrally isomorphic. These checked examples show why
2078 residual-only detection and full preservation of the input precision cannot
2079 be asserted here.
2080 
2081 
2082 \paragraph{Lifting a summand inside a supplied finite-group carrier (Block 18).}
2083 Let $R$ be a commutative integral domain complete and separated for the
2084 $(\pi)$-adic filtration. Let $\Gamma$ be a finite group, and let
2085 $\rho:\Gamma\to\mathrm{GL}_n(R)$ be an actual integral representation.
2086 Assume that $a=|\Gamma|\ne0$ in $R$ and $a\mid\pi^e$. For $k>0$, suppose
2087 \[
2088 \bar E\in M_n\bigl(R/(\pi)^{e+k}\bigr),\qquad
2089 \bar E^2=\bar E,\qquad
2090 \bar\rho(g)\bar E=\bar E\bar\rho(g)\quad(g\in\Gamma).
2091 \]
2092 There is an actual integral matrix $E$ satisfying
2093 \[
2094 E^2=E,\qquad \rho(g)E=E\rho(g),\qquad
2095 E\bmod(\pi)^k=\bar E\bmod(\pi)^k.
2096 \]
2097 No integral summand or coherent family of quotient projectors is assumed.
2098 No local-ring assumption or finiteness of the residue field is needed.
2099 
2100 To prove this, apply the preceding averaging correction with both
2101 representations equal to $\rho$. This produces an exact equivariant matrix
2102 $A$ with the prescribed reduction at depth $k$, so that
2103 $A^2-A\in(\pi)^kM_n(R)$. Averaging alone need not preserve idempotence.
2104 Use the integral polynomial
2105 \[
2106 f(A)=3A^2-2A^3.
2107 \]
2108 The identities
2109 \[
2110 f(A)-A=(1-2A)(A^2-A),\qquad
2111 f(A)^2-f(A)=(A^2-A)^2(4A^2-4A-3)
2112 \]
2113 show that successive corrections preserve the retained reduction and improve
2114 the idempotence defect. In these formulas scalar constants denote scalar
2115 matrices. The Lean proof establishes at least one additional ideal digit at
2116 each step, constructs the resulting compatible family of finite-level matrices, and uses
2117 completeness and separatedness to recover $E$. Every matrix commuting with
2118 $A$ commutes with $E$. There is no division by $2$, so the correction also
2119 works in residue characteristic $2$.
2120 
2121 The actual submodules $U=\operatorname{im}E$ and $W=\ker E$ are invariant,
2122 and addition gives an equivariant isomorphism
2123 \[
2124 U\oplus W\simeq R^n.
2125 \]
2126 The inclusion $i:U\hookrightarrow R^n$ and retraction $r(v)=Ev$ are
2127 constructed as linear maps and satisfy $ri=1_U$ and $ir=E$. Their
2128 equivariance is proved. Coordinatewise reduction maps $U$ onto
2129 $\operatorname{im}(\bar E\bmod(\pi)^k)$ and maps $W$ onto
2130 $\ker(\bar E\bmod(\pi)^k)$. Both equalities are surjectivity statements
2131 onto the actual submodules over the finite-level quotient, not merely containment. The same
2132 projector defines a summand after pullback through any group homomorphism
2133 to $\Gamma$.
2134 
2135 For $R=\mathbb Z_2$ and the sign carrier
2136 $\rho(s)=\operatorname{diag}(1,-1)$, the projector
2137 \[
2138 \bar E=\begin{pmatrix}1&2\\0&0\end{pmatrix}\pmod4
2139 \]
2140 is equivariant and the theorem constructs a nonzero proper equivariant
2141 projector retaining its reduction modulo $2$. No exact equivariant
2142 endomorphism retains this prescribed matrix modulo $4$. At the insufficient
2143 input depth $1$, the projector
2144 $\left(\begin{smallmatrix}1&1\\0&0\end{smallmatrix}\right)\pmod2$
2145 has no exact equivariant lift retaining its reduction. These are statements
2146 about the supplied carrier and prescribed projectors, not about nonexistence
2147 of all integral summands.
2148 
2149 This block constructs one summand and its complement inside a supplied
2150 finite-group carrier. It advances the carrier step in Claim 9.2. It does
2151 not identify the intended arithmetic packets, construct the arithmetic
2152 Weil--Deligne attachment, establish the Hodge--Tate comparisons, or prove
2153 universal occupancy. At the Block 18 checkpoint, the ledger recorded fifteen
2154 checked claims and five partially formalized claims; see the Block 23
2155 conditional-scope correction above.
2156 
2157 
2158 \paragraph{Simultaneous projector-family lifting and rigidity (Block 19).}
2159 Keep the complete domain, supplied finite-group carrier and group-order
2160 hypotheses of Block 18. Let $J$ be any finite label set and $k>0$. Suppose
2161 $(\bar E_i)_{i\in J}$ is a complete orthogonal family of equivariant
2162 idempotents modulo $(\pi)^{e+k}$. There exists an integral equivariant
2163 family $(E_i)_{i\in J}$ satisfying
2164 \[
2165 E_i^2=E_i,\qquad E_iE_j=0\ (i\ne j),\qquad
2166 \sum_{i\in J}E_i=1,\qquad
2167 E_i\bmod(\pi)^k=\bar E_i\bmod(\pi)^k.
2168 \]
2169 The loss is at most $e$, independent of $|J|$ and the ambient matrix rank.
2170 There is no local-ring or finite-residue-field hypothesis for existence.
2171 The formal theorem also treats empty label sets whenever their input
2172 equations can hold.
2173 
2174 Average every supplied matrix once. Inductively let $C$ be the complement
2175 of the previously lifted projectors and correct the next averaged matrix
2176 inside the corner defined by $C$. The integral polynomial correction
2177 preserves the retained reduction and commutation with $C$ and the carrier.
2178 Multiplication by $C$ gives the required supported projector. This consumes
2179 no further precision. Once every label has been lifted, the complementary
2180 idempotent reduces to zero at positive depth. Adic separatedness forces it
2181 to vanish, proving the sum-to-identity equation.
2182 
2183 The actual invariant images $U_i=\operatorname{im}E_i$ give an equivariant
2184 linear isomorphism
2185 \[
2186 \bigoplus_{i\in J}U_i\simeq R^n,
2187 \qquad (v_i)_i\longmapsto\sum_i v_i,
2188 \qquad v\longmapsto(E_iv)_i.
2189 \]
2190 Lean represents the finite direct sum by the finite product of the image
2191 submodules. The existing coordinatewise reduction theorem maps every
2192 $U_i$ onto the corresponding reduced projector image. No chosen bases or
2193 unproved freeness of the images are used.
2194 
2195 For rigidity alone, let $R$ be a commutative local ring, let $\pi$ be a
2196 nonunit, and let $E,F$ be complete equivariant families on the same carrier
2197 with $E_i\equiv F_i\pmod{(\pi)^k}$ for every label and $k>0$. Then
2198 \[
2199 U=\sum_{i\in J}F_iE_i,\qquad
2200 U\equiv1\pmod{(\pi)^k},\qquad UE_i=F_iU.
2201 \]
2202 Reduction reflects invertibility in this setting, so $U$ is an integral
2203 unit and $UE_iU^{-1}=F_i$. It commutes with the carrier and induces actual
2204 equivariant isomorphisms $\operatorname{im}E_i\simeq\operatorname{im}F_i$.
2205 This rigidity theorem requires neither a finite acting group, a domain,
2206 nor completeness. More generally a unit-reflecting coefficient map suffices.
2207 The combined result proves existence and uniqueness up to this labeled
2208 conjugacy; exact uniqueness of the matrices is false.
2209 
2210 For the continuous $\mathbb Z_2$ carrier
2211 $\rho(s)=\operatorname{diag}(1,-1,1)$, conjugate the three coordinate
2212 projectors by $1+2e_{01}$ and reduce modulo $4$. They form a complete
2213 equivariant family. The general theorem constructs three nonzero integral
2214 summands retaining this family modulo $2$. No exact equivariant family
2215 retains the whole prescribed family modulo $4$. Separate checked examples
2216 show that independent equivariant idempotent lifts can lose orthogonality,
2217 and that distinct complete families with the same reduction can be related
2218 by the asserted identity-congruent conjugacy.
2219 
2220 Block 19 completes this finite-group projector-family step. The actual
2221 arithmetic packets, Galois-to-Weil--Deligne attachment, coefficient and
2222 Hodge--Tate/period comparisons, and arithmetic Frobenius coverage remain
2223 outside this result. At the Block 19 checkpoint, the ledger recorded fifteen
2224 checked claims and five partial claims; see the Block 23 conditional-scope
2225 correction above. Universal occupancy remains conjectural.
2226 
2227 
2228 \paragraph{General finite logarithmic recovery (Block 20).}
2229 Let $A$ be a rational algebra, without any commutativity assumption on $A$.
2230 For a unipotent element $U$ and a positive integer $d$ satisfying
2231 $(U-1)^d=0$, put
2232 \[
2233 L_d(U)=\sum_{j=1}^{d-1}\frac{(-1)^{j+1}}{j}(U-1)^j.
2234 \]
2235 The value is independent of the chosen annihilating exponent. The finite
2236 logarithm and the nilpotent exponential satisfy
2237 \[
2238 L(\exp N)=N,\qquad \exp(L(U))=U.
2239 \]
2240 Both maps preserve every annihilating exponent, and hence preserve the
2241 exact nilpotency class of $N$ and $\exp(N)-1$, or of $U-1$ and $L(U)$.
2242 The Lean finite sum includes its zero-index term with coefficient zero;
2243 the displayed mathematical sum starts at one. The formal statements also
2244 handle the zero algebra and the exponent-zero case.
2245 
2246 The proof evaluates Mathlib's formal power-series inverse identities at
2247 constant nilpotent series. Such evaluation is exactly a finite polynomial.
2248 For an arbitrary noncommutative ambient algebra, perform the calculation
2249 inside the commutative subalgebra generated by the element and then apply
2250 its inclusion. No analytic convergence or topology is assumed. The
2251 finite logarithm commutes with ring homomorphisms between rational algebras.
2252 
2253 Let $K$ be a characteristic-zero field and $N$ an endomorphism with
2254 $N^d=0$. For $t\ne0$ the actual recovery formula is
2255 \[
2256 N=\frac1t\sum_{j=1}^{d-1}\frac{(-1)^{j+1}}{j}
2257        \bigl(\exp(tN)-1\bigr)^j.
2258 \]
2259 All coefficients lie in $K$. The vector spaces need not be finite
2260 dimensional, but nilpotence still means that some finite power of the
2261 whole operator is zero. A linear map intertwines two nilpotent operators exactly
2262 when it intertwines their exponential samples at a common nonzero
2263 parameter. Also
2264 \[
2265 \ker\bigl(\exp(tN)-1\bigr)=\ker N.
2266 \]
2267 
2268 For supplied covariance data and the twisted cocycle of Block 13, let
2269 $\rho_D(g)=\exp(t(g)N_D)r_D(g)$. If a common element $u$ satisfies
2270 $r_D(u)=r_E(u)=1$ and $t(u)\ne0$, every intertwiner of $\rho_D$ and
2271 $\rho_E$ recovers both the original $r$-intertwiner and the $N$-intertwiner.
2272 There is no cubic nilpotence restriction. This recovers equivariant
2273 projectors for both original components. Reconstructed-action isomorphisms
2274 induce actual isomorphisms of the inertia-fixed monodromy kernels. Their local characteristic polynomials
2275 agree under the existing finite-dimensional and normal-subgroup hypotheses.
2276 
2277 For actual finite original inertia images the common kernel sample is
2278 derived. Suppose $u\in H$ satisfies $\nu(u)=1$ and $t(u)\ne0$ and both
2279 $r_D(H)$ and $r_E(H)$ are finite. Their sampled actions have positive
2280 finite orders $a,b$. At $u^{ab}$ both original actions are trivial, and
2281 \[
2282 t(u^{ab})=(ab)t(u)\ne0
2283 \]
2284 by the cocycle identity and characteristic zero. Thus the same full
2285 intertwiner equivalence holds using the actual finite-image hypotheses,
2286 without a separately supplied common trivial-action sample. The initial
2287 nonzero cocycle sample and the arithmetic interpretation of the data
2288 remain requirements.
2289 
2290 Actual affine representations with monodromy chains of every finite
2291 length invoke these theorems. In particular a length-six example has
2292 $N^5\ne0$ and $N^6=0$ and is recovered from its actual reconstructed action.
2293 The length-four example still defeats the old quadratic logarithm, while
2294 the full finite logarithm recovers it.
2295 
2296 The sample hypotheses retain substantive content. A zero parameter loses
2297 $N$. For unrestricted supplied algebraic data, one can also absorb
2298 $\exp(tN)$ into $r$ and set the new monodromy to zero; the reconstructed
2299 representation is unchanged. The absorbed original action fails the
2300 required trivial-action sample condition. This is a counterexample in the
2301 algebraic datum class, not a failure of uniqueness of arithmetic
2302 Weil--Deligne attachment with finite original inertia action.
2303 
2304 Block 20 removes the general logarithmic-extraction gap from the local
2305 algebraic comparison. It does not construct the actual arithmetic
2306 attachment, identify every intended packet, prove the coefficient and
2307 Hodge--Tate/period comparisons, or prove arithmetic Frobenius coverage.
2308 At the Block 20 checkpoint, the ledger recorded fifteen checked claims
2309 and five partial claims; see the Block 23 scope correction above.
2310 
2311 
2312 
2313 \paragraph{Interpreted quadratic arithmetic completion (Block 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 Block 21 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 Block 21. The full
2405 manuscript still requires its remaining packet identifications and
2406 arithmetic comparisons. At the Block 21 checkpoint, the ledger recorded
2407 fifteen checked claims and five partial claims; see the Block 23 conditional-scope
2408 correction above. Universal positive occupancy remains conjectural.
2409 
2410 \paragraph{Actual quadratic local conditions and completion (Block 22).}
2411 Continue with the fixed packet $\mathcal P_q$ above. For a
2412 characteristic-zero field $K$, let
2413 \[
2414 j_K:G_K\longrightarrow G_{\Q}
2415 \]
2416 be the actual field-induced homomorphism between absolute Galois groups.
2417 It includes a chosen embedding of algebraic closures. Let $i_K$ be the
2418 image of the chosen square root $i$ under that embedding. Lean proves
2419 compatibility with the Galois actions and hence
2420 \[
2421 (q\circ j_K)(\sigma)=1
2422 \quad\Longleftrightarrow\quad \sigma(i_K)=i_K.
2423 \]
2424 The fixed-field theorem for the algebraic closure then gives
2425 \[
2426 q\circ j_K=1
2427 \quad\Longleftrightarrow\quad
2428 \exists x\in K,\ x^2=-1.
2429 \]
2430 If no such root exists, the local quotient is surjective onto $C_2$.
2431 These are statements about the actual local Galois map, not a supplied
2432 arithmetic interpretation of a scalar label.
2433 
2434 For every commutative coefficient ring $B$ and $\chi\in\mathcal P_q(B)$,
2435 define $\chi_K=\chi\circ j_K$. The local character is continuous and
2436 commutes with coefficient change. The precise local admissibility
2437 condition is
2438 \[
2439 \operatorname{LocallyTrivial}_K(\chi)
2440 \quad\Longleftrightarrow\quad \chi_K=1.
2441 \]
2442 Descent through the fixed quadratic quotient proves
2443 \[
2444 \operatorname{LocallyTrivial}_K(\chi)
2445 \quad\Longleftrightarrow\quad
2446 \bigl(\exists x\in K,\ x^2=-1\bigr)\ \lor\ \chi=1.
2447 \]
2448 No reducedness, characteristic-zero or domain hypothesis is imposed on
2449 $B$. In particular, the formula applies to the finite coefficient
2450 quotients used in completion.
2451 
2452 The p-adic square-root criterion is proved for every prime:
2453 \[
2454 \bigl(\exists x\in\Q_p,\ x^2=-1\bigr)
2455 \quad\Longleftrightarrow\quad p\equiv1\pmod4.
2456 \]
2457 A root satisfies $\lvert x\rvert_p^2=1$ and is therefore integral.
2458 Reduction modulo three rules out a root in $\Q_3$, and reduction modulo
2459 four rules out a root in $\Q_2$. At an odd prime, any residue root of
2460 $X^2+1$ has nonzero derivative and lifts by the pinned Mathlib Hensel
2461 theorem. The finite-field square criterion then gives the stated
2462 congruence. An explicit Hensel application at the residue root $2$ modulo $5$ supplies
2463 a root in $\Z_5$. Consequently
2464 \[
2465 \boxed{
2466 \operatorname{LocallyTrivial}_{\Q_p}(\chi)
2467 \quad\Longleftrightarrow\quad p\equiv1\pmod4\ \lor\ \chi=1.
2468 }
2469 \]
2470 The arithmetic prime $p$ is independent of the coefficient prime. For
2471 the two integral $\Z_2$-valued characters, the sign character is locally
2472 trivial exactly at primes congruent to one modulo four. Both distinct
2473 global characters are locally trivial at five, while the sign character
2474 is nontrivial on the full local Galois groups at three and two.
2475 
2476 The inertia theorem uses actual residue actions. For a valuation subring
2477 $A$ of an extension field $L/K$, let $D_A$ be its decomposition subgroup
2478 in $\operatorname{Aut}_K(L)$ and put
2479 \[
2480 I_A=\ker\bigl(D_A\longrightarrow\operatorname{Aut}(k_A)\bigr),
2481 \]
2482 where $k_A$ is the residue field. If $2$ is a unit in $A$, every member
2483 of $I_A$ fixes every $y\in L$ with $y^2=-1$. Indeed $y^{-1}=-y$, so
2484 $y$ belongs to $A$ and is a unit there. An automorphism sends $y$ to
2485 $y$ or $-y$. Their residues are distinct because $2$ and $y$ are units,
2486 whereas inertia fixes residues. The second possibility is excluded.
2487 
2488 For every prime $p$, Lean constructs a valuation subring
2489 $A\subseteq\overline{\Q_p}$ containing the integral image of $\Z_p$
2490 such that the induced map $\Z_p\to A$ is local. For odd $p$, two is
2491 a unit. The preceding argument applies to every valuation subring
2492 containing that integral image, and hence every member of
2493 $\mathcal P_q(B)$ is trivial on its inertia subgroup after actual local
2494 restriction. The existence theorem supplies a locally dominating choice,
2495 so this assertion is not vacuous.
2496 
2497 This inertia is the actual residue-action kernel inside $D_A$. No equality
2498 $D_A=G_{\Q_p}$ is established in this block. Nor is ramification at two
2499 proved: the nontrivial full local character there is a separate result.
2500 At three the $\Z_2$-valued sign character is nontrivial on the full local
2501 Galois group but trivial on every inertia subgroup covered by the theorem.
2502 Thus local triviality and the stated inertia triviality are distinguished
2503 by checked arithmetic examples.
2504 
2505 The local conditions survive coefficient completion by a proved theorem.
2506 For an $I$-adically separated commutative ring $R$,
2507 \[
2508 \operatorname{LocallyTrivial}_K(\chi)
2509 \quad\Longleftrightarrow\quad
2510 \operatorname{LocallyTrivial}_K(\chi\bmod I^m)
2511 \text{ for every }m\ge1.
2512 \]
2513 If $-1$ has a square root in $K$, every packet member satisfies the
2514 condition. Otherwise the condition says that the character is globally
2515 trivial, and separatedness detects that equality through all reductions.
2516 This proves the closure statement for the independently defined arithmetic
2517 property.
2518 
2519 Suppose now that $R$ is $I$-adically complete and that every positive
2520 quotient $R/I^m$ is finite. Let $C_m\subseteq\mathcal P_q(R/I^m)$ be
2521 allowed subsets preserved by reduction, and let $(p_s)_{s\in S}$ be any
2522 indexed family of arithmetic primes. The index set $S$ need not be finite.
2523 Lean proves the simultaneous arithmetic completion criterion
2524 \[
2525 \begin{split}
2526 &\exists\chi\in\mathcal P_q(R),\quad
2527  \chi\text{ continuous},\quad
2528  \chi\bmod I^m\in C_m\ (m\ge1),\quad
2529  \chi_{\Q_{p_s}}=1\ (s\in S)\\
2530 &\quad\Longleftrightarrow\quad
2531  \forall m\ge1,\ \exists\psi\in C_m,\quad
2532  \forall s\in S,\ p_s\equiv1\pmod4\ \lor\ \psi=1.
2533 \end{split}
2534 \]
2535 The constructed character also satisfies every odd-prime valuation-inertia
2536 condition stated above. Finite-branch compactness selects all finite
2537 characters together; no coherent branch or surjective transition maps
2538 are assumed. The new local-closure implication is proved, not supplied.
2539 Every-level occupancy remains a substantive hypothesis. One nonsplit
2540 selected prime forces the completed global character to be trivial.
2541 
2542 For the integral dyadic packet, a single detecting precision is also
2543 proved: reduction modulo four detects local triviality uniformly in the
2544 arithmetic prime. Modulo two does not suffice. The sign character is
2545 nontrivial locally at three, while its reduction modulo two is trivial.
2546 This is a coefficient-depth failure, distinct from splitting of the
2547 arithmetic field.
2548 
2549 Block 22 finishes this actual local admissibility and completion step for
2550 the fixed quadratic packet. It does not identify all packets in the
2551 manuscript's common arithmetic spine, attach Weil--Deligne objects, or
2552 prove coefficient and Hodge--Tate/period comparisons. The decomposition
2553 and full local Galois group identification remains a separate inertia
2554 obligation, and ramification at two is not claimed. The full arithmetic
2555 ledger at the Block 22 checkpoint recorded fifteen checked source claims
2556 and five partial claims; the Block 23 conditional-scope correction gives
2557 sixteen checked and four partial.
2558 Universal occupancy and natural finite seed rank remain conjectures.
2559 
2560 \input{residue_continuation_body.tex}
2561 \input{conditional_completion.tex}
2562 \clearpage
2563 \phantomsection
2564 \addcontentsline{toc}{section}{References}
2565 \input{references.tex}
2566 \clearpage
2567 \section{Worked visual atlas}\label{sec:atlas}
2568 The following thirty pages reproduce the worked atlas from the separate visual
2569 guide. They retain their own page labels V1--V30, so the same example has the
2570 same address in either reading route. The two opening contract pages of the
2571 standalone guide are not repeated here.
2572 
2573 The atlas develops exact finite models, not substitutes for universal proofs.
2574 Its first part separates residual roots, coherent branches, and occupied carrier
2575 packets. Its second part studies residue norms, cancellation, Mellin estimates,
2576 and the boundary between a finite calculation and arithmetic occurrence.
2577 The final page records the three distinct historical and current contracts.
2578 
2579 The build script appends these source-built pages after this leaf and copies their
2580 bookmarks and internal links. The mathematical manuscript, its historical
2581 checkpoint statements, and the later conditional assembly remain above.
2582 \end{document}

Back to source controls

Back to Paper X: Universal Residual Seeds and Conditional Occupied-System Completion