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

Back to source controls

Back to Realization Calculus