B.6 Paper IX: weighted nonlinear lifting
On this page · Permalink · Source line 2
Komorebi P. — 8 September 2026.
B.6.1 The theorem
On this page · Permalink · Source line 8
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
Assume
Then
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
On this page · Permalink · Source line 32
Write \(A=p^sJ^{-1}\in M_d(R)\). Then
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
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
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
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
On this page · Permalink · Source line 71
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.