Paper IXReading edition

B.6. Paper IX: weighted nonlinear lifting

Reading tools
Reading libraryFind statementsInspect Lean
Switch work

Saved reading

Read side by side

Start reading

Resources & source

Original TeX with line links · Download TeX

The wording and mathematics follow the retained manuscript. This reading format does not add a proof review or extend Lean coverage.

Skip contents and start reading

B.6 Paper IX: weighted nonlinear lifting

Komorebi P. — 8 September 2026.

B.6.1 The theorem

Let \(p\) be prime, \(R=\mathbb Z_p\), \(K=\mathbb Q_p\), and \(d,s,r\in\mathbb N\). Let \(F=(F_1,\ldots,F_d)\in R[X_1,\ldots,X_d]^d\), \(a\in R^d\), and let

\[ J=DF(a)=\bigl(\partial_jF_i(a)\bigr)_{i,j}. \]

Assume

\[ J\in\operatorname{GL}_d(K),\qquad p^sJ^{-1}\in M_d(R),\qquad F(a)\in p^rR^d,\qquad r>2s. \]

Then

\[ \boxed{\exists!\,b\in a+p^{s+1}R^d:\ F(b)=0,} \qquad \boxed{b-a\in p^{r-s}R^d.} \]

All vector divisibility assertions are coordinatewise. The uniqueness predicate is the entire ball of depth \(s+1\): competitors need not be assumed to have depth \(r-s\). The theorem permits arbitrary integral p-adic coefficients and centers, every prime including two, and dimension zero. It retains the supplied inverse-denominator exponent \(s\); there is no replacement by a determinant valuation. Integrality of \(p^sJ^{-1}\) is expressed in Lean by existence of an integral matrix with exactly that image under the coefficient inclusion \(R\hookrightarrow K\).

B.6.2 Proof

Write \(A=p^sJ^{-1}\in M_d(R)\). Then

\[ AJ=JA=p^sI. \]

The formal matrix bridge proves the equivalence with the stated fraction-field hypotheses, including nonsingularity. In particular, multiplication by \(A\) is injective, since multiplication by \(J\) sends \(Av=0\) to \(p^sv=0\).

Put \(G=AF\), \(t=p^{s+1}\), and \(k=r-(2s+1)\). Taylor expansion of the actual preconditioned polynomials gives one polynomial system \(Q\) such that

\[ G(a+tu)=G(a)+p^{2s+1}u+p^{2s+2}Q(u),\qquad Q(0)=0. \]

This expansion is proved first over every commutative ring. Its remainder is a polynomial valid for every \(u\), not a pointwise quotient depending on \(u\). Since \(G(a)\in p^rR^d\), it can be written \(p^{2s+1}C\) with \(C\in p^kR^d\). Thus

\[ G(a+tu)=p^{2s+1}\bigl(C+u+pQ(u)\bigr). \]

Integral polynomial evaluation is 1-Lipschitz in the supremum p-adic metric. Consequently \(T(u)=-C-pQ(u)\) has contraction constant \(|p|_p<1\) on the complete space \(R^d\), and has exactly one fixed point \(u\).

For completeness, the sharp precision is additional to this fixed-point existence. Inductively, if \(u\in p^nR^d\), then polynomial congruence and \(Q(0)=0\) imply \(Q(u)\in p^nR^d\). For \(n<k\), the equation \(u=-C-pQ(u)\) therefore gives \(u\in p^{n+1}R^d\). Starting at \(n=0\), this proves \(u\in p^kR^d\). Hence \(b=a+tu\) satisfies

\[ b-a\in p^{s+1+k}R^d=p^{r-s}R^d. \]

The normalization and injectivity of \(A\) give \(F(b)=0\).

Every other \(z\in a+p^{s+1}R^d\) has the form \(a+tw\). If \(F(z)=0\), the same normalization, with cancellation of the nonzero scalar \(p^{2s+1}\), gives \(w=T(w)\). Fixed-point uniqueness implies \(w=u\), hence \(z=b\).

B.6.3 Boundary and sharpness

The strict inequality cannot in general be weakened to \(r\ge2s\): for \(p=2\), \(F(X)=X^2+3\), and \(a=1\), we have \(F(a)=4\), \(DF(a)=2\), and may take \(s=1,r=2\). Yet no root exists in \(\mathbb Z_2\), since there is none modulo eight. The auxiliary Lean controls prove this obstruction and the exact residual depth.

The displacement exponent cannot uniformly be increased by one. For \(F(X)=p^sX+p^r\) at \(a=0\), with \(r>2s\), its root is \(b=-p^{r-s}\), which is not divisible by \(p^{r-s+1}\). The controls prove the linear root and the absence of that extra digit for all primes.

Source and conversion record

Source SHA-256: 72b22d173ad349c8c619b5942cd0286b95096d162d483b0b69c6bb1f69a86baa

Unsupported prose commands stop the build. The mathematical expression sequence is checked against the source, with manuscript macros expanded for display.

Conversion records

Notation in Paper IX

Look up a symbol without leaving this chapter. Select text before opening help to search for it.

Search this work’s notation.

    Symbols can have different meanings in different passages. Read each result in its own context.

    Open the full notation index