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{cont2:paper-ix-correction-torsors-and-exact-polynomial-lift-counts}{%
2 \subsection{Paper IX: correction torsors and exact polynomial lift
3 counts}\label{cont2:paper-ix-correction-torsors-and-exact-polynomial-lift-counts}}
4 
5 \textbf{Author: Komorebi P. --- 8 September 2026.}
6 
7 This block formalizes the correction-digit torsor and prime-field counts
8 from the previous checklist. The counts apply to distinct next-level
9 residue classes satisfying the actual polynomial equations. They do not
10 count integer representatives, of which there can be infinitely many.
11 
12 \hypertarget{cont2:the-theorem}{%
13 \subsubsection{The theorem}\label{cont2:the-theorem}}
14 
15 Let \(p\) be prime, \(L\ge1\), and \[
16 F\in\mathbb Z[X_1,\ldots,X_d]^e,
17 \qquad x\in\mathbb Z^d,
18 \qquad F(x)\equiv0\pmod{p^L}.
19 \] Write \[
20 r_x=F(x)/p^L,\qquad b_x=r_x\bmod p,
21 \qquad A_x=DF(x)\bmod p:\mathbb F_p^d\longrightarrow\mathbb F_p^e,
22 \qquad \rho_x=\operatorname{rank}_{\mathbb F_p}A_x.
23 \] The actual lift set is \[
24 \mathcal L_{x,L}=
25 \left\{y\in(\mathbb Z/p^{L+1}\mathbb Z)^d:
26  y\equiv x\pmod{p^L},\quad F(y)=0\right\},
27 \] where polynomial evaluation in the displayed set is modulo
28 \(p^{L+1}\). Define \[
29 \mathcal O_x=\mathbb F_p^e/\operatorname{im}A_x,
30 \qquad o_x=[b_x].
31 \] Lean proves \[
32 \boxed{
33 \#\mathcal L_{x,L}=
34 \begin{cases}
35 p^{d-\rho_x},&o_x=0,\\
36 0,&o_x\ne0,
37 \end{cases}
38 \qquad
39 \#\mathcal O_x=p^{e-\rho_x}.
40 }
41 \] These formulas permit singular Jacobians and zero variables or zero
42 equations. Nonsingularity is not assumed. In particular, rank alone
43 gives the size of a nonempty lift fiber; the residual obstruction
44 determines whether it is empty.
45 
46 \hypertarget{cont2:why-these-are-actual-residue-class-counts}{%
47 \subsubsection{Why these are actual residue-class
48 counts}\label{cont2:why-these-are-actual-residue-class-counts}}
49 
50 For every positive integer \(q\), including composite moduli and modulus
51 one, and every \(L\ge0\), the checked map \[
52 \Phi_{x,L}:(\mathbb Z/q\mathbb Z)^d\longrightarrow
53 \{y\bmod q^{L+1}:y\equiv x\pmod{q^L}\},
54 \qquad t\longmapsto x+q^L\widetilde t
55 \] is a bijection. Here \(\widetilde t\) is the canonical integer
56 representative of the digit vector. The entire residue fiber therefore
57 has \(q^d\) elements. Injectivity is proved by cancelling \(q^L\) in the
58 corresponding integer divisibility statement; surjectivity comes from
59 the lower-residue congruence.
60 
61 The formal type \mcode{ActualLifts} is a subtype of these genuine
62 \texttt{ZMod\ (q\^{}(L+1))} residue vectors. Its polynomial predicate is
63 evaluated on canonical integer representatives and tested for
64 divisibility by \(q^{L+1}\). The checked polynomial congruence theorem
65 makes that predicate independent of the integer representative. Thus
66 using canonical representatives does not discard or duplicate residue
67 classes.
68 
69 At positive depth, the preceding actual multivariable Taylor theorem
70 gives \[
71 F(x+p^L\widetilde t)\equiv
72 p^L(r_x+DF(x)\widetilde t)\pmod{p^{L+1}}.
73 \] The new bridge proves that the evaluated integer Jacobian reduces to
74 the actual \(\mathbb F_p\)-linear map \(A_x\). Restricting
75 \(\Phi_{x,L}\) therefore gives an explicit equivalence \[
76 \boxed{\{t\in\mathbb F_p^d:b_x+A_xt=0\}\simeq\mathcal L_{x,L}.}
77 \] The proof uses the actual formal partial derivatives of the original
78 polynomial list.
79 
80 \hypertarget{cont2:the-torsor}{%
81 \subsubsection{The torsor}\label{cont2:the-torsor}}
82 
83 Let \(\mathcal T_x=\{t:b_x+A_xt=0\}\). Its natural kernel action is \[
84 k\cdot t=k+t,\qquad k\in\ker A_x.
85 \] For every pair \(u,t\in\mathcal T_x\), exactly one kernel vector
86 sends \(u\) to \(t\), namely \(t-u\). Thus every nonempty correction
87 fiber is a torsor for \(\ker A_x\). Choosing one valid digit \(u\) gives
88 \[
89 \mathcal T_x\simeq\ker A_x,
90 \qquad t\longmapsto t-u.
91 \] Lean constructs an explicit \mcode{AddTorsor} structure for the
92 digit fiber, proves the unique translation property, and supplies a
93 chosen-point equivalence from the actual residue lift set to the kernel.
94 A basepoint is required for this equivalence, but the translation action
95 itself does not depend on choosing one.
96 
97 The torsor and residue bijection remain valid over every positive
98 modulus at positive polynomial depth. The displayed powers involving
99 vector-space rank are restricted to prime moduli.
100 
101 \hypertarget{cont2:connecting-the-old-obstruction-to-the-new-count}{%
102 \subsubsection{Connecting the old obstruction to the new
103 count}\label{cont2:connecting-the-old-obstruction-to-the-new-count}}
104 
105 The earlier obstruction used the integer-domain map \[
106 J_x=\rho_p\circ DF(x):\mathbb Z^d\to\mathbb F_p^e.
107 \] The new count uses \(A_x:\mathbb F_p^d\to\mathbb F_p^e\). Reduction
108 of integer vectors onto finite vectors is surjective, so the two maps
109 have the same image after restricting scalars. Lean constructs a
110 class-preserving integer-linear equivalence \[
111 \mathbb F_p^e/\operatorname{im}J_x
112 \simeq
113 \mathbb F_p^e/\operatorname{im}A_x.
114 \] Consequently the cardinality theorem counts the original obstruction
115 group, preserving its distinguished residual class. It is not merely a
116 formula for a separately introduced comparison object.
117 
118 Rank-nullity gives \(\dim\ker A_x=d-\rho_x\), and the quotient dimension
119 is \(e-\rho_x\). Cardinalities of finite vector spaces complete both
120 formulas.

Back to source controls

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