B.11. Paper IX: analytic regularity of the local parameter solution

Author: Komorebi P.

This block establishes both analyticity and differentiability of the actual local polynomial solution map at a root with an invertible solved Jacobian. The statements apply to every prime, including \(p=2\). They also hold over any complete nontrivially normed field.

Let \(\mathbb K\) be such a field, let \(e,k\in\mathbb N\), and let

Evaluation of \(F\) means coordinatewise evaluation of its actual polynomials. Define the actual derivative blocks

where each matrix entry is the corresponding formal partial derivative evaluated at \(a\). The hypotheses are exactly

Neither analyticity of a proposed solution nor a derivative formula is assumed.

Local analytic graph theorem. There exist a map

and open sets \(U\subseteq\mathbb K^k\), \(V\subseteq\mathbb K^e\) such that

The map is analytic at every point of \(U\), and its graph describes all roots in the product neighborhood:

At the base parameter it has the strict Fréchet derivative

Consequently it is differentiable on \(U\). The map is defined on the ambient parameter space, but its root, analyticity and uniqueness conclusions are restricted to the specified neighborhood. Uniqueness is among solved coordinates in \(V\).

The main Lean theorem is Komorebi.PolynomialAnalyticImplicit.exists_analytic_implicit. The matrix in its HasStrictFDerivAt conclusion is the continuous linear map represented by the displayed matrix. differentiableOn_of_analytic_graph records the differentiability consequence.

Proof chain. The scalar polynomial derivative bridge is proved by induction on actual multivariate polynomials: constants, sums, and multiplication by a variable. For a scalar polynomial \(P\), its strict derivative is

Assembling the coordinates gives the strict derivative of the evaluated system as its actual Jacobian matrix. Polynomial analyticity is supplied by the pinned Mathlib theorem for multivariate polynomial evaluation, followed by finite coordinate assembly.

Consider the actual augmented polynomial map

Its derivative and inverse derivative at \(a\) are

The proof constructs the continuous linear equivalence from these explicit matrices and verifies both inverse identities. The strict inverse theorem gives a local inverse \(g\) of \(\Phi\), and the analytic inverse result shows that this same inverse is analytic near \(\Phi(a)=(0,t_0)\). Set

The two inverse identities and a sufficiently small product neighborhood give the exact local graph statement. Composing the derivative of \(g\) with parameter insertion and solved-coordinate projection yields \(-J^{-1}K\). The chosen parameter neighborhood is also restricted so that the inverse identities, analyticity and inclusion \(\psi(U)\subseteq V\) hold there simultaneously.

Transfer to a supplied continuous solution. Suppose \(g:\mathbb K^k\to\mathbb K^e\) is continuous at \(t_0\), \(g(t_0)=y_0\), and

for all \(t\) in some neighborhood of \(t_0\). Under the same invertibility hypothesis at \(a\), continuity places \(g(t)\) in the uniqueness neighborhood \(V\) for all sufficiently close parameters. Hence \(g\) and \(\psi\) agree on a neighborhood of \(t_0\). The theorem continuous_selection_regularity transfers both analyticity and the strict derivative formula to \(g\).

There is also an explicit open-set version. Let \(U\) be open, let \(g\) be continuous on \(U\), and suppose for every \(t\in U\) that

Writing \(K_t=D_TF(g(t),t)\), the theorem continuous_selection_analyticOnNhd proves

with a strict Fréchet derivative at each point. The per-point invertibility hypothesis is part of this theorem. This is a transfer statement for continuous local root selections satisfying its hypotheses; it does not assert equality of arbitrary global branch choices.

Integral p-adic specialization. For any prime \(p\), let

Let \(\iota:\mathbb Z_p\hookrightarrow\mathbb Q_p\) be the coefficient inclusion, applied entrywise to points and matrices. Assume only that

The theorem PolynomialRegularityIntegral.exists_analytic_integral_implicit constructs the preceding analytic graph in the ambient spaces \(\mathbb Q_p^k\) and \(\mathbb Q_p^e\). Its root equation evaluates the original integral polynomial coefficients using \(\iota\), and its base derivative is

The source proves that polynomial evaluation, formal partial differentiation and both Jacobian blocks commute with this inclusion. No invertibility modulo \(p\) or integral inverse is required. This permits a solved Jacobian that is singular modulo \(p\) while remaining invertible over \(\mathbb Q_p\). The new specialization is an ambient-field theorem; it does not treat \(\mathbb Z_p\) as a vector space over \(\mathbb Q_p\) or assert a new explicit integral radius.

Permalink · Source line 5

This block closes the local analytic regularity obligation stated in TARGET_CONTRACT.json. It supplies no new uniform numerical radius. The previous weighted lifting and joint deformation results retain their own explicit radii and error estimates. It does not establish a global analytic branch or a result at a point whose solved Jacobian is singular over the fraction field. The proof uses established analytic inverse machinery and makes no novelty claim for the general implicit-function theorem.

The remaining Paper IX work includes general singular persistence with higher obstructions, native presentation invariance (13.2), global or completed compatibility and descent (13.3), the outstanding sharper arithmetic statements, and manuscript consolidation. None of those is closed by this local regularity theorem. Release-level checks and audit counts are recorded in the separate release verification and audit files.

Permalink · Source line 159