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

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

1 \hypertarget{cont5:paper-ix-continuous-p-adic-parameter-charts}{%
2 \subsection{Paper IX: continuous p-adic parameter
3 charts}\label{cont5:paper-ix-continuous-p-adic-parameter-charts}}
4 
5 \textbf{Komorebi P. --- 8 September 2026.}
6 
7 \textbf{Fresh verification: PASS --- 40 checks, 244 explicit declaration
8 audits.}
9 
10 \hypertarget{cont5:main-statement}{%
11 \subsubsection{Main statement}\label{cont5:main-statement}}
12 
13 Let \(p\) be prime, \(L\ge1\), \(e,q\ge0\), and \[
14 F\in\mathbb Z[X_1,\ldots,X_{e+q}]^e,\qquad
15 x\in\mathbb Z^{e+q},\qquad F(x)\equiv0\pmod{p^L}.
16 \] Assume the actual reduced Jacobian \[
17 A_x=DF(x)\bmod p:\mathbb F_p^{e+q}\longrightarrow\mathbb F_p^e
18 \] is surjective. All vector congruences are coordinatewise.
19 
20 There is a coordinate permutation \(\sigma\), with
21 \((\sigma z)_i=z_{\sigma(i)}\). Write \(\sigma z=(y,t)\), using \(e\)
22 solved coordinates and \(q\) free coordinates. Define \[
23 (y_0,t_0)=\sigma x,\qquad
24 B=x+p^L\mathbb Z_p^{e+q},\qquad
25 T=t_0+p^L\mathbb Z_p^q,\qquad
26 \mathcal R=\{z\in B:F(z)=0\}.
27 \] There is a homeomorphism \[
28 h:T\xrightarrow{\ \sim\ }\mathcal R,\qquad
29 h^{-1}(z)=\operatorname{free}(\sigma z).
30 \] Equivalently, a continuous function
31 \(\phi:T\to y_0+p^L\mathbb Z_p^e\) gives the entire root locus through
32 \(\sigma h(t)=(\phi(t),t)\). Every parameter has exactly one
33 corresponding root in \(B\). For every \(N\ge0\), \[
34 \boxed{h(t)\equiv h(u)\pmod{p^N}\iff t\equiv u\pmod{p^N}.}
35 \]
36 
37 The coordinate choice is a conclusion. A suitable minor and a
38 preexisting chart are not hypotheses. The theorem covers the original
39 root locus after undoing the coordinate reordering. Since \(x\) is an
40 approximate root, it does not assert \(\phi(t_0)=y_0\) unless \(F(x)=0\)
41 exactly. The cases \(p=2\), \(L=1\), \(e=0\), and \(q=0\) are included.
42 
43 \hypertarget{cont5:supporting-theorems}{%
44 \subsubsection{Supporting theorems}\label{cont5:supporting-theorems}}
45 
46 For a rectangular integer polynomial system with a surjective reduced
47 Jacobian at \(x\), and \(L\ge1\), \[
48 F(x+p^L\mathbb Z_p^d)=F(x)+p^L\mathbb Z_p^e.
49 \] This covers arbitrary p-adic output targets. No lower-root hypothesis
50 is needed.
51 
52 When \(d=e\), the actual restricted polynomial map is a homeomorphism.
53 Moreover, for arbitrary \(a,b\in x+p\mathbb Z_p^d\) and every \(N\ge0\),
54 \[
55 F(a)\equiv F(b)\pmod{p^N}\iff a\equiv b\pmod{p^N}.
56 \] Its inverse therefore preserves every congruence depth.
57 
58 \hypertarget{cont5:proof-structure}{%
59 \subsubsection{Proof structure}\label{cont5:proof-structure}}
60 
61 \begin{enumerate}
62 \def\labelenumi{\arabic{enumi}.}
63 \tightlist
64 \item
65   The actual integer Taylor formula gives one additional input digit
66   from one additional output digit when the reduced square Jacobian is
67   surjective. Its finite domain and codomain have the same size, so it
68   is injective. Induction gives every integer precision.
69 \item
70   Canonical integer truncations of arbitrary p-adic vectors preserve
71   evaluation modulo each power of \(p\). Applying the integer result to
72   truncations proves the p-adic congruence equivalence.
73 \item
74   Subtracting an integer target from the constant terms leaves the
75   actual Jacobian unchanged. The previous root-lifting theorem supplies
76   a preimage. The image of the compact input ball is closed and contains
77   the convergent truncations of every admissible p-adic target, hence
78   contains the target. No compatibility of arbitrarily chosen preimages
79   is assumed.
80 \item
81   In the square case, the resulting continuous bijection from a compact
82   ball to a Hausdorff ball is a homeomorphism. Its forward map is actual
83   polynomial evaluation, and its inverse solves the output equation.
84 \item
85   For a specified surjective solved-variable block, apply this inverse
86   to the actual augmented polynomial map \[
87   \Psi(y,t)=(F(y,t),t).
88   \] Its derivative has an identity free-coordinate block. The inverse
89   at \((0,t)\) gives the root. The lower-root congruence places this
90   target in the output ball. Injectivity proves uniqueness and full
91   graph coverage. Projection identifies the inverse chart and reflects
92   congruences.
93 \item
94   The columns of a surjective finite-dimensional linear map contain a
95   basis. Select those columns and extend their injection to a coordinate
96   permutation. Polynomial renaming by \(\sigma^{-1}\) transports actual
97   evaluations and partial derivatives. The fixed-coordinate chart then
98   gives the main theorem on the entire original root locus.
99 \end{enumerate}
100 
101 \hypertarget{cont5:scope}{%
102 \subsubsection{Scope}\label{cont5:scope}}
103 
104 Coefficients are integers; roots and parameters are arbitrary p-adic
105 points. This supplies continuous polynomial parameter charts.
106 Analyticity, differentiability, arbitrary p-adic coefficient interfaces,
107 weighted lifting for nonunit Jacobians, and first-order root-motion
108 estimates are separate.
109 
110 Full Jacobian surjectivity need not allow an arbitrary prescribed
111 parameter choice. At the dyadic origin, \(F(X,T)=X^2-T\) has a
112 surjective full Jacobian but zero \(X\)-derivative. Prescribing \(T=2\)
113 gives no root even modulo \(4\). Suitable coordinates instead solve for
114 \(T\).
115 
116 \hypertarget{cont5:verification-and-provenance}{%
117 \subsubsection{Verification and
118 provenance}\label{cont5:verification-and-provenance}}
119 
120 The eight new mathematical modules contain 75 declarations: 60 theorems
121 and 15 definitions. The active polynomial dependency set contains 25
122 mathematical modules. Counts including inherited support and theorem
123 contracts are recorded separately in the final report.
124 
125 The exact universal statements are Lean theorems, not conclusions from
126 sampled numerical tests. The fresh gate rebuilds project sources with
127 warnings treated as errors, checks expanded theorem contracts, audits
128 explicit declarations, and checks rejected invalid extensions. Only
129 propext, Classical.choice, and Quot.sound are permitted as axiom
130 dependencies.
131 
132 Pinned runtime: Lean 4.34.0-rc2, Mathlib revision
133 \mcode{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.
134 
135 See \nolinkurl{inventory.json}, \nolinkurl{verification/polynomial_charts_verification.json},
136 and \nolinkurl{INDEPENDENT_PROOF_AUDIT.md} for actual evidence.
137 RECOVERY\_RECORD.md explains workspace maintenance, the intact previous
138 release, and reconstruction of the unpublished chart sources. Lost logs
139 are not represented as recovered.

Back to source controls

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