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{cont11:paper-ix-analytic-regularity-of-the-local-parameter-solution}{%
2 \subsection{Paper IX: analytic regularity of the local parameter
3 solution}\label{cont11:paper-ix-analytic-regularity-of-the-local-parameter-solution}}
4 
5 Author: Komorebi P.
6 
7 This block establishes both analyticity and differentiability of the
8 actual local polynomial solution map at a root with an invertible solved
9 Jacobian. The statements apply to every prime, including \(p=2\). They
10 also hold over any complete nontrivially normed field.
11 
12 Let \(\mathbb K\) be such a field, let \(e,k\in\mathbb N\), and let \[
13 F\in\mathbb K[Y_1,\ldots,Y_e,T_1,\ldots,T_k]^e,
14 \qquad a=(y_0,t_0)\in\mathbb K^e\times\mathbb K^k.
15 \] Evaluation of \(F\) means coordinatewise evaluation of its actual
16 polynomials. Define the actual derivative blocks \[
17 J=D_YF(a)\in M_e(\mathbb K),
18 \qquad K=D_TF(a)\in M_{e\times k}(\mathbb K),
19 \] where each matrix entry is the corresponding formal partial
20 derivative evaluated at \(a\). The hypotheses are exactly \[
21 F(a)=0,
22 \qquad J\in\operatorname{GL}_e(\mathbb K).
23 \] Neither analyticity of a proposed solution nor a derivative formula
24 is assumed.
25 
26 \textbf{Local analytic graph theorem.} There exist a map \[
27 \psi:\mathbb K^k\longrightarrow\mathbb K^e
28 \] and open sets \(U\subseteq\mathbb K^k\), \(V\subseteq\mathbb K^e\)
29 such that \[
30 t_0\in U,\qquad y_0\in V,\qquad \psi(t_0)=y_0,
31 \qquad \psi(U)\subseteq V.
32 \] The map is analytic at every point of \(U\), and its graph describes
33 all roots in the product neighborhood: \[
34 \forall t\in U\;\forall y\in V,
35 \qquad F(y,t)=0\quad\Longleftrightarrow\quad y=\psi(t).
36 \] At the base parameter it has the strict Fréchet derivative \[
37 \boxed{D\psi(t_0)=-J^{-1}K.}
38 \] Consequently it is differentiable on \(U\). The map is defined on the
39 ambient parameter space, but its root, analyticity and uniqueness
40 conclusions are restricted to the specified neighborhood. Uniqueness is
41 among solved coordinates in \(V\).
42 
43 The main Lean theorem is
44 \mcode{Komorebi.PolynomialAnalyticImplicit.exists_analytic_implicit}.
45 The matrix in its \mcode{HasStrictFDerivAt} conclusion is the
46 continuous linear map represented by the displayed matrix.
47 \mcode{differentiableOn_of_analytic_graph} records the
48 differentiability consequence.
49 
50 \textbf{Proof chain.} The scalar polynomial derivative bridge is proved
51 by induction on actual multivariate polynomials: constants, sums, and
52 multiplication by a variable. For a scalar polynomial \(P\), its strict
53 derivative is \[
54 v\longmapsto\sum_j \frac{\partial P}{\partial x_j}(a)v_j.
55 \] Assembling the coordinates gives the strict derivative of the
56 evaluated system as its actual Jacobian matrix. Polynomial analyticity
57 is supplied by the pinned Mathlib theorem for multivariate polynomial
58 evaluation, followed by finite coordinate assembly.
59 
60 Consider the actual augmented polynomial map \[
61 \Phi(y,t)=(F(y,t),t).
62 \] Its derivative and inverse derivative at \(a\) are \[
63 D\Phi(a)=
64 \begin{pmatrix}J&K\\0&I_k\end{pmatrix},
65 \qquad
66 D\Phi(a)^{-1}=
67 \begin{pmatrix}J^{-1}&-J^{-1}K\\0&I_k\end{pmatrix}.
68 \] The proof constructs the continuous linear equivalence from these
69 explicit matrices and verifies both inverse identities. The strict
70 inverse theorem gives a local inverse \(g\) of \(\Phi\), and the
71 analytic inverse result shows that this same inverse is analytic near
72 \(\Phi(a)=(0,t_0)\). Set \[
73 \psi(t)=\pi_Y g(0,t).
74 \] The two inverse identities and a sufficiently small product
75 neighborhood give the exact local graph statement. Composing the
76 derivative of \(g\) with parameter insertion and solved-coordinate
77 projection yields \(-J^{-1}K\). The chosen parameter neighborhood is
78 also restricted so that the inverse identities, analyticity and
79 inclusion \(\psi(U)\subseteq V\) hold there simultaneously.
80 
81 \textbf{Transfer to a supplied continuous solution.} Suppose
82 \(g:\mathbb K^k\to\mathbb K^e\) is continuous at \(t_0\),
83 \(g(t_0)=y_0\), and \[
84 F(g(t),t)=0
85 \] for all \(t\) in some neighborhood of \(t_0\). Under the same
86 invertibility hypothesis at \(a\), continuity places \(g(t)\) in the
87 uniqueness neighborhood \(V\) for all sufficiently close parameters.
88 Hence \(g\) and \(\psi\) agree on a neighborhood of \(t_0\). The theorem
89 \mcode{continuous_selection_regularity} transfers both analyticity
90 and the strict derivative formula to \(g\).
91 
92 There is also an explicit open-set version. Let \(U\) be open, let \(g\)
93 be continuous on \(U\), and suppose for every \(t\in U\) that \[
94 F(g(t),t)=0,
95 \qquad
96 J_t:=D_YF(g(t),t)\in\operatorname{GL}_e(\mathbb K).
97 \] Writing \(K_t=D_TF(g(t),t)\), the theorem
98 \mcode{continuous_selection_analyticOnNhd} proves \[
99 g\text{ is analytic at every }t\in U,
100 \qquad Dg(t)=-J_t^{-1}K_t\quad(t\in U),
101 \] with a strict Fréchet derivative at each point. The per-point
102 invertibility hypothesis is part of this theorem. This is a transfer
103 statement for continuous local root selections satisfying its
104 hypotheses; it does not assert equality of arbitrary global branch
105 choices.
106 
107 \textbf{Integral p-adic specialization.} For any prime \(p\), let \[
108 F\in\mathbb Z_p[Y,T]^e,
109 \qquad a\in\mathbb Z_p^{e+k},
110 \qquad F(a)=0.
111 \] Let \(\iota:\mathbb Z_p\hookrightarrow\mathbb Q_p\) be the
112 coefficient inclusion, applied entrywise to points and matrices. Assume
113 only that \[
114 \iota(D_YF(a))\in\operatorname{GL}_e(\mathbb Q_p).
115 \] The theorem
116 \mcode{PolynomialRegularityIntegral.exists_analytic_integral_implicit}
117 constructs the preceding analytic graph in the ambient spaces
118 \(\mathbb Q_p^k\) and \(\mathbb Q_p^e\). Its root equation evaluates the
119 original integral polynomial coefficients using \(\iota\), and its base
120 derivative is \[
121 -\iota(D_YF(a))^{-1}\,\iota(D_TF(a)).
122 \] The source proves that polynomial evaluation, formal partial
123 differentiation and both Jacobian blocks commute with this inclusion. No
124 invertibility modulo \(p\) or integral inverse is required. This permits
125 a solved Jacobian that is singular modulo \(p\) while remaining
126 invertible over \(\mathbb Q_p\). The new specialization is an
127 ambient-field theorem; it does not treat \(\mathbb Z_p\) as a vector
128 space over \(\mathbb Q_p\) or assert a new explicit integral radius.
129 
130 \begin{longtable}[]{@{}
131   >{\raggedright\arraybackslash}p{(\columnwidth - 2\tabcolsep) * \real{0.5000}}
132   >{\raggedright\arraybackslash}p{(\columnwidth - 2\tabcolsep) * \real{0.5000}}@{}}
133 \toprule\noalign{}
134 \begin{minipage}[b]{\linewidth}\raggedright
135 Source module
136 \end{minipage} & \begin{minipage}[b]{\linewidth}\raggedright
137 Mathematical role
138 \end{minipage} \\
139 \midrule\noalign{}
140 \endhead
141 \bottomrule\noalign{}
142 \endlastfoot
143 \mcode{PolynomialAnalyticEvaluation.lean} & Actual polynomial
144 analyticity and strict derivative equals the evaluated formal
145 Jacobian. \\
146 \mcode{PolynomialAnalyticInverse.lean} & Analyticity of the same local
147 inverse supplied by an invertible strict derivative. \\
148 \mcode{PolynomialAnalyticBlocks.lean} & Explicit augmented derivative
149 equivalence and its solved-coordinate restriction. \\
150 \mcode{PolynomialAnalyticImplicit.lean} & Open local root graph,
151 analyticity, base strict derivative and differentiability. \\
152 \mcode{PolynomialAnalyticSelection.lean} & Transfer to continuous root
153 selections, including the per-point open-set theorem. \\
154 \mcode{PolynomialRegularityIntegral.lean} & Integral coefficients and
155 centers included in the ambient p-adic field, with actual Jacobian
156 compatibility. \\
157 \end{longtable}
158 
159 This block closes the local analytic regularity obligation stated in
160 \mcode{TARGET_CONTRACT.json}. It supplies no new uniform numerical
161 radius. The previous weighted lifting and joint deformation results
162 retain their own explicit radii and error estimates. It does not
163 establish a global analytic branch or a result at a point whose solved
164 Jacobian is singular over the fraction field. The proof uses established
165 analytic inverse machinery and makes no novelty claim for the general
166 implicit-function theorem.
167 
168 The remaining Paper IX work includes general singular persistence with
169 higher obstructions, native presentation invariance (13.2), global or
170 completed compatibility and descent (13.3), the outstanding sharper
171 arithmetic statements, and manuscript consolidation. None of those is
172 closed by this local regularity theorem. Release-level checks and audit
173 counts are recorded in the separate release verification and audit
174 files.

Back to source controls

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