B.2 Paper IX: correction torsors and exact polynomial lift counts
On this page · Permalink · Source line 2
Author: Komorebi P. — 8 September 2026.
This block formalizes the correction-digit torsor and prime-field counts from the previous checklist. The counts apply to distinct next-level residue classes satisfying the actual polynomial equations. They do not count integer representatives, of which there can be infinitely many.
B.2.1 The theorem
On this page · Permalink · Source line 13
Let \(p\) be prime, \(L\ge1\), and
Write
The actual lift set is
where polynomial evaluation in the displayed set is modulo \(p^{L+1}\). Define
Lean proves
These formulas permit singular Jacobians and zero variables or zero equations. Nonsingularity is not assumed. In particular, rank alone gives the size of a nonempty lift fiber; the residual obstruction determines whether it is empty.
B.2.2 Why these are actual residue-class counts
On this page · Permalink · Source line 47
For every positive integer \(q\), including composite moduli and modulus one, and every \(L\ge0\), the checked map
is a bijection. Here \(\widetilde t\) is the canonical integer representative of the digit vector. The entire residue fiber therefore has \(q^d\) elements. Injectivity is proved by cancelling \(q^L\) in the corresponding integer divisibility statement; surjectivity comes from the lower-residue congruence.
The formal type ActualLifts is a subtype of these genuine ZMod\ (q\^{}(L+1)) residue vectors. Its polynomial predicate is evaluated on canonical integer representatives and tested for divisibility by \(q^{L+1}\). The checked polynomial congruence theorem makes that predicate independent of the integer representative. Thus using canonical representatives does not discard or duplicate residue classes.
At positive depth, the preceding actual multivariable Taylor theorem gives
The new bridge proves that the evaluated integer Jacobian reduces to the actual \(\mathbb F_p\)-linear map \(A_x\). Restricting \(\Phi_{x,L}\) therefore gives an explicit equivalence
The proof uses the actual formal partial derivatives of the original polynomial list.
B.2.3 The torsor
On this page · Permalink · Source line 81
Let \(\mathcal T_x=\{t:b_x+A_xt=0\}\). Its natural kernel action is
For every pair \(u,t\in\mathcal T_x\), exactly one kernel vector sends \(u\) to \(t\), namely \(t-u\). Thus every nonempty correction fiber is a torsor for \(\ker A_x\). Choosing one valid digit \(u\) gives
Lean constructs an explicit AddTorsor structure for the digit fiber, proves the unique translation property, and supplies a chosen-point equivalence from the actual residue lift set to the kernel. A basepoint is required for this equivalence, but the translation action itself does not depend on choosing one.
The torsor and residue bijection remain valid over every positive modulus at positive polynomial depth. The displayed powers involving vector-space rank are restricted to prime moduli.
B.2.4 Connecting the old obstruction to the new count
On this page · Permalink · Source line 102
The earlier obstruction used the integer-domain map
The new count uses \(A_x:\mathbb F_p^d\to\mathbb F_p^e\). Reduction of integer vectors onto finite vectors is surjective, so the two maps have the same image after restricting scalars. Lean constructs a class-preserving integer-linear equivalence
Consequently the cardinality theorem counts the original obstruction group, preserving its distinguished residual class. It is not merely a formula for a separately introduced comparison object.
Rank-nullity gives \(\dim\ker A_x=d-\rho_x\), and the quotient dimension is \(e-\rho_x\). Cardinalities of finite vector spaces complete both formulas.