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{cont6:paper-ix-weighted-nonlinear-lifting}{%
2 \subsection{Chapter IX: weighted nonlinear
3 lifting}\label{cont6:paper-ix-weighted-nonlinear-lifting}}
4 
5 \hypertarget{cont6:the-theorem}{%
6 \subsubsection{The theorem}\label{cont6:the-theorem}}
7 
8 Let \(p\) be prime, \(R=\mathbb Z_p\), \(K=\mathbb Q_p\), and
9 \(d,s,r\in\mathbb N\). Let
10 \(F=(F_1,\ldots,F_d)\in R[X_1,\ldots,X_d]^d\), \(a\in R^d\), and let \[
11 J=DF(a)=\bigl(\partial_jF_i(a)\bigr)_{i,j}.
12 \] Assume \[
13 J\in\operatorname{GL}_d(K),\qquad p^sJ^{-1}\in M_d(R),\qquad
14 F(a)\in p^rR^d,\qquad r>2s.
15 \] Then \[
16 \boxed{\exists!\,b\in a+p^{s+1}R^d:\ F(b)=0,}
17 \qquad
18 \boxed{b-a\in p^{r-s}R^d.}
19 \] All vector divisibility assertions are coordinatewise. The uniqueness
20 predicate is the entire ball of depth \(s+1\): competitors need not be
21 assumed to have depth \(r-s\). The theorem permits arbitrary integral
22 p-adic coefficients and centers, every prime including two, and
23 dimension zero. It retains the supplied inverse-denominator exponent
24 \(s\). There is no replacement by a determinant valuation. Integrality
25 of \(p^sJ^{-1}\) is expressed in Lean by existence of an integral matrix
26 with exactly that image under the coefficient inclusion
27 \(R\hookrightarrow K\).
28 
29 \hypertarget{cont6:proof}{%
30 \subsubsection{Proof}\label{cont6:proof}}
31 
32 Write \(A=p^sJ^{-1}\in M_d(R)\). Then \[
33 AJ=JA=p^sI.
34 \] The formal matrix bridge proves the equivalence with the stated
35 fraction-field hypotheses, including nonsingularity. In particular,
36 multiplication by \(A\) is injective, since multiplication by \(J\)
37 sends \(Av=0\) to \(p^sv=0\).
38 
39 Put \(G=AF\), \(t=p^{s+1}\), and \(k=r-(2s+1)\). Taylor expansion of the
40 actual preconditioned polynomials gives one polynomial system \(Q\) such
41 that \[
42 G(a+tu)=G(a)+p^{2s+1}u+p^{2s+2}Q(u),\qquad Q(0)=0.
43 \] This expansion is proved first over every commutative ring. Its
44 remainder is a polynomial valid for every \(u\), not a pointwise
45 quotient depending on \(u\). Since \(G(a)\in p^rR^d\), it can be written
46 \(p^{2s+1}C\) with \(C\in p^kR^d\). Thus \[
47 G(a+tu)=p^{2s+1}\bigl(C+u+pQ(u)\bigr).
48 \]
49 
50 Integral polynomial evaluation is 1-Lipschitz in the supremum p-adic
51 metric. Consequently \(T(u)=-C-pQ(u)\) has contraction constant
52 \(|p|_p<1\) on the complete space \(R^d\), and has exactly one fixed
53 point \(u\).
54 
55 For completeness, the sharp precision is additional to this fixed-point
56 existence. Inductively, if \(u\in p^nR^d\), then polynomial congruence
57 and \(Q(0)=0\) imply \(Q(u)\in p^nR^d\). For \(n<k\), the equation
58 \(u=-C-pQ(u)\) therefore gives \(u\in p^{n+1}R^d\). Starting at \(n=0\),
59 this proves \(u\in p^kR^d\). Hence \(b=a+tu\) satisfies \[
60 b-a\in p^{s+1+k}R^d=p^{r-s}R^d.
61 \] The normalization and injectivity of \(A\) give \(F(b)=0\).
62 
63 Every other \(z\in a+p^{s+1}R^d\) has the form \(a+tw\). If \(F(z)=0\),
64 the same normalization, with cancellation of the nonzero scalar
65 \(p^{2s+1}\), gives \(w=T(w)\). Fixed-point uniqueness implies \(w=u\),
66 hence \(z=b\).
67 
68 \hypertarget{cont6:boundary-and-sharpness}{%
69 \subsubsection{Boundary and sharpness}\label{cont6:boundary-and-sharpness}}
70 
71 The strict inequality cannot in general be weakened to \(r\ge2s\): for
72 \(p=2\), \(F(X)=X^2+3\), and \(a=1\), we have \(F(a)=4\), \(DF(a)=2\),
73 and may take \(s=1,r=2\). Yet no root exists in \(\mathbb Z_2\), since
74 there is none modulo eight. The auxiliary Lean controls prove this
75 obstruction and the exact residual depth.
76 
77 The displacement exponent cannot uniformly be increased by one. For
78 \(F(X)=p^sX+p^r\) at \(a=0\), with \(r>2s\), its root is \(b=-p^{r-s}\),
79 which is not divisible by \(p^{r-s+1}\). The controls prove the linear
80 root and the absence of that extra digit for all primes.

Back to source controls

Back to Realization Calculus