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

Back to source controls

Back to Realization Calculus