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

Back to source controls

Back to Realization Calculus