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{cont7:paper-ix-weighted-first-order-root-motion}{%
2 \subsection{Chapter IX: weighted first-order root
3 motion}\label{cont7:paper-ix-weighted-first-order-root-motion}}
4 
5 \hypertarget{cont7:the-theorem}{%
6 \subsubsection{The theorem}\label{cont7:the-theorem}}
7 
8 Let \(p\) be prime, \(R=\mathbb Z_p\), \(K=\mathbb Q_p\), and
9 \(d,s,M\in\mathbb N\). Let \(F,H\in R[X_1,\ldots,X_d]^d\), let
10 \(a\in R^d\) satisfy \(F(a)=0\), and set \[
11 J=DF(a),\qquad G=F+p^M H.
12 \] Assume \[
13 J\in\operatorname{GL}_d(K),\qquad p^sJ^{-1}\in M_d(R),\qquad M>2s.
14 \] Then there is exactly one root \(b\) of \(G\) in \(a+p^{s+1}R^d\). It
15 satisfies \[
16 b-a\in p^{M-s}R^d,
17 \] and there is \(\varepsilon\in p^{2M-3s}R^d\) such that, in \(K^d\),
18 \[
19 \boxed{b-a=-p^M J^{-1}H(a)+\varepsilon.}
20 \] The inverse in this formula belongs to the original Jacobian
21 \(DF(a)\). The theorem constructs the perturbed root from these
22 hypotheses and proves uniqueness throughout the full ball of depth
23 \(s+1\). It does not require an additional Jacobian hypothesis on \(G\).
24 Coefficients and centers are arbitrary integral p-adic elements. Every
25 prime and finite square dimension are included, including \(p=2\) and
26 dimension zero.
27 
28 The error depth exceeds the displacement depth by \[
29 (2M-3s)-(M-s)=M-2s\ge1.
30 \] Thus the first-order term determines strictly more digits than the
31 displacement bound alone. These are guaranteed divisibility bounds.
32 Equality of valuations is not asserted for every system.
33 
34 \hypertarget{cont7:root-construction-with-the-original-inverse}{%
35 \subsubsection{Root construction with the original
36 inverse}\label{cont7:root-construction-with-the-original-inverse}}
37 
38 Write \(A=p^sJ^{-1}\in M_d(R)\), so \(AJ=JA=p^sI\). Let \(t=p^{s+1}\)
39 and \(k=M-(2s+1)\ge0\). The actual polynomial Taylor and difference
40 identities give polynomial systems \(Q_F,Q_H\), both vanishing at zero,
41 such that \[
42 (AF)(a+tu)=p^{2s+1}u+p^{2s+2}Q_F(u),
43 \] \[
44 (AH)(a+tu)=(AH)(a)+tQ_H(u).
45 \] Consequently \[
46 (AG)(a+tu)=p^{2s+1}\bigl(C+u+pQ(u)\bigr),
47 \] where \[
48 C=p^kAH(a),\qquad
49 Q=Q_F+p^{M-s-1}Q_H,\qquad Q(0)=0.
50 \] All exponents are nonnegative under \(M>2s\). Actual integral
51 polynomial evaluation is 1-Lipschitz, so \(u\mapsto-C-pQ(u)\) is a
52 strict contraction on the complete space \(R^d\). Its unique fixed point
53 inherits the depth \(k\) of \(C\), because \(Q(0)=0\). Thus \(b=a+tu\)
54 has displacement depth \(s+1+k=M-s\).
55 
56 The certificate \(JA=p^sI\) makes multiplication by \(A\) injective, so
57 the normalized zero is an actual root of \(G\). Every root in \(a+tR^d\)
58 has the form \(a+tw\) and satisfies the same fixed-point equation. This
59 proves uniqueness on the entire stated ball using the original matrix
60 certificate.
61 
62 \hypertarget{cont7:the-first-order-error}{%
63 \subsubsection{The first-order error}\label{cont7:the-first-order-error}}
64 
65 Put \(\delta=b-a\) and \(L=M-s\). The displacement form of Taylor's
66 theorem, proved over any commutative ring, gives \[
67 E_F=(AF)(b)-(AF)(a)-p^s\delta\in p^{2L}R^d.
68 \] Polynomial congruence gives \[
69 E_H=(AH)(b)-(AH)(a)\in p^LR^d.
70 \] Since \(F(a)=0\) and \(G(b)=0\), \[
71 p^s\delta+p^MAH(a)=-E_F-p^ME_H.
72 \] We have \(M+L\ge2L\), so the right side lies in \(p^{2L}R^d\).
73 Cancelling the nonzero scalar \(p^s\) proves the integral estimate \[
74 \delta+p^{M-s}AH(a)\in p^{2M-3s}R^d.
75 \] Define this integral vector to be \(\varepsilon\). Under
76 \(R\hookrightarrow K\), the exact identity \(p^{M-s}A=p^MJ^{-1}\) gives
77 the displayed first-order formula. The Lean bridge checks matrix
78 evaluation and all coefficient inclusions explicitly.
79 
80 \hypertarget{cont7:sharpness-and-the-strict-threshold}{%
81 \subsubsection{Sharpness and the strict
82 threshold}\label{cont7:sharpness-and-the-strict-threshold}}
83 
84 For \(p=2\), take \(F(X)=X+X^2\), \(H(X)=1\), \(a=0\), \(s=0\), \(M=1\).
85 There is a unique root \(b\in2\mathbb Z_2\) of \(X+X^2+2\). Its equation
86 gives \(b+2=-b^2\). It also forces \(b\equiv2\pmod4\). Therefore \[
87 v_2(b+2)=2=2M-3s.
88 \] The accompanying Lean controls show that the error is divisible by
89 four and is not divisible by eight. This refutes a uniform replacement
90 of \(2M-3s\) by \(2M-3s+1\), even for a one-variable unit Jacobian.
91 
92 The prior strict-threshold example also applies to perturbations: take
93 \(F(X)=X^2-1\), \(H(X)=1\), \(a=1\), \(p=2\), \(s=1\), \(M=2\). Then
94 \(F(a)=0\), \(DF(a)=2\), and \(F+2^2H=X^2+3\) has no root modulo eight,
95 hence none in \(\mathbb Z_2\). The new explanatory identification uses
96 the previously checked no-root polynomial. The strict inequality
97 \(M>2s\) cannot uniformly be replaced by \(M\ge2s\).

Back to source controls

Back to Realization Calculus