Symmetric Simple Zero Fixed Axis

Abstract

A symmetric simple zero has a public unique local continuation fixed by completed reflection.

Theorem 1.1 (A symmetric simple zero remains reflection-fixed).

$$\begin{gathered} \forall F:\mathbb{R}\to \mathbb{C}\to \mathbb{C},d_{tau}:\mathbb{R}\to \mathbb{C}\to \mathrm{ContinuousLinearMap}(\mathbb{R},\mathbb{R},\mathbb{C}),d_s:\mathbb{R}\to \mathbb{C}\to \mathbb{C}, \\ ta{u}_0\in \mathbb{R},s_0\in \mathbb{C},(\forall tau\in \mathbb{R},s\in \mathbb{C},F(tau,\mathrm{mirror}(s))=\overline{F(tau,s)})\wedge \\ \mathrm{EventuallyAt}(tau,s,\mathrm{nhds}(ta{u}_0,s_0),\mathrm{HasFDerivAt}(\mathrm{timeSlice}(F,s),{\mathrm{d}}_{\mathrm{tau}}(tau,s),tau))\wedge \mathrm{EventuallyAt}(tau,s,\mathrm{nhds}(ta{u}_0,s_0),\mathrm{HasDerivAt}(\mathrm{spaceSlice}(F,tau),{\mathrm{d}}_{\mathrm{s}}(tau,s),s))\wedge \\ \mathrm{ContinuousAt}(tau,s\mapsto {\mathrm{d}}_{\mathrm{tau}}(tau,s),ta{u}_0,s_0)\wedge \mathrm{ContinuousAt}(tau,s\mapsto {\mathrm{d}}_{\mathrm{s}}(tau,s)\mathrm{smul}(\mathrm{id}(\mathbb{C})),ta{u}_0,s_0)\Rightarrow \\ (F(ta{u}_0,s_0)=0\wedge {\mathrm{d}}_{\mathrm{s}}(ta{u}_0,s_0)\ne 0\wedge \mathrm{mirror}(s_0)=s_0)\Rightarrow \\ \exists delta:\mathbb{R},0<delta\wedge \\ \exists epsilon:\mathbb{R},0<epsilon\wedge \\ \exists rho:\mathbb{R}\to \mathbb{C}, \\ \mathrm{rho}(ta{u}_0)=s_0\wedge \mathrm{ContinuousAt}(rho,ta{u}_0)\wedge \\ (\forall kappa:\mathbb{R},\left|kappa-ta{u}_0\right|<delta\Rightarrow \mathrm{rho}(kappa)\in \mathrm{ball}(s_0,epsilon))\wedge \\ (\forall kappa:\mathbb{R},\left|kappa-ta{u}_0\right|<delta\Rightarrow F(kappa,\mathrm{rho}(kappa))=0)\wedge \\ (\forall kappa:\mathbb{R},\left|kappa-ta{u}_0\right|<delta\Rightarrow \forall s:\mathbb{C},s\in \mathrm{ball}(s_0,epsilon)\Rightarrow F(kappa,s)=0\Rightarrow s=\mathrm{rho}(kappa))\wedge \\ (\forall kappa:\mathbb{R},\left|kappa-ta{u}_0\right|<delta\Rightarrow \mathrm{mirror}(\mathrm{rho}(kappa))=\mathrm{rho}(kappa))\wedge \\ (\forall kappa:\mathbb{R},\left|kappa-ta{u}_0\right|<delta\Rightarrow \Re (\mathrm{rho}(kappa))=criticalAbscissa). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Zeros/Symmetry/SymmetricSimpleZeroFixedAxis.symmetric_simple_zero_fixed_axis (✓ std3). ∎

Source. Repository-derived.

Commentary.

The statement exposes positive parameter and zero radii together with the implicit-function continuation through the base zero.

The continuation is continuous at the base parameter, is the unique zero in the displayed ball, and remains fixed by completed reflection on the whole displayed parameter interval.

References

• Truth anchor: D5/S3/Zeros/Symmetry/SymmetricSimpleZeroFixedAxis.symmetric_simple_zero_fixed_axis
• Dependency: D5/S3/Zeros/Symmetry/SimpleZeroNoBifurcation