B.1 Paper IX: finite polynomial lifting and shared corrections
On this page · Permalink · Source line 2
Author: Komorebi P. — 8 September 2026.
This block supplies the actual nonlinear Taylor argument previously missing from the Lean formalization. The statements concern a fixed finite list of integer polynomials. They hold for every positive integer modulus, including composite moduli and modulus one. No Jacobian-surjectivity assumption is needed.
B.1.1 Statement and notation
On this page · Permalink · Source line 14
Let
Write \(R_q=\mathbb Z/q\mathbb Z\), let \(\rho_q\) denote coordinatewise reduction, and put
Here \(A_x\) is computed from the actual formal partial derivatives of the input polynomials. The Lean map \(J_x\) has domain \(\mathbb Z^d\) and codomain \(R_q^e\), viewed as integer modules. It factors through reduction to \(R_q^d\); the cokernel below is presented directly using its integer-domain image.
Define the finite obstruction module and its distinguished class by
The checked criterion is
The residual exists by the lower congruence and is unique because \(q>0\). The quotient is finite since its ambient module \(R_q^e\) is finite. The theorem permits zero variables or zero equations as well.
B.1.2 The checked Taylor bridge
On this page · Permalink · Source line 47
For every \(P\in\mathbb Z[X_1,\ldots,X_d]\), integer \(a\), and \(x,t\in\mathbb Z^d\), Lean proves
The proof uses polynomial induction: constants, addition, and multiplication by a variable. The product rule for the actual partial derivatives controls the multiplication step. It does not assume a Taylor identity or a liftability condition.
Taking \(a=q^L\), the inequality \(2L\ge L+1\) gives
Since \(q^L\ne0\) in the integers, cancellation in divisibility yields
Every integer representative of the lower residue has the form \(x+q^Lt\), and this correction equation has a solution exactly when \(o_x=0\).
The positive-depth hypothesis is necessary for the general nonlinear theorem. For \(F(X)=X^2-1\), \(q=2\), \(L=0\), \(x=0\), the Jacobian is zero and the residual class is nonzero, yet \(y=1\) is a solution modulo two in the same residue modulo one. Affine systems retain the previously checked \(L\ge0\) theorem.
B.1.3 Independence of the integer representative
On this page · Permalink · Source line 77
Suppose \(x'=x+q^Ls\) represents the same lower residue, with exact residual \(r_{x'}\). Polynomial evaluation respects coordinatewise congruences, including when applied to each partial derivative. Hence
The two cokernels therefore have the same ambient module and the same defining submodule, and
Lean states this using one explicit common reduced map, avoiding an implicit comparison between differently indexed quotient types. This establishes independence of the integer representative within the fixed polynomial presentation.
Changing the polynomial presentation is a separate question. Appending a zero equation can change the raw cokernel by adding a copy of \(R_q\), even though it does not change the solutions.
B.1.4 Two polynomial blocks and one shared lift
On this page · Permalink · Source line 99
Let \(G\in\mathbb Z[X_1,\ldots,X_d]^f\) be a second fixed system with the same variables and the same lower root \(x\). Let \(K_x=\rho_q\circ DG(x)\), and define
This quotient is finite: it is a quotient of the finite image of \(J_x\), or equivalently of the finite image of \(K_x\).
Suppose \(u,v\in\mathbb Z^d\) are separately valid corrections:
Then
The labels are independent of the choices of valid \(u\) and \(v\). An unconditional version asks for separately valid corrections with equal labels; it does not assume that each block is liftable.
Taylor transport turns a common correction \(t\) into the simultaneous equations \(J_xt=J_xu\) and \(K_xt=K_xv\). The previously checked common-quotient theorem gives precisely the displayed equivalence. Separate solvability alone does not imply joint solvability; the controls include \(F(X)=X\), \(G(X)=X-2\), starting at \(x=0\) modulo two and lifting to modulus four.