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

Back to source controls

Back to Realization Calculus