Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation

Download original file

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

Read the typeset paper

Read this chapter with formatted equations

1 \hypertarget{cont3:paper-ix-compatible-polynomial-towers-and-p-adic-roots}{%
2 \subsection{Paper IX: compatible polynomial towers and p-adic
3 roots}\label{cont3:paper-ix-compatible-polynomial-towers-and-p-adic-roots}}
4 
5 \textbf{Author: Komorebi P. --- 8 September 2026.}
6 
7 This block completes the nonsingular branch of the passage from one-step
8 polynomial lifting to an infinite compatible tower and an actual p-adic
9 root. Surjectivity is required only of the reduced Jacobian at the
10 initial root. The proof derives its persistence, constructs the tower,
11 proves convergence and verifies the original polynomial equations at the
12 limit.
13 
14 \hypertarget{cont3:main-theorem}{%
15 \subsubsection{Main theorem}\label{cont3:main-theorem}}
16 
17 Let \(p\) be prime, \(L\ge1\), and \[
18 F\in\mathbb Z[X_1,\ldots,X_d]^e,\qquad x\in\mathbb Z^d,
19 \qquad F(x)\equiv0\pmod{p^L}.
20 \] Assume the actual reduced Jacobian \[
21 A_x=DF(x)\bmod p:\mathbb F_p^d\longrightarrow\mathbb F_p^e
22 \] is surjective. Then Lean proves that there is a point \[
23 \boxed{a\in\mathbb Z_p^d,\qquad F(a)=0,\qquad
24  a\equiv x\pmod{p^L}.}
25 \] Here the coefficients of the original integer polynomials are cast
26 into \(\mathbb Z_p\), and their multivariable evaluation is exactly
27 zero. This is an existence theorem for a fixed polynomial presentation
28 with the stated Jacobian hypothesis.
29 
30 The stronger checked statement constructs \(z_n\in\mathbb Z^d\),
31 \(n\ge0\), with \[
32 \begin{aligned}
33 z_0&=x,\\
34 F(z_n)&\equiv0\pmod{p^{L+n}},\\
35 z_{n+1}&\equiv z_n\pmod{p^{L+n}},\\
36 DF(z_n)\bmod p&=A_x,\\
37 z_n&\longrightarrow a\quad\text{in }\mathbb Z_p^d,\\
38 a-z_n&\in p^{L+n}\mathbb Z_p^d.
39 \end{aligned}
40 \] The last inclusion retains every prescribed precision. It is a
41 divisibility lower bound, not an assertion that the error has exactly
42 that valuation. An approximation can already equal the limiting root.
43 
44 \hypertarget{cont3:why-the-single-initial-hypothesis-suffices}{%
45 \subsubsection{Why the single initial hypothesis
46 suffices}\label{cont3:why-the-single-initial-hypothesis-suffices}}
47 
48 The one-step Taylor theorem already supplies the exact correction
49 equation \[
50 b_n+A_{z_n}t=0,\qquad
51 b_n=F(z_n)/p^{L+n}\bmod p.
52 \] Surjectivity supplies a correcting digit for every residual \(b_n\).
53 The chosen correction gives an actual new integer point \(z_{n+1}\),
54 using the proved nonlinear Taylor remainder.
55 
56 Every coordinate change is divisible by \(p^{L+n}\), hence by \(p\).
57 Each formal partial derivative is itself an integer polynomial, so its
58 value is unchanged modulo \(p\). Therefore \[
59 A_{z_{n+1}}=A_{z_n}=A_x.
60 \] The proof assumes no separate surjectivity or solvability statement
61 at later levels. A dependent recursion chooses each next point from the
62 proved one-step existence theorem. It produces one compatible sequence,
63 rather than unrelated witnesses at different precisions.
64 
65 The integer tower construction works more generally for every positive
66 modulus \(q\), including composite \(q\) and \(q=1\), with a surjective
67 map over \(\mathbb Z/q\mathbb Z\). The p-adic completion and the
68 rank-based branching formulas in this block use prime \(p\).
69 
70 \hypertarget{cont3:convergence-and-exact-polynomial-vanishing}{%
71 \subsubsection{Convergence and exact polynomial
72 vanishing}\label{cont3:convergence-and-exact-polynomial-vanishing}}
73 
74 Compatibility implies, for \(m\ge n\), \[
75 p^{L+n}\mid z_m-z_n.
76 \] After casting to \(\mathbb Z_p\), this bounds each coordinate
77 distance by \(p^{-(L+n)}\), so the sequence is Cauchy. Completeness
78 supplies its limit. Closed norm bounds show that the limit retains the
79 congruence at every stage.
80 
81 The generic convergence theorem is proved independently of the
82 polynomial application. It also proves \[
83 p^{L+n}\mid v_n\ \text{for all }n
84 \quad\Longrightarrow\quad v_n\longrightarrow0\text{ in }\mathbb Z_p.
85 \] Apply this to each integer sequence \(F_i(z_n)\). Continuity of
86 multivariable polynomial evaluation also gives \(F_i(z_n)\to F_i(a)\).
87 Uniqueness of limits then yields \(F_i(a)=0\).
88 
89 The cast-evaluation identity is explicitly checked, so the continuous
90 function is the evaluation of the original polynomials. Convergence and
91 polynomial vanishing are conclusions, not assumptions of the main
92 existence theorem.
93 
94 \hypertarget{cont3:exact-number-of-choices-at-each-level}{%
95 \subsubsection{Exact number of choices at each
96 level}\label{cont3:exact-number-of-choices-at-each-level}}
97 
98 Surjectivity implies \[
99 \operatorname{rank}_{\mathbb F_p}A_x=e,\qquad e\le d.
100 \] Combining this with the preceding exact residue-lift count gives \[
101 \boxed{\#\mathcal L_{z_n,L+n}=p^{d-e}\quad\text{for every }n.}
102 \] These are distinct solutions modulo \(p^{L+n+1}\) lying above the
103 selected point modulo \(p^{L+n}\). The original finite obstruction group
104 at each smooth point has cardinality one.
105 
106 The theorem constructs one path through these finite choices. When
107 \(d>e\), it does not claim that all paths have the same limit. The
108 generic uniqueness theorem concerns the limit of a fixed sequence only.
109 
110 \hypertarget{cont3:boundary-controls}{%
111 \subsubsection{Boundary controls}\label{cont3:boundary-controls}}
112 
113 The positive control theorems and rejected invalid proofs cover three
114 distinctions.
115 
116 \begin{enumerate}
117 \def\labelenumi{\arabic{enumi}.}
118 \tightlist
119 \item
120   \textbf{An initial lift does not guarantee an infinite tower without
121   the Jacobian condition.} \(X^2-5\) has the odd lower root modulo two
122   and a lift modulo four, but no root modulo eight. Lean proves that no
123   integer tower can continue through all precisions in this example.
124 \item
125   \textbf{Surjective rectangular Jacobians do not give uniqueness of all
126   roots.} The system \(F(X,Y)=X\) has a surjective Jacobian and distinct
127   dyadic roots \((0,0)\) and \((0,2)\), both in the same residue modulo
128   two.
129 \item
130   \textbf{The retained initial precision cannot be increased without
131   justification.} For \(F(X)=X-2\), zero is a lower root modulo two with
132   surjective derivative, but its exact root two does not retain zero
133   modulo four.
134 \end{enumerate}
135 
136 The controls are theorem checks of these explicit examples. They
137 supplement the universal proof audit and do not replace it.
138 
139 For several polynomial blocks, the hypothesis applies to their combined
140 system. Surjectivity of each block separately does not imply
141 surjectivity of the combined Jacobian or shared liftability. The
142 preceding shared-correction obstruction remains relevant in that
143 situation.

Back to source controls

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation