Realization Calculus

Download original file

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

Read the typeset paper

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

Back to source controls

Back to Realization Calculus