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{cont1:paper-ix-finite-polynomial-lifting-and-shared-corrections}{%
2 \subsection{Paper IX: finite polynomial lifting and shared
3 corrections}\label{cont1:paper-ix-finite-polynomial-lifting-and-shared-corrections}}
4 
5 \textbf{Author: Komorebi P. --- 8 September 2026.}
6 
7 This block supplies the actual nonlinear Taylor argument previously
8 missing from the Lean formalization. The statements concern a fixed
9 finite list of integer polynomials. They hold for every positive integer
10 modulus, including composite moduli and modulus one. No
11 Jacobian-surjectivity assumption is needed.
12 
13 \hypertarget{cont1:statement-and-notation}{%
14 \subsubsection{Statement and notation}\label{cont1:statement-and-notation}}
15 
16 Let \[
17 F=(F_1,\ldots,F_e)\in\mathbb Z[X_1,\ldots,X_d]^e,
18 \quad q\ge1,\quad L\ge1,
19 \quad x\in\mathbb Z^d,
20 \quad F(x)\equiv0\pmod{q^L}.
21 \] Write \(R_q=\mathbb Z/q\mathbb Z\), let \(\rho_q\) denote
22 coordinatewise reduction, and put \[
23 r_x=F(x)/q^L\in\mathbb Z^e,
24 \qquad A_x=DF(x):\mathbb Z^d\longrightarrow\mathbb Z^e,
25 \qquad J_x=\rho_q\circ A_x.
26 \] Here \(A_x\) is computed from the actual formal partial derivatives
27 of the input polynomials. The Lean map \(J_x\) has domain
28 \(\mathbb Z^d\) and codomain \(R_q^e\), viewed as integer modules. It
29 factors through reduction to \(R_q^d\); the cokernel below is presented
30 directly using its integer-domain image.
31 
32 Define the finite obstruction module and its distinguished class by \[
33 \mathcal O_x=R_q^e/\operatorname{im}J_x,
34 \qquad o_x=[\rho_q(r_x)]\in\mathcal O_x.
35 \] The checked criterion is \[
36 \boxed{
37  o_x=0
38  \iff
39  \exists y\in\mathbb Z^d:\quad
40  y\equiv x\pmod{q^L},\qquad F(y)\equiv0\pmod{q^{L+1}}.
41 }
42 \] The residual exists by the lower congruence and is unique because
43 \(q>0\). The quotient is finite since its ambient module \(R_q^e\) is
44 finite. The theorem permits zero variables or zero equations as well.
45 
46 \hypertarget{cont1:the-checked-taylor-bridge}{%
47 \subsubsection{The checked Taylor
48 bridge}\label{cont1:the-checked-taylor-bridge}}
49 
50 For every \(P\in\mathbb Z[X_1,\ldots,X_d]\), integer \(a\), and
51 \(x,t\in\mathbb Z^d\), Lean proves \[
52 \boxed{
53  a^2\mid P(x+at)-P(x)-a\sum_{i=1}^{d}(\partial_iP)(x)t_i.
54 }
55 \] The proof uses polynomial induction: constants, addition, and
56 multiplication by a variable. The product rule for the actual partial
57 derivatives controls the multiplication step. It does not assume a
58 Taylor identity or a liftability condition.
59 
60 Taking \(a=q^L\), the inequality \(2L\ge L+1\) gives \[
61 F(x+q^Lt)\equiv q^L(r_x+A_xt)\pmod{q^{L+1}}.
62 \] Since \(q^L\ne0\) in the integers, cancellation in divisibility
63 yields \[
64 F(x+q^Lt)\equiv0\pmod{q^{L+1}}
65 \iff \rho_q(r_x)+J_xt=0.
66 \] Every integer representative of the lower residue has the form
67 \(x+q^Lt\), and this correction equation has a solution exactly when
68 \(o_x=0\).
69 
70 The positive-depth hypothesis is necessary for the general nonlinear
71 theorem. For \(F(X)=X^2-1\), \(q=2\), \(L=0\), \(x=0\), the Jacobian is
72 zero and the residual class is nonzero, yet \(y=1\) is a solution modulo
73 two in the same residue modulo one. Affine systems retain the previously
74 checked \(L\ge0\) theorem.
75 
76 \hypertarget{cont1:independence-of-the-integer-representative}{%
77 \subsubsection{Independence of the integer
78 representative}\label{cont1:independence-of-the-integer-representative}}
79 
80 Suppose \(x'=x+q^Ls\) represents the same lower residue, with exact
81 residual \(r_{x'}\). Polynomial evaluation respects coordinatewise
82 congruences, including when applied to each partial derivative. Hence \[
83 J_{x'}=J_x,
84 \qquad
85 \rho_q(r_{x'})=\rho_q(r_x)+J_xs.
86 \] The two cokernels therefore have the same ambient module and the same
87 defining submodule, and \[
88 [\rho_q(r_{x'})]=[\rho_q(r_x)].
89 \] Lean states this using one explicit common reduced map, avoiding an
90 implicit comparison between differently indexed quotient types. This
91 establishes independence of the integer representative within the fixed
92 polynomial presentation.
93 
94 Changing the polynomial presentation is a separate question. Appending a
95 zero equation can change the raw cokernel by adding a copy of \(R_q\),
96 even though it does not change the solutions.
97 
98 \hypertarget{cont1:two-polynomial-blocks-and-one-shared-lift}{%
99 \subsubsection{Two polynomial blocks and one shared
100 lift}\label{cont1:two-polynomial-blocks-and-one-shared-lift}}
101 
102 Let \(G\in\mathbb Z[X_1,\ldots,X_d]^f\) be a second fixed system with
103 the same variables and the same lower root \(x\). Let
104 \(K_x=\rho_q\circ DG(x)\), and define \[
105 \mathcal C_x=\mathbb Z^d/(\ker J_x+\ker K_x).
106 \] This quotient is finite: it is a quotient of the finite image of
107 \(J_x\), or equivalently of the finite image of \(K_x\).
108 
109 Suppose \(u,v\in\mathbb Z^d\) are separately valid corrections: \[
110 F(x+q^Lu)\equiv0\pmod{q^{L+1}},
111 \qquad
112 G(x+q^Lv)\equiv0\pmod{q^{L+1}}.
113 \] Then \[
114 \boxed{
115 \begin{gathered}
116 [u]=[v]\text{ in }\mathcal C_x
117 \iff
118 \exists y\equiv x\pmod{q^L}:\\
119 F(y)\equiv0\pmod{q^{L+1}},\quad G(y)\equiv0\pmod{q^{L+1}}.
120 \end{gathered}
121 }
122 \] The labels are independent of the choices of valid \(u\) and \(v\).
123 An unconditional version asks for separately valid corrections with
124 equal labels; it does not assume that each block is liftable.
125 
126 Taylor transport turns a common correction \(t\) into the simultaneous
127 equations \(J_xt=J_xu\) and \(K_xt=K_xv\). The previously checked
128 common-quotient theorem gives precisely the displayed equivalence.
129 Separate solvability alone does not imply joint solvability; the
130 controls include \(F(X)=X\), \(G(X)=X-2\), starting at \(x=0\) modulo
131 two and lifting to modulus four.

Back to source controls

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