30_lifting.tex

Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation

30_lifting.tex

17 indexed statements in this file

These links follow the claim index. They do not extend the recorded proof or Lean coverage.

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

Skip source text

1 \section{Finite obstructions, compatible lifts, and deformation}
2 \label{sec:lifting}
3 
4 The arithmetic results above concern particular families. We now study the
5 underlying correction problem, from finite polynomial lifts to continuous
6 parameter charts and quantitative deformation. Throughout, we distinguish
7 three objects: a residual obstruction, the set of correcting digits, and a
8 root in a completion. A vanishing obstruction at one precision gives a lift
9 to the next. Continuing indefinitely requires additional hypotheses.
10 
11 Unless a different coefficient ring is specified, a polynomial system is a
12 finite list of integer polynomials. All divisibility conditions on vectors are
13 coordinatewise. For a positive integer $q$, write $S_q=\Z/q\Z$ and use an
14 overline for reduction modulo $q$. For a prime $p$, write
15 $\F_p=S_p$, normalize $|p|_p=p^{-1}$, and put
16 \[
17  B_L(x)=x+p^L\Zp^d.
18 \]
19 An integer center is included in this notation by its natural image in
20 $\Zp^d$. All dimensions below are finite and may be zero. A statement over
21 $S_q$ allows composite $q$ and $q=1$ when explicitly stated. A cardinality
22 formula in terms of vector-space rank uses prime $p$.
23 
24 \subsection{The polynomial correction equation}
25 
26 For $F=(F_1,\ldots,F_e)\in\Z[X_1,\ldots,X_d]^e$, define its evaluated
27 Jacobian by the formal partial derivatives:
28 \[
29  DF(x)_{ij}=(\partial_jF_i)(x),\qquad
30  J_x=DF(x)\bmod q:S_q^d\longrightarrow S_q^e.
31 \]
32 The obstruction therefore uses the Jacobian of the given polynomials. The
33 following algebraic Taylor identity relates this linear map to polynomial
34 evaluation.
35 
Statement: Polynomial Taylor remainder · Go to proof · Read statement and proof side by side36 \begin{lemma}[Polynomial Taylor remainder]\label{lem:polynomial-taylor}
37 Let $R$ be a commutative ring, $P\in R[X_1,\ldots,X_d]$, $a\in R^d$, and
38 $c\in R$. There is a polynomial $Q\in R[U_1,\ldots,U_d]$, with $Q(0)=0$,
39 such that for every $u\in R^d$,
40 \begin{equation}\label{eq:polynomial-taylor}
41  P(a+cu)=P(a)+c\sum_{j=1}^d(\partial_jP)(a)u_j+c^2Q(u).
42 \end{equation}
43 In particular, when $R=\Z$ and $a,u,c$ are integral, subtracting the first
44 two terms on the right from $P(a+cu)$ gives a multiple of $c^2$.
45 \end{lemma}
46 
Proof block: Polynomial Taylor remainder · Go to statement · Read statement and proof side by side47 \begin{proof}
48 Apply polynomial induction using constants, addition, and multiplication by a
49 variable. Constants have zero remainder, and remainders add. For the
50 multiplication step, suppose the assertion is known for $P$ and write
51 $D_P(U)=\sum_j(\partial_jP)(a)U_j$. Multiplication of its expansion by
52 $a_i+cU_i$ gives constant term $P(a)a_i$, linear term
53 $c(a_iD_P(U)+P(a)U_i)$, and remainder
54 \[
55  c^2\bigl(Q(U)(a_i+cU_i)+D_P(U)U_i\bigr).
56 \]
57 The product rule identifies the linear term with the derivative of
58 $PX_i$. The displayed remainder vanishes at $U=0$. This constructs the
59 polynomial remainder before evaluation at $u$, even over rings where
60 division by $c$ would be invalid.
61 \end{proof}
62 
63 The general polynomial identity is formalized by
64 \lean{Komorebi.PolynomialTaylorRing.exists_eval_scaled_remainder}.
65 Its integer divisibility form is
66 \lean{Komorebi.PolynomialTaylor.taylor_dvd}.
67 
Statement: Finite polynomial obstruction · Go to proof · Read statement and proof side by side68 \begin{theorem}[Finite polynomial obstruction]\label{thm:finite-polynomial-obstruction}
69 Let $q\ge1$, $L\ge1$, $x\in\Z^d$, and suppose
70 $F(x)\in q^L\Z^e$. Define the exact integer residual $r_x$ by
71 $F(x)=q^Lr_x$, and put
72 \[
73  \mathcal O_x=S_q^e/\im J_x,\qquad o_x=[\overline{r_x}].
74 \]
75 Then $\mathcal O_x$ is finite and
76 \begin{equation}\label{eq:finite-obstruction}
77  o_x=0\quad\Longleftrightarrow\quad
78  \exists y\in\Z^d:\quad
79  y\equiv x\pmod{q^L},\qquad F(y)\equiv0\pmod{q^{L+1}}.
80 \end{equation}
81 No surjectivity or nonsingularity assumption is required.
82 \end{theorem}
83 
Proof block: Finite polynomial obstruction · Go to statement · Read statement and proof side by side84 \begin{proof}
85 Every point in the lower residue class has the form $y=x+q^Lt$ with
86 $t\in\Z^d$. By Lemma~\ref{lem:polynomial-taylor} and $2L\ge L+1$,
87 \[
88  F(x+q^Lt)\equiv q^L\bigl(r_x+DF(x)t\bigr)\pmod{q^{L+1}}.
89 \]
90 The integer $q^L$ is nonzero. Cancelling it in the corresponding divisibility
91 condition proves
92 \begin{equation}\label{eq:digit-correction}
93  F(x+q^Lt)\equiv0\pmod{q^{L+1}}
94  \quad\Longleftrightarrow\quad
95  \overline{r_x}+J_x\overline t=0.
96 \end{equation}
97 Integer vectors reduce onto $S_q^d$. The equation on the right is solvable
98 exactly when $\overline{r_x}$ belongs to $\im J_x$, since that image is
99 closed under negation. This is precisely $o_x=0$. Finiteness follows because
100 $\mathcal O_x$ is a quotient of the finite module $S_q^e$.
101 \end{proof}
102 
103 The formal theorem
104 \lean{Komorebi.PolynomialObstruction.finite_polynomial_obstruction}
105 presents the image using the integer-domain map
106 $\Z^d\xrightarrow{DF(x)}\Z^e\to S_q^e$. Reduction onto $S_q^d$ identifies
107 that image with $\im J_x$. The class-preserving comparison is explicit in
108 \lean{Komorebi.PolynomialLiftCounts.obstructionEquiv}; the change of
109 presentation does not change the distinguished residual class.
110 
Statement: Affine depth zero · Go to proof · Read statement and proof side by side111 \begin{proposition}[Affine depth zero]\label{prop:affine-obstruction}
112 Let $F(x)=Ax-b$ for an integer linear map $A:\Z^d\to\Z^e$. The criterion
113 of Theorem~\ref{thm:finite-polynomial-obstruction} holds for every $L\ge0$,
114 with $J=A\bmod q$.
115 \end{proposition}
116 
Proof block: Affine depth zero · Go to statement · Read statement and proof side by side117 \begin{proof}
118 The affine identity
119 $F(x+q^Lt)=F(x)+q^LAt$ has no quadratic remainder. The proof of
120 \eqref{eq:digit-correction} therefore needs no inequality involving $2L$.
121 The residual and the finite quotient are obtained as above.
122 \end{proof}
123 
124 The affine statement is formalized by
125 \lean{Komorebi.NativeAffine.finite_affine_obstruction}.
126 Positive depth is essential in the nonlinear theorem: for $F(X)=X^2-1$,
127 $q=2$, $L=0$, and $x=0$, the Jacobian is zero and the residual class is
128 nonzero, yet $y=1$ is a root modulo two in the same residue modulo one.
129 
Statement: Independence of the integer representative · Go to proof · Read statement and proof side by side130 \begin{proposition}[Independence of the integer representative]
131 \label{prop:representative-independence}
132 Under the hypotheses of Theorem~\ref{thm:finite-polynomial-obstruction},
133 let $x'=x+q^Ls$ and write $F(x')=q^Lr_{x'}$. Then
134 \[
135  J_{x'}=J_x,\qquad
136  \overline{r_{x'}}=\overline{r_x}+J_x\overline s.
137 \]
138 Consequently the two residual classes coincide in the common quotient
139 $S_q^e/\im J_x$.
140 \end{proposition}
141 
Proof block: Independence of the integer representative · Go to statement · Read statement and proof side by side142 \begin{proof}
143 Polynomial evaluation respects coordinatewise congruence. Apply this first
144 to every formal partial derivative: $x'\equiv x\pmod q$ gives
145 $J_{x'}=J_x$. Next apply \eqref{eq:polynomial-taylor} to $F$ at scale $q^L$.
146 Subtract the two exact residual identities and cancel $q^L$ to obtain the
147 displayed relation modulo $q$. Its additional term belongs to the common
148 Jacobian image, so it vanishes in the quotient.
149 \end{proof}
150 
151 This comparison is formalized by
152 \lean{Komorebi.PolynomialRepresentative.representative_independence}.
153 This proves independence of the integer representative within a fixed
154 polynomial presentation. It makes no identification of the raw cokernels
155 of different equation lists. For example, adjoining a zero equation leaves
156 the roots unchanged while adding an $S_q$ summand to the raw cokernel.
157 
158 \subsection{One correction shared by two systems}
159 
160 The next obstruction concerns compatibility between individually attainable
161 corrections. Its algebraic form works over an arbitrary commutative ring.
162 Let $U,V,W$ be $R$-modules and let $J:U\to V$, $K:U\to W$ be linear.
163 Define
164 \begin{equation}\label{eq:common-quotient}
165  C(J,K)=U/(\ker J+\ker K).
166 \end{equation}
167 An attainable value $Ju$ has label $[u]\in C(J,K)$; this is independent of
168 the choice of its preimage because $\ker J$ is killed in the quotient.
169 Similarly, $Kv$ has label $[v]$. Denote these maps by
170 $\lambda_J:\im J\to C(J,K)$ and $\lambda_K:\im K\to C(J,K)$.
171 
Statement: Common correction and fiber product · Go to proof · Read statement and proof side by side172 \begin{theorem}[Common correction and fiber product]\label{thm:common-correction}
173 For every $u,v\in U$,
174 \begin{equation}\label{eq:common-correction}
175  [u]=[v]\text{ in }C(J,K)
176  \quad\Longleftrightarrow\quad
177  \exists w\in U:\ Jw=Ju,\quad Kw=Kv.
178 \end{equation}
179 Both label maps are surjective, and the image of the joint map is exactly
180 the fiber product:
181 \begin{equation}\label{eq:joint-fiber-product}
182  \im\bigl(U\to\im J\times\im K,\ u\mapsto(Ju,Ku)\bigr)
183  =\im J\mathbin{\times}_{C(J,K)}\im K.
184 \end{equation}
185 If either $V$ or $W$ is finite, then $C(J,K)$ is finite.
186 \end{theorem}
187 
Proof block: Common correction and fiber product · Go to statement · Read statement and proof side by side188 \begin{proof}
189 If $[u]=[v]$, write $u-v=s+t$ with $s\in\ker J$ and $t\in\ker K$.
190 Then $w=u-s=v+t$ satisfies both required equalities. Conversely, a common
191 $w$ gives
192 \[
193  u-v=(u-w)+(w-v)\in\ker J+\ker K.
194 \]
195 Every class $[u]$ is the label of $Ju$ and of $Ku$, proving surjectivity.
196 For attainable $a=Ju$ and $b=Kv$, the first equivalence says exactly that
197 equal labels are equivalent to a simultaneous preimage. This proves
198 \eqref{eq:joint-fiber-product}. Finally, a finite target has finite image,
199 and the associated surjective label map makes $C(J,K)$ finite.
200 \end{proof}
201 
202 These statements are
203 \lean{Komorebi.SharedCorrection.quotient_mk_eq_iff_common} and
204 \lean{Komorebi.SharedCorrection.joint_range_eq_fiber}, together with the
205 finite-target corollaries in the same module. The quotient also has the
206 expected universal property: every linear map from $U$ annihilating both
207 kernels factors uniquely through $C(J,K)$. Equivalently, compatible linear
208 observations on $\im J$ and $\im K$ factor uniquely through their label
209 maps. This is formalized by
210 \lean{Komorebi.SharedCorrection.common_paired_universal}.
211 
Statement: Simultaneous polynomial lifting · Go to proof · Read statement and proof side by side212 \begin{corollary}[Simultaneous polynomial lifting]\label{cor:shared-polynomial}
213 Let $F\in\Z[X_1,\ldots,X_d]^e$ and
214 $G\in\Z[X_1,\ldots,X_d]^f$ have a common lower root $x$ modulo $q^L$,
215 where $q\ge1$ and $L\ge1$. Use the integer-domain reduced Jacobians
216 $J:\Z^d\to S_q^e$ and $K:\Z^d\to S_q^f$. Suppose $u,v\in\Z^d$ are
217 separately valid corrections for $F$ and $G$, respectively. Then
218 \[
219  [u]=[v]\text{ in }\Z^d/(\ker J+\ker K)
220 \]
221 if and only if a single $y\equiv x\pmod{q^L}$ solves both systems modulo
222 $q^{L+1}$. Each separate label is independent of the chosen valid
223 correction. The common quotient is finite.
224 \end{corollary}
225 
Proof block: Simultaneous polynomial lifting · Go to statement · Read statement and proof side by side226 \begin{proof}
227 For each system, \eqref{eq:digit-correction} translates a valid next root
228 into a linear correction equation. Once $u$ corrects $F$, another digit
229 $w$ corrects $F$ precisely when $Jw=Ju$. The analogous condition for $G$
230 is $Kw=Kv$. Theorem~\ref{thm:common-correction} now gives the criterion.
231 Two valid corrections of one block differ by a vector in its Jacobian
232 kernel, so they have equal labels. Finiteness follows from either finite
233 residue target. An unconditional formulation quantifies over separately
234 valid $u,v$ with equal labels, thereby including their existence in the
235 criterion rather than assuming it.
236 \end{proof}
237 
238 See \lean{Komorebi.PolynomialShared.joint_lift_iff_class_eq} and
239 \lean{Komorebi.PolynomialShared.finite_polynomial_pair_compatibility}.
240 
241 For affine integer systems $F(X)=AX-b$ and $G(X)=BX-c$, where
242 $A:\Z^d\to\Z^e$ and $B:\Z^d\to\Z^f$ are linear,
243 Corollary~\ref{cor:shared-polynomial} holds for $q\ge1$ and every
244 $L\ge0$, including depth zero. Here $x$ is a common root modulo $q^L$,
245 and $J$ and $K$ are the reductions of $A$ and $B$ with domain $\Z^d$.
246 Given separately valid corrections $u,v$, a simultaneous next lift exists
247 if and only if their classes in $\Z^d/(\ker J+\ker K)$ agree. The quotient
248 is finite, and each label is independent of the chosen valid correction.
249 Indeed, Proposition~\ref{prop:affine-obstruction} supplies the correction
250 equation without a positive-depth restriction, and the proof of
251 Theorem~\ref{thm:common-correction} then applies unchanged. The formal
252 statement is \lean{Komorebi.AffinePair.joint_lift_iff_class_eq}.
253 Quantifying over separately valid corrections with equal labels also
254 includes their existence in the criterion, as in
255 \lean{Komorebi.AffinePair.finite_affine_pair_compatibility}.
256 Separate liftability alone is insufficient. At $x=0$ modulo two,
257 $F(X)=X$ and $G(X)=X-2$ both lift to modulus four, but their correcting
258 digits are respectively $0$ and $1$ modulo two. No single residue solves
259 both equations modulo four.
260 
261 \subsection{Correction torsors and exact residue counts}
262 
263 Integer representatives and residue classes at the next level must also be
264 distinguished. For $q\ge1$ and $L\ge0$, the map
265 \[
266  S_q^d\longrightarrow
267  \{y\in(\Z/q^{L+1}\Z)^d:y\equiv x\pmod{q^L}\},
268  \qquad t\longmapsto x+q^L\widetilde t
269 \]
270 is a bijection, where $\widetilde t$ is any integer representative.
271 Independence of the representative and injectivity both follow by cancelling
272 $q^L$ in integer divisibility; surjectivity follows by expressing the lower
273 congruence as a multiple of $q^L$. This is the equivalence
274 \lean{Komorebi.ResidueLiftDigits.digitEquivResidue}.
275 
276 At positive polynomial depth, restrict it to the correction fiber
277 \[
278  \mathcal T_x=\{t\in S_q^d:\overline{r_x}+J_xt=0\}
279 \]
280 and the lift set
281 \[
282  \mathcal L_{x,L}=
283  \{y\in(\Z/q^{L+1}\Z)^d:y\equiv x\pmod{q^L},\ F(y)=0\}.
284 \]
285 The polynomial predicate in the second display is evaluation in the residue
286 ring. Evaluation on canonical integer representatives gives the same
287 predicate, because integer polynomial evaluation respects congruence.
288 
Statement: Torsor and lift cardinalities · Go to proof · Read statement and proof side by side289 \begin{theorem}[Torsor and lift cardinalities]\label{thm:lift-torsor-count}
290 Under the hypotheses of Theorem~\ref{thm:finite-polynomial-obstruction},
291 there is an equivalence $\mathcal T_x\simeq\mathcal L_{x,L}$.
292 Every nonempty fiber is a torsor for $\ker J_x$ under addition of
293 correction digits. If $q=p$ is prime and
294 $\rho_x=\rank_{\F_p}J_x$, then
295 \begin{equation}\label{eq:lift-count}
296  \#\mathcal L_{x,L}=
297  \begin{cases}p^{d-\rho_x},&o_x=0,\\0,&o_x\ne0,\end{cases}
298  \qquad
299  \#\mathcal O_x=p^{e-\rho_x}.
300 \end{equation}
301 \end{theorem}
302 
Proof block: Torsor and lift cardinalities · Go to statement · Read statement and proof side by side303 \begin{proof}
304 Equation~\eqref{eq:digit-correction} identifies exactly which points of the
305 residue fiber satisfy the equations, proving the restricted equivalence.
306 If $u,t\in\mathcal T_x$, subtraction gives $J_x(t-u)=0$. Conversely,
307 adding any element of $\ker J_x$ preserves the correction equation. The
308 unique kernel vector carrying $u$ to $t$ is $t-u$, so the action is free
309 and transitive. Choosing one valid digit identifies the fiber with the
310 kernel, without making that choice part of its translation action.
311 
312 For prime $p$, rank-nullity gives
313 $\dim\ker J_x=d-\rho_x$ and
314 $\dim(\F_p^e/\im J_x)=e-\rho_x$. The cardinality of an
315 $n$-dimensional $\F_p$-space is $p^n$. Combine these identities with the
316 obstruction criterion and the residue equivalence.
317 \end{proof}
318 
319 The cardinality formula is formalized by
320 \lean{Komorebi.PolynomialLiftCounts.finite_polynomial_lift_count}.
321 The explicit torsor and chosen-point equivalence are developed in
322 \lean{Komorebi.FiniteFiberCounts.translate_exists_unique} and
323 \lean{Komorebi.PolynomialLiftCounts.liftEquivKernel}.
324 For composite $q$, the torsor and kernel cardinality remain valid, while the
325 vector-space rank formula is unavailable. Multiplication by two on
326 $\Z/4\Z$ already has a kernel of size two.
327 
328 \subsection{Smooth compatible towers and exact roots}
329 
330 Surjectivity removes every residual obstruction and persists throughout a
331 positive-depth residue ball. This supplies the additional hypothesis needed
332 to iterate the finite theorem.
333 
Statement: Compatible polynomial tower · Go to proof · Read statement and proof side by side334 \begin{theorem}[Compatible polynomial tower]\label{thm:smooth-tower}
335 Let $q\ge1$, $L\ge1$, $F\in\Z[X_1,\ldots,X_d]^e$, and
336 $x\in\Z^d$ satisfy $F(x)\in q^L\Z^e$. Suppose $J_x:S_q^d\to S_q^e$
337 is surjective. There is a single sequence $z_n\in\Z^d$ such that
338 \begin{align*}
339  z_0&=x,& F(z_n)&\in q^{L+n}\Z^e,\\
340  z_{n+1}-z_n&\in q^{L+n}\Z^d,& J_{z_n}&=J_x.
341 \end{align*}
342 For $a\le b$, it also satisfies $z_b-z_a\in q^{L+a}\Z^d$.
343 \end{theorem}
344 
Proof block: Compatible polynomial tower · Go to statement · Read statement and proof side by side345 \begin{proof}
346 At level $N=L+n$, divide the residual by $q^N$. Surjectivity supplies
347 $t\in S_q^d$ with $J_{z_n}t=-\overline{F(z_n)/q^N}$. Choose an integer
348 representative and apply \eqref{eq:digit-correction} to obtain $z_{n+1}$.
349 The new point is congruent to $z_n$ modulo $q$. Evaluation of each formal
350 partial derivative therefore gives $J_{z_{n+1}}=J_{z_n}$.
351 
352 Construct the sequence recursively, retaining the root condition and the
353 fixed Jacobian at each step. Surjectivity at every later stage then follows
354 from the single initial assumption. The cross-level congruence follows by
355 induction, adding consecutive differences whose divisibilities all imply divisibility
356 by $q^{L+a}$.
357 \end{proof}
358 
359 The full tower statement is
360 \lean{Komorebi.PolynomialIntegerTower.exists_compatible_tower_strong}.
361 The proof constructs a compatible path using classical choice. It does not
362 claim an optimized procedure for selecting its digits.
363 
Statement: Completion and smooth branching · Go to proof · Read statement and proof side by side364 \begin{theorem}[Completion and smooth branching]\label{thm:smooth-padic-root}
365 In Theorem~\ref{thm:smooth-tower}, let $q=p$ be prime. The tower can be
366 chosen with a limit $a\in\Zp^d$ such that
367 \[
368  F(a)=0,\qquad z_n\longrightarrow a,\qquad
369  a-z_n\in p^{L+n}\Zp^d\quad(n\ge0).
370 \]
371 At each stage, the number of distinct next-level residue roots over $z_n$
372 is exactly $p^{d-e}$, and the finite obstruction module has one element.
373 If $d=e$, there is exactly one root of $F$ in $B_L(x)$.
374 \end{theorem}
375 
Proof block: Completion and smooth branching · Go to statement · Read statement and proof side by side376 \begin{proof}
377 Cross-level compatibility bounds the supremum distance between later terms
378 by $p^{-(L+n)}$. Completeness gives a limit, and closed norm bounds retain
379 the congruence to every $z_n$. View the coefficients of the original integer
380 polynomials in $\Zp$. Their evaluations satisfy
381 both $F_i(z_n)\to F_i(a)$, by continuity, and $F_i(z_n)\to0$, by their
382 growing divisibility. Uniqueness of limits gives exact vanishing.
383 
384 Surjectivity gives $\rank J_x=e\le d$. Theorem~\ref{thm:lift-torsor-count}
385 then gives $p^{d-e}$ next residue roots and obstruction cardinality one at
386 every stage.
387 
388 For square uniqueness, let $a,b\in B_L(x)$ be arbitrary exact roots.
389 Their canonical integer truncations are genuine roots in the respective
390 finite residue rings, since evaluation commutes with reduction. They agree
391 at depth $L$. If they agree at depth $N\ge L$, both next residues belong
392 to the same lift set, which has cardinality $p^{d-d}=1$. Induction gives
393 agreement at every depth. The residue maps separate $p$-adic integers, so
394 $a=b$. Existence was already supplied by the tower.
395 \end{proof}
396 
397 The endpoint construction is
398 \lean{Komorebi.PolynomialPadicLift.exists_padic_root_with_tower}, the
399 branching statement is
400 \lean{Komorebi.PolynomialSmoothCounts.exists_regular_tower}, and uniqueness
401 for all roots in the ball is
402 \lean{Komorebi.PolynomialPadicUnique.exists_unique_padic_root}.
403 
404 \begin{remark}\label{rem:singular-tower-boundary}
405 The one-step singular criterion and the smooth infinite theorem have
406 different hypotheses. The polynomial $X^2-5$ has odd roots modulo two and
407 four but has no root modulo eight. Thus a previous zero obstruction does
408 not force the next one to vanish. Also, rectangular surjectivity alone
409 does not imply uniqueness: $F(X,Y)=X$ has the distinct dyadic roots
410 $(0,0)$ and $(0,2)$ in the same residue ball modulo two. These examples show
411 why the hypotheses of the tower theorem and its uniqueness clause are needed.
412 \end{remark}
413 
414 \subsection{Coefficient stability and continuous root charts}
415 
Statement: Smooth coefficient stability · Go to proof · Read statement and proof side by side416 \begin{proposition}[Smooth coefficient stability]\label{prop:smooth-coefficient-stability}
417 Let $p$ be prime, $M\ge1$, $F,H\in\Z[X_1,\ldots,X_d]^e$, and
418 $c\in p^M\Z$. Suppose $DF(x)\bmod p$ is surjective for an integer
419 $x\in\Z^d$. If $a\in\Zp^d$ satisfies $F(a)=0$ and
420 $a\equiv x\pmod p$, then there is a root $b$ of $G=F+cH$ with
421 $b-a\in p^M\Zp^d$.
422 
423 If $d=e$ and $M\ge L\ge1$, every pair of roots $a,b\in B_L(x)$ of
424 $F$ and $G$, respectively, satisfies $b-a\in p^M\Zp^d$. The perturbed
425 root is unique in that ball whenever it exists.
426 \end{proposition}
427 
Proof block: Smooth coefficient stability · Go to statement · Read statement and proof side by side428 \begin{proof}
429 Since $p\mid c$, differentiation gives
430 $DG(x)\equiv DF(x)\pmod p$. Truncate $a$ to an integer vector $y$ at
431 depth $M$. Then $F(y)\equiv0\pmod{p^M}$, hence also
432 $G(y)\equiv0\pmod{p^M}$. Congruence of $y$ and $x$ modulo $p$ preserves
433 the reduced Jacobian. The smooth root theorem gives
434 $b\equiv y\equiv a\pmod{p^M}$.
435 
436 In the square case this constructed root lies in $B_L(x)$ because $M\ge L$.
437 Square uniqueness for $G$ identifies it with every competing root in that
438 ball. The construction therefore gives the precision assertion for an
439 arbitrary root there.
440 \end{proof}
441 
442 See \lean{Komorebi.PolynomialRootStability.exists_nearby_perturbed_root}
443 and \lean{Komorebi.PolynomialRootStability.perturbed_roots_congruent}.
444 The scalar $c$ may be negative or zero. The weighted theorems below allow
445 arbitrary integral $p$-adic coefficients and give an explicit first-order
446 displacement.
447 
Statement: Continuous charts with a selected Jacobian minor · Go to proof · Read statement and proof side by side448 \begin{theorem}[Continuous charts with a selected Jacobian minor]
449 \label{thm:continuous-parameter-chart}
450 Let $p$ be prime, $L\ge1$,
451 $F\in\Z[X_1,\ldots,X_{e+k}]^e$, and $x\in\Z^{e+k}$ satisfy
452 $F(x)\in p^L\Z^e$. Suppose the full reduced Jacobian is surjective.
453 There is a permutation $\sigma$ of the coordinates such that, writing
454 $\sigma x=(y_0,t_0)$ with $e$ solved coordinates and $k$ parameter
455 coordinates, the parameter ball
456 $T=t_0+p^L\Zp^k$ is homeomorphic to the entire root locus
457 \[
458  \mathcal R=\{z\in B_L(x):F(z)=0\}.
459 \]
460 The inverse homeomorphism is the actual free-coordinate projection
461 $z\mapsto\operatorname{free}(\sigma z)$. If $h:T\to\mathcal R$ is the
462 forward map, then for every $N\ge0$,
463 \begin{equation}\label{eq:chart-congruence}
464  h(t)\equiv h(u)\pmod{p^N}
465  \quad\Longleftrightarrow\quad t\equiv u\pmod{p^N}.
466 \end{equation}
467 Equivalently, $\sigma h(t)=(\phi(t),t)$ for a continuous
468 $\phi:T\to y_0+p^L\Zp^e$ whose graph is the entire reordered root locus.
469 \end{theorem}
470 
Proof block: Continuous charts with a selected Jacobian minor · Go to statement · Read statement and proof side by side471 \begin{proof}
472 First consider a square integer polynomial map $P$ whose reduced Jacobian
473 at $x$ is surjective. Its Jacobian is invertible over $\F_p$. A digit
474 comparison using Taylor expansion shows that equal outputs modulo
475 $p^{N+1}$ force equal inputs modulo $p^{N+1}$ whenever the inputs already
476 agree modulo $p^N$ and belong to $B_1(x)$. Induction and integer truncation
477 give, for arbitrary $a,b\in B_1(x)$,
478 \[
479  P(a)\equiv P(b)\pmod{p^N}
480  \quad\Longleftrightarrow\quad a\equiv b\pmod{p^N}.
481 \]
482 
483 More generally, for a rectangular map with surjective reduced Jacobian,
484 \begin{equation}\label{eq:polynomial-ball-image}
485  P(B_L(x))=P(x)+p^L\Zp^e.
486 \end{equation}
487 One inclusion follows from polynomial congruence. For integer targets in
488 the right-hand ball, subtract the target from the constant terms and use
489 the smooth root theorem. For arbitrary $p$-adic targets, approximate by
490 integer truncations. The input ball is compact, so its continuous image is
491 closed. It contains all these approximants and hence their limit. This
492 argument does not assume that independently chosen preimages form a
493 compatible sequence.
494 
495 For square $P$, the resulting bijection between the two compact residue
496 balls is continuous, and its target is Hausdorff. It is therefore a
497 homeomorphism, with the same congruence preservation for its inverse.
498 
499 Now suppose a chosen set of $e$ columns of $DF(x)\bmod p$ is independent,
500 and put those coordinates first. Apply the square result to the augmented
501 polynomial map
502 \[
503  \Psi(Y,T)=(F(Y,T),T).
504 \]
505 Its reduced Jacobian has upper blocks $(D_YF,D_TF)$ and lower blocks
506 $(0,I_k)$, so it is invertible. For $t\in T$, the target $(0,t)$ belongs
507 to $\Psi(x)+p^L\Zp^{e+k}$ because $F(x)\equiv0\pmod{p^L}$.
508 The inverse of $\Psi$ at that target gives the unique root with parameters
509 $t$. The inverse congruence property gives one direction of
510 \eqref{eq:chart-congruence}; projection onto the parameter coordinates
511 gives the other.
512 
513 Finally, surjectivity of the original rectangular Jacobian guarantees a
514 basis among its columns. Extend the corresponding injection of coordinate
515 indices to a permutation $\sigma$. Renaming the variables by
516 $\sigma^{-1}$ transports polynomial evaluation and every formal partial
517 derivative. The fixed-coordinate construction therefore applies to the
518 original system after undoing the permutation.
519 \end{proof}
520 
521 The main theorem is
522 \lean{Komorebi.PolynomialGeneralChart.exists_parameter_homeomorph}.
523 The square local inverse and surjectivity for arbitrary targets are
524 \lean{Komorebi.PolynomialLocalInverse.localHomeomorph} and
525 \lean{Komorebi.PolynomialLocalSurjective.exists_padic_preimage}.
526 The center $x$ is only an approximate root: the chart need not satisfy
527 $\phi(t_0)=y_0$ unless $F(x)=0$ exactly. The assertion selects suitable
528 coordinates; it does not permit an arbitrary prescribed solved block.
529 
530 \subsection{Prescribed parameters and their obstruction}
531 
532 Suppose now that the split into solved variables and parameter variables
533 is fixed in advance. Let
534 \[
535  F\in\Z[Y_1,\ldots,Y_m,T_1,\ldots,T_k]^e,\qquad x=(y_0,t_0),
536 \]
537 and assume $F(x)=q^Lr_x$ with $q\ge1$ and $L\ge1$. Write the reduced
538 Jacobian as
539 \[
540  DF(x)\bmod q=(J_x\ K_x),\qquad
541  J_x:S_q^m\to S_q^e,\quad K_x:S_q^k\to S_q^e.
542 \]
543 For a prescribed parameter digit $v\in S_q^k$, let $\mathcal L_{x,L,v}$
544 be the set of next residue roots over $x$ whose parameter coordinates are
545 $t_0+q^L\widetilde v$ modulo $q^{L+1}$.
546 
Statement: Prescribed-parameter obstruction and count · Go to proof · Read statement and proof side by side547 \begin{theorem}[Prescribed-parameter obstruction and count]
548 \label{thm:prescribed-obstruction}
549 Define
550 \[
551  o_x(v)=[\overline{r_x}+K_xv]\in S_q^e/\im J_x.
552 \]
553 Then $\mathcal L_{x,L,v}$ is nonempty if and only if $o_x(v)=0$.
554 When nonempty, it is a torsor for $\ker J_x$. If $q=p$ is prime and
555 $\rho_x=\rank_{\F_p}J_x$, then
556 \begin{equation}\label{eq:prescribed-count}
557  \#\mathcal L_{x,L,v}
558  =\begin{cases}p^{m-\rho_x},&o_x(v)=0,\\0,&o_x(v)\ne0,\end{cases}
559  \qquad \#(\F_p^e/\im J_x)=p^{e-\rho_x}.
560 \end{equation}
561 The criterion holds uniformly for every prescribed $v$ without a
562 surjectivity hypothesis.
563 \end{theorem}
564 
Proof block: Prescribed-parameter obstruction and count · Go to statement · Read statement and proof side by side565 \begin{proof}
566 A candidate for the next lift has the form
567 $x+q^L(\widetilde u,\widetilde v)$, with solved digit $u\in S_q^m$.
568 Its Taylor correction equation is
569 \[
570  \overline{r_x}+J_xu+K_xv=0.
571 \]
572 Solvability is exactly vanishing of the displayed cokernel class. Restrict
573 the residue-digit equivalence to the prescribed parameter coordinates.
574 This identifies the lift fiber with the solved-digit fiber.
575 Translation by $\ker J_x$ is free and transitive on any nonempty such
576 fiber. The prime-field count follows from rank-nullity as before.
577 \end{proof}
578 
579 The formal statements start from the lower root and construct its residual:
580 \lean{Komorebi.PolynomialPrescribedObstruction.finite_prescribed_obstruction}
581 and \lean{Komorebi.PolynomialPrescribedObstruction.finite_prescribed_lift_count}.
582 For $F(Y,T)=T$ at the dyadic origin, the full Jacobian $(0\ 1)$ is
583 surjective but $J_x=0$. Prescribing $v=1$ forces $T=2\pmod4$, so no root
584 exists; prescribing $v=0$ gives two choices of $Y$ modulo four over the
585 initial zero residue. This example explains why the criterion depends on
586 the solved block, rather than merely on the full Jacobian.
587 
Statement: Every compatible integer parameter path · Go to proof · Read statement and proof side by side588 \begin{theorem}[Every compatible integer parameter path]
589 \label{thm:prescribed-integer-tower}
590 In the preceding notation, assume $J_x$ is surjective. For every supplied
591 integer path $t_n\in\Z^k$ satisfying
592 \[
593  t_0=\operatorname{free}(x),\qquad
594  t_{n+1}-t_n\in q^{L+n}\Z^k,
595 \]
596 there is a compatible polynomial tower $z_n\in\Z^{m+k}$ with
597 \[
598  z_0=x,\quad \operatorname{free}(z_n)=t_n,\quad
599  F(z_n)\in q^{L+n}\Z^e,\quad
600  z_{n+1}-z_n\in q^{L+n}\Z^{m+k}.
601 \]
602 The free-coordinate equality is exact in integers. Both reduced Jacobian
603 blocks remain fixed, and $z_b-z_a\in q^{L+a}\Z^{m+k}$ whenever $a\le b$.
604 \end{theorem}
605 
Proof block: Every compatible integer parameter path · Go to statement · Read statement and proof side by side606 \begin{proof}
607 At level $N=L+n$, write the supplied parameter increment exactly as
608 $t_{n+1}-t_n=q^Nw$ with $w\in\Z^k$. Surjectivity of the solved block
609 gives a digit $u$ satisfying
610 $J_{z_n}u=-\overline{F(z_n)/q^N}-K_{z_n}\overline w$.
611 Choose an integer representative $\widetilde u$ and set
612 $z_{n+1}=z_n+q^N(\widetilde u,w)$. Its parameter coordinates equal the
613 supplied target exactly. Taylor expansion proves the next root condition,
614 while congruence modulo $q$ preserves the full reduced Jacobian.
615 Construct the sequence recursively, preserving the exact parameter
616 coordinates and the fixed solved Jacobian. The earlier cross-level
617 argument proves all the stated integer congruences.
618 \end{proof}
619 
620 This is
621 \lean{Komorebi.PolynomialPrescribedIntegerTower.exists_prescribed_tower_strong}.
622 In particular, no assumption about solvability at each later level has been
623 added to the initial surjectivity condition.
624 
Statement: Arbitrary p-adic parameter endpoints · Go to proof · Read statement and proof side by side625 \begin{theorem}[Arbitrary $p$-adic parameter endpoints]
626 \label{thm:prescribed-padic-tower}
627 Let $q=p$ be prime in Theorem~\ref{thm:prescribed-integer-tower}.
628 For every $\tau\in t_0+p^L\Zp^k$, there are an integer tower $z_n$ and
629 $b\in\Zp^{m+k}$ such that
630 \[
631  F(b)=0,\qquad\operatorname{free}(b)=\tau,\qquad
632  z_n\longrightarrow b,\qquad b-z_n\in p^{L+n}\Zp^{m+k}.
633 \]
634 The initial value is $z_0=x$. At every stage and for every proposed
635 parameter digit $v\in\F_p^k$, the corresponding next residue fiber has
636 exactly $p^{m-e}$ elements. If $m=e$, then for each $\tau$ there is exactly
637 one such root in $B_L(x)$, independently of all choices of integer
638 approximants and correcting digits.
639 \end{theorem}
640 
Proof block: Arbitrary p-adic parameter endpoints · Go to statement · Read statement and proof side by side641 \begin{proof}
642 Set the first integer parameter approximation equal to the prescribed
643 $t_0$. For $n\ge1$, use canonical representatives of
644 $\tau\bmod p^{L+n}$. The initial congruence and truncation precision give
645 \[
646  \tau-t_n\in p^{L+n}\Zp^k.
647 \]
648 Subtracting consecutive relations gives compatibility in $\Zp$.
649 Faithfulness of integer divisibility under $\Z\hookrightarrow\Zp$
650 gives compatibility in $\Z$, and the same norm bounds give $t_n\to\tau$.
651 Theorem~\ref{thm:prescribed-integer-tower} and completion now produce $b$
652 with exact polynomial vanishing and all retained precisions. Each free
653 coordinate has both the corresponding coordinate of $b$ and that of
654 $\tau$ as its limit, proving exact parameter equality.
655 
656 The solved Jacobian remains surjective, so every shifted obstruction
657 $[\overline r+K_{z_n}v]$ vanishes. Formula~\eqref{eq:prescribed-count}
658 therefore gives $p^{m-e}$ choices for every parameter digit at every stage.
659 When $m=e$, the fixed-coordinate chart in the proof of
660 Theorem~\ref{thm:continuous-parameter-chart} contains every root in the
661 initial ball with the specified parameters. Its uniqueness proves the
662 endpoint assertion. This is uniqueness of the actual endpoint, not of the
663 integer representatives used to approach it.
664 \end{proof}
665 
666 The endpoint theorems are
667 \lean{Komorebi.PolynomialPrescribedPadicTower.exists_prescribed_padic_root_with_tower}
668 and \lean{Komorebi.PolynomialPrescribedPadicTower.exists_unique_prescribed_padic_root}.
669 The separate supplied-path theorem
670 \lean{Komorebi.PolynomialPrescribedPadicTower.exists_root_with_prescribed_path}
671 accepts any compatible integer parameter path with limit $\tau$.
672 For $m>e$, endpoint uniqueness is false in general: the system
673 $F(Y_1,Y_2,T)=Y_1$ has two distinct roots $(0,0,0)$ and $(0,2,0)$ in the
674 same dyadic ball with identical parameter value.
675 
676 \subsection{Weighted lifting for a nonunit Jacobian}
677 
678 The remaining theorems in this section allow arbitrary coefficients and
679 centers in $R=\Zp$. They concern square solved Jacobians invertible over
680 $\Qp$, even when their reductions modulo $p$ are singular. The exponent
681 controlling an integral inverse is retained explicitly.
682 
Statement: Weighted nonlinear lifting · Go to proof · Read statement and proof side by side683 \begin{theorem}[Weighted nonlinear lifting]\label{thm:weighted-lifting}
684 Let $p$ be prime, $d,s,r\in\N$, $F\in R[X_1,\ldots,X_d]^d$, and
685 $a\in R^d$. Set $J=DF(a)$. Suppose
686 \begin{equation}\label{eq:weighted-hypotheses}
687  J\in\operatorname{GL}_d(\Qp),\qquad
688  p^sJ^{-1}\in M_d(R),\qquad F(a)\in p^rR^d,\qquad r>2s.
689 \end{equation}
690 Then there is exactly one root $b$ of $F$ in $a+p^{s+1}R^d$, and it
691 satisfies
692 \begin{equation}\label{eq:weighted-displacement}
693  b-a\in p^{r-s}R^d.
694 \end{equation}
695 Uniqueness holds throughout the full ball of depth $s+1$.
696 \end{theorem}
697 
Proof block: Weighted nonlinear lifting · Go to statement · Read statement and proof side by side698 \begin{proof}
699 Let $A=p^sJ^{-1}\in M_d(R)$. Inclusion into $\Qp$ and its injectivity
700 give the two integral identities
701 \[
702  AJ=JA=p^sI_d.
703 \]
704 These identities are also an equivalent integral certificate for the
705 first two hypotheses of \eqref{eq:weighted-hypotheses}. In particular,
706 $A$ is injective: $Aw=0$ implies $p^sw=JAw=0$, hence $w=0$.
707 
708 Precondition the polynomial system by $A$ and set $c=p^{s+1}$.
709 Its derivative at $a$ is $AJ=p^sI_d$. Lemma~\ref{lem:polynomial-taylor}
710 gives a polynomial vector $Q$ with $Q(0)=0$ and
711 \[
712  (AF)(a+cu)=(AF)(a)+p^{2s+1}u+p^{2s+2}Q(u).
713 \]
714 Since $A$ is integral, $(AF)(a)\in p^rR^d$. The strict integer inequality
715 $r>2s$ permits $k=r-(2s+1)\ge0$ and a vector $C\in p^kR^d$ such that
716 $(AF)(a)=p^{2s+1}C$. The normalized root equation is therefore
717 \begin{equation}\label{eq:weighted-fixed-point}
718  u=-C-pQ(u).
719 \end{equation}
720 
721 Integral polynomial evaluation is $1$-Lipschitz for the supremum
722 $p$-adic metric: a common divisibility of input differences is preserved
723 under addition and multiplication by integral elements. Consequently the
724 right side of \eqref{eq:weighted-fixed-point} has contraction constant
725 $|p|_p<1$ on the complete space $R^d$. It has a unique fixed point $u$.
726 
727 To obtain the sharper displacement, begin with $u\in R^d$. If
728 $u\in p^nR^d$, then $Q(0)=0$ and polynomial congruence give
729 $Q(u)\in p^nR^d$. For $n<k$, both $C$ and $pQ(u)$ are divisible by
730 $p^{n+1}$. Equation~\eqref{eq:weighted-fixed-point} therefore improves
731 the divisibility of $u$ by one digit. Induction gives $u\in p^kR^d$.
732 Thus $b=a+p^{s+1}u$ satisfies \eqref{eq:weighted-displacement}, because
733 $s+1+k=r-s$. Its normalized preconditioned value vanishes, and injectivity
734 of $A$ gives $F(b)=0$.
735 
736 Every competing root $z\in a+p^{s+1}R^d$ can be written
737 $z=a+p^{s+1}w$. Its root equation implies the same fixed-point
738 equation after cancellation of the nonzero scalar $p^{2s+1}$.
739 Contraction uniqueness gives $w=u$, proving uniqueness on the entire
740 stated ball.
741 \end{proof}
742 
743 The existence and uniqueness statements are
744 \lean{Komorebi.PolynomialWeightedLift.exists_weighted_root} and
745 \lean{Komorebi.PolynomialWeightedLift.exists_unique_weighted_root}.
746 The inverse hypothesis in Lean specifies an integral matrix whose image
747 is exactly $p^sJ^{-1}$; it does not substitute a potentially larger
748 determinant valuation for $s$.
749 
750 \begin{example}[Strict threshold and displacement boundary]
751 \label{ex:weighted-boundary}
752 For $p=2$, $F(X)=X^2+3$, and $a=1$, one has $F(a)=4$ and $DF(a)=2$.
753 Thus $s=1$ and $r=2$ satisfy every displayed hypothesis except the strict
754 inequality. No root exists in $\Z_2$, since none exists modulo eight.
755 Hence $r\ge2s$ cannot replace $r>2s$ uniformly. Also,
756 $F(X)=p^sX+p^r$ has root $-p^{r-s}$, whose displacement is not divisible
757 by $p^{r-s+1}$. The guaranteed displacement cannot uniformly gain a digit.
758 \end{example}
759 
760 \subsection{First-order coefficient and parameter motion}
761 
Statement: Weighted coefficient deformation · Go to proof · Read statement and proof side by side762 \begin{theorem}[Weighted coefficient deformation]\label{thm:coefficient-motion}
763 Let $F,H\in R[X_1,\ldots,X_d]^d$, $F(a)=0$, and $J=DF(a)$. Suppose
764 $J\in\operatorname{GL}_d(\Qp)$, $p^sJ^{-1}\in M_d(R)$, and $M>2s$.
765 For $G=F+p^MH$, there is exactly one root $b\in a+p^{s+1}R^d$.
766 It satisfies $b-a\in p^{M-s}R^d$ and, in $\Qp^d$,
767 \begin{equation}\label{eq:coefficient-first-order}
768  b-a=-p^MJ^{-1}H(a)+\varepsilon,
769  \qquad\varepsilon\in p^{2M-3s}R^d.
770 \end{equation}
771 Only the original Jacobian $DF(a)$ is subject to an inverse hypothesis.
772 \end{theorem}
773 
Proof block: Weighted coefficient deformation · Go to statement · Read statement and proof side by side774 \begin{proof}
775 Retain the original certificate $A=p^sJ^{-1}$ and put $c=p^{s+1}$.
776 Taylor expansion and a polynomial difference identity yield polynomial
777 vectors $Q_F,Q_H$, both zero at the origin, such that
778 \[
779  (AF)(a+cu)=p^{2s+1}u+p^{2s+2}Q_F(u),\qquad
780  (AH)(a+cu)=AH(a)+cQ_H(u).
781 \]
782 Consequently
783 \[
784  (AG)(a+cu)=p^{2s+1}\bigl(C+u+pQ(u)\bigr),
785 \]
786 where
787 \[
788  C=p^{M-(2s+1)}AH(a),\qquad
789  Q=Q_F+p^{M-s-1}Q_H,\qquad Q(0)=0.
790 \]
791 All exponents are nonnegative. The same contraction and divisibility
792 argument as in Theorem~\ref{thm:weighted-lifting} gives the root,
793 the displacement $p^{M-s}$, and full-ball uniqueness. This constructs the
794 root without introducing an inverse hypothesis for $DG(a)$.
795 
796 For the error estimate, let $\delta=b-a$ and $D=M-s$. Taylor's theorem
797 for the preconditioned polynomial gives
798 \[
799  E_F=(AF)(b)-(AF)(a)-p^s\delta\in p^{2D}R^d.
800 \]
801 Polynomial congruence gives
802 $E_H=(AH)(b)-(AH)(a)\in p^DR^d$.
803 The equations $F(a)=0$ and $G(b)=0$ imply
804 \[
805  p^s\delta+p^MAH(a)=-E_F-p^ME_H\in p^{2D}R^d,
806 \]
807 because $M+D\ge2D$. Cancel $p^s$ in the integral domain $R$ to obtain
808 \[
809  \delta+p^{M-s}AH(a)\in p^{2M-3s}R^d.
810 \]
811 This integral vector is $\varepsilon$. After inclusion into $\Qp$,
812 $p^{M-s}A=p^MJ^{-1}$ gives \eqref{eq:coefficient-first-order}.
813 \end{proof}
814 
815 The complete theorem is
816 \lean{Komorebi.PolynomialRootMotion.exists_unique_root_motion}.
817 The error depth exceeds the displacement depth by $M-2s\ge1$. It is a
818 guaranteed divisibility, not an assertion of exact valuation for every
819 system.
820 
Statement: Joint coefficient and parameter deformation · Go to proof · Read statement and proof side by side821 \begin{theorem}[Joint coefficient and parameter deformation]
822 \label{thm:joint-deformation}\leavevmode\par
823 Let $F,H\in R[Y_1,\ldots,Y_e,T_1,\ldots,T_k]^e$ and
824 $a=(y_0,t_0)\in R^{e+k}$ satisfy $F(a)=0$. Define the actual blocks
825 \[
826  J=D_YF(a)\in M_e(R),\qquad K=D_TF(a)\in M_{e\times k}(R).
827 \]
828 Suppose $J\in\operatorname{GL}_e(\Qp)$,
829 $p^sJ^{-1}\in M_e(R)$, and $M>2s$. For every $v\in R^k$, set
830 \[
831  \tau=t_0+p^Mv,\qquad G=F+p^MH.
832 \]
833 There is exactly one $y\in y_0+p^{s+1}R^e$ with $G(y,\tau)=0$.
834 It satisfies
835 \begin{equation}\label{eq:joint-first-order}
836  \begin{aligned}
837   y-y_0&\in p^{M-s}R^e,\\
838   y-y_0&=-p^MJ^{-1}\bigl(H(a)+Kv\bigr)+\varepsilon,
839   \qquad\varepsilon\in p^{2M-3s}R^e.
840  \end{aligned}
841 \end{equation}
842 The equality involving $J^{-1}$ is in $\Qp^e$, with an integral error
843 vector. The parameter equality is exact.
844 \end{theorem}
845 
Proof block: Joint coefficient and parameter deformation · Go to statement · Read statement and proof side by side846 \begin{proof}
847 Use the augmented polynomial systems
848 \[
849  \mathcal F(Y,T)=(F(Y,T),T-t_0),\qquad
850  \mathcal H(Y,T)=(H(Y,T),-v).
851 \]
852 Then $\mathcal F(a)=0$, and its derivative is
853 \[
854  B=D\mathcal F(a)=\begin{pmatrix}J&K\\0&I_k\end{pmatrix}.
855 \]
856 For $A=p^sJ^{-1}\in M_e(R)$ and $c=p^s$, define
857 \[
858  C=\begin{pmatrix}A&-AK\\0&cI_k\end{pmatrix}.
859 \]
860 The identities $AJ=JA=cI_e$ give $CB=BC=cI_{e+k}$. In the second
861 product, the upper right block is $-JAK+cK=0$; in the first, it is
862 $AK-AK=0$. Thus augmentation preserves the original inverse bound $s$.
863 
864 Theorem~\ref{thm:coefficient-motion} gives a unique root $b$ of
865 $\mathcal F+p^M\mathcal H$ in $a+p^{s+1}R^{e+k}$, with displacement
866 depth $M-s$. Its last equations say exactly
867 $b_T=t_0+p^Mv=\tau$. Its first equations are $G(b)=0$.
868 The integral first-order expression uses
869 \[
870  C\binom{H(a)}{-v}
871  =\binom{A(H(a)+Kv)}{-p^sv}.
872 \]
873 Projection onto the solved coordinates gives
874 \[
875  b_Y-y_0+p^{M-s}A(H(a)+Kv)\in p^{2M-3s}R^e.
876 \]
877 The same inclusion identity as before converts this to
878 \eqref{eq:joint-first-order}.
879 
880 Finally, if $z\in y_0+p^{s+1}R^e$ is any competing solved root with
881 parameters $\tau$, then $(z,\tau)$ belongs to the full augmented ball.
882 Indeed, $M>2s$ implies $M\ge s+1$. Full-point uniqueness therefore gives
883 $(z,\tau)=b$. This comparison proves uniqueness on exactly the solved
884 ball stated in the theorem.
885 \end{proof}
886 
887 The exact solved-coordinate statement is
888 \lean{Komorebi.PolynomialJointDeformation.exists_joint_deformation},
889 with its unique-existence interface
890 \lean{Komorebi.PolynomialJointDeformation.exists_unique_joint_deformation}.
891 The triangular inverse identities hold over arbitrary commutative rings,
892 so they apply in particular over the $p$-adic integers.
893 
894 \begin{example}[First-order sign and error precision]\label{ex:motion-boundary}
895 For $p=2$, $s=0$, $M=2$, $F(Y,T)=Y+T$, $H=1$, $a=0$, and $v=1$,
896 the prescribed parameter is $\tau=4$ and the solved root is $y=-8$.
897 Here $J=K=1$, and the forcing term is $H(a)+Kv=2$. Omitting the parameter
898 term would predict $-4$, and reversing its sign would predict $0$.
899 The corresponding errors $-4$ and $-8$ are both outside
900 $2^{2M}\Z_2=16\Z_2$. Thus either change would violate the stated error
901 bound.
902 
903 The error exponent cannot uniformly be increased. For
904 $F(Y,T)=Y+Y^2+T$, $H=0$, $a=0$, $p=2$, $s=0$, $M=1$, and $v=1$,
905 there is an even root $y$ of $y+y^2+2=0$. Its equation forces
906 $y\equiv2\pmod4$ and $y+2=-y^2$, so
907 \[
908  4\mid y+2,\qquad 8\nmid y+2.
909 \]
910 Thus the error depth $2M-3s=2$ is attained even for parameter-only motion.
911 The same quadratic with a constant coefficient perturbation gives the
912 coefficient-only boundary. These examples refute a uniform extra error
913 digit; they do not assert optimality for every individual choice of
914 $p,s,M$.
915 \end{example}
916 
917 The combined results establish finite singular obstructions, smooth
918 compatible towers, full continuous root charts after a suitable coordinate
919 choice, and quantitative deformation for a rationally invertible solved
920 Jacobian. Rationally rank-deficient persistence remains a separate problem.
921 The analytic solution-map theorem in the next section supplies the
922 regularity conclusion for these same derivative blocks.

Back to source controls

Other PDFs for this work

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: 47225f39e2cbd069e1ea1b2ea218522fd4dce353e1c1ca718db5e6c246a6d441

Original source on GitHub

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation