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{cont4:polynomial-roots-under-coefficient-perturbation}{%
2 \subsection{Polynomial roots under coefficient
3 perturbation}\label{cont4:polynomial-roots-under-coefficient-perturbation}}
4 
5 The argument proves uniqueness of roots for square systems and nearby-root stability
6 for finite systems of integer polynomials. The polynomials and their
7 partial derivatives are evaluated directly. No root-uniqueness or
8 perturbation-stability premise is assumed.
9 
10 \hypertarget{cont4:notation}{%
11 \subsubsection{Notation}\label{cont4:notation}}
12 
13 Let \(p\) be prime, \(L\ge1\), and \[
14 F,H\in\mathbb Z[X_1,\ldots,X_d]^e,
15 \qquad x\in\mathbb Z^d.
16 \] Write \[
17 A_x=DF(x)\bmod p:\mathbb F_p^d\longrightarrow\mathbb F_p^e,
18 \qquad B_L(x)=x+p^L\mathbb Z_p^d.
19 \] For an integer \(c\), the perturbed system is the actual polynomial
20 list \[
21 G=F+cH.
22 \] There is no restriction on the sign of \(c\), and \(c=0\) is allowed.
23 Divisibility conclusions give lower bounds on precision and allow zero
24 differences.
25 
26 \hypertarget{cont4:unique-roots-for-square-systems}{%
27 \subsubsection{1. Unique roots for square
28 systems}\label{cont4:unique-roots-for-square-systems}}
29 
30 If \(d=e\), \(A_x\) is surjective, and \(F(x)\equiv0\pmod{p^L}\), then
31 \[
32 \boxed{\exists!\,a\in B_L(x):F(a)=0.}
33 \] The stronger comparison lemma proves that any two exact roots of
34 \(F\) in \(B_L(x)\) coincide, without needing a separate lower-root
35 hypothesis.
36 
37 \textbf{Proof implemented.} Map every arbitrary p-adic root into the
38 actual residue rings \(\mathbb Z/p^n\mathbb Z\), and choose its
39 canonical integer representative. Evaluation commutes with reduction, so
40 these representatives are genuine finite polynomial roots. The preceding
41 count theorem gives exactly \(p^{d-d}=1\) next-level residue lift.
42 Inductively any two roots agree at every precision. The p-adic residue
43 maps separate points, so the roots are equal. Existence is the preceding
44 checked tower theorem.
45 
46 This extends uniqueness from the limit of a selected sequence to
47 \textbf{all exact roots in the prescribed ball}.
48 
49 \hypertarget{cont4:coefficient-perturbations-preserve-smooth-liftability}{%
50 \subsubsection{2. Coefficient perturbations preserve smooth
51 liftability}\label{cont4:coefficient-perturbations-preserve-smooth-liftability}}
52 
53 If \(p^L\mid c\), the actual identities give \[
54 G(x)=F(x)+cH(x),\qquad DG(x)\equiv DF(x)\pmod p.
55 \] Thus if \(F(x)\equiv0\pmod{p^L}\) and \(A_x\) is surjective, then \[
56 \exists b\in B_L(x):G(b)=0.
57 \] This theorem allows rectangular systems. The evaluation, derivative
58 and Jacobian identities are proved from the polynomial definition
59 \(G_i=F_i+C(c)H_i\), rather than supplied as hypotheses. Algebraic
60 congruence helpers also permit composite moduli. Exact p-adic root
61 existence uses prime \(p\).
62 
63 \hypertarget{cont4:nearby-roots-for-rectangular-systems}{%
64 \subsubsection{3. Nearby roots for rectangular
65 systems}\label{cont4:nearby-roots-for-rectangular-systems}}
66 
67 Let \(M\ge1\) and \(p^M\mid c\). Suppose \(A_x\) is surjective and
68 \(a\in\mathbb Z_p^d\) is an exact root of \(F\) with
69 \(a\equiv x\pmod p\). Then \[
70 \boxed{\exists b\in\mathbb Z_p^d:\quad G(b)=0,
71 \qquad b\equiv a\pmod{p^M}.}
72 \] No uniqueness is claimed when \(d>e\).
73 
74 \textbf{Proof implemented.} Truncate \(a\) to an integer vector \(y\)
75 modulo \(p^M\). It is an actual lower root of \(F\), and its reduced
76 Jacobian agrees with \(A_x\). Apply the coefficient-perturbed existence
77 theorem at precision \(M\), then combine the two congruences through
78 \(y\).
79 
80 \hypertarget{cont4:full-precision-for-the-unique-square-root}{%
81 \subsubsection{4. Full precision for the unique root of a square
82 system}\label{cont4:full-precision-for-the-unique-square-root}}
83 
84 Suppose \(d=e\), \(M\ge L\ge1\), \(p^M\mid c\), and \(A_x\) is
85 surjective. If \[
86 a,b\in B_L(x),\qquad F(a)=0,\qquad G(b)=0,
87 \] then \[
88 \boxed{b-a\in p^M\mathbb Z_p^d.}
89 \] In particular, for \(G=F+p^MH\), no p-adic digits below depth \(M\)
90 are changed in the selected root.
91 
92 The formalization also proves a combined existence theorem. Starting
93 only with \(F(x)\equiv0\pmod{p^L}\), it constructs an original root
94 \(a\in B_L(x)\) and proves that there is exactly one \(b\in B_L(x)\)
95 satisfying \(G(b)=0\) and \(b\equiv a\pmod{p^M}\). The comparison
96 theorem shows that the precision bound holds for every root of \(G\) in
97 that ball, so uniqueness is not obtained merely by adding a restrictive
98 displacement condition.
99 
100 \textbf{Proof implemented.} Section 3 produces a nearby root \(b'\).
101 Since \(M\ge L\), it belongs to \(B_L(x)\). The perturbed Jacobian
102 remains surjective, and square uniqueness identifies \(b'\) with the
103 arbitrary root \(b\).

Back to source controls

Back to Realization Calculus