Simple-Zero No-Bifurcation

Abstract

Completed reflection keeps a simple critical-line zero on the line, so an off-line birth requires a multiple zero.

Theorem 1.1 (A simple reflected zero has no off-line bifurcation).

$$\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 \Re (s_0)=criticalAbscissa)\Rightarrow \mathrm{EventuallyAt}(tau,s,\mathrm{nhds}(ta{u}_0,s_0),F(tau,s)=0\Rightarrow \Re (s)=criticalAbscissa))\wedge \\ ((\Re (s_0)=criticalAbscissa\wedge \exists tau:\mathbb{N}\to \mathbb{R},s:\mathbb{N}\to \mathbb{C},\mathrm{Tendsto}(tau,\mathrm{atTop}(\mathbb{N}),\mathrm{nhds}(ta{u}_0))\wedge \mathrm{Tendsto}(s,\mathrm{atTop}(\mathbb{N}),\mathrm{nhds}(s_0))\wedge \\ \forall n\in \mathbb{N},F(ta{u}_n,s_n)=0\wedge \Re (s_n)\ne criticalAbscissa)\Rightarrow F(ta{u}_0,s_0)=0\wedge {\mathrm{d}}_{\mathrm{s}}(ta{u}_0,s_0)=0). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The family parameter is real and the zero coordinate is complex. The public assumptions retain completed reflection, both local partial derivatives, and continuity of their real-linear fields.

At a simple critical-line zero, the bivariate implicit-function theorem constructs a unique local zero branch. Reflecting that branch gives another nearby zero branch, so uniqueness makes every nearby zero reflection-fixed and hence critical-line valued.

The second public conjunct considers convergent sequences of off-line zeros. Joint continuity supplies the limiting zero; if its complex derivative were nonzero, the first conjunct would put the sequence on the critical line eventually, a contradiction.

Repository search found no exact frozen owner. The construction imports the canonical reflection ledger and directly applies Mathlib’s bivariate implicit-function theorem and complex-to-real derivative.

References

• Truth anchor: D5/S3/Zeros/Symmetry/SimpleZeroNoBifurcation.simple_zero_no_bifurcation
• Dependency: D5/S3/Weil/ReflectionLedger