Critical-Zero Transverse Gap

Abstract

A critical-line zero has a transverse gap whose order is twice its multiplicity.

Theorem 1.1 (The transverse gap at a critical zero).

$$\begin{gathered} \forall r:\mathbb{N},t_0:\mathbb{R}, \\ 0<r\wedge (\forall j:\mathbb{N},j<r\Rightarrow \mathrm{iteratedDeriv}\left(j,criticalXi,t_0\right)=0)\wedge \mathrm{iteratedDeriv}\left(r,criticalXi,t_0\right)\ne 0\Rightarrow \begin{array}{c}(\forall m:\mathbb{N},m<r\Rightarrow \mathrm{normalJet}\left(t_0,m\right)=0)\wedge \\ \mathrm{normalJet}\left(t_0,r\right)={\frac{\mathrm{iteratedDeriv}\left(r,criticalXi,t_0\right)}{\mathrm{factorial}\left(r\right)}}^2\wedge \\ 0<\mathrm{normalJet}\left(t_0,r\right)\wedge \\ \mathrm{IsBigOAtZero}\left((delta\mapsto \mathrm{normalIntensity}\left(delta,t_0\right)-{\frac{\mathrm{iteratedDeriv}\left(r,criticalXi,t_0\right)}{\mathrm{factorial}\left(r\right)}}^2\cdot delt{a}^{2r}),(delta\mapsto delt{a}^{2r+2})\right)\wedge \\ (r=1\Rightarrow \mathrm{IsBigOAtZero}\left((delta\mapsto \mathrm{normalIntensity}\left(delta,t_0\right)-\mathrm{iteratedDeriv}{\left(1,criticalXi,t_0\right)}^2\cdot delt{a}^2),(delta\mapsto delt{a}^4)\right))\end{array}. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Zeros/CriticalZeroTransverseGap.critical_zero_transverse_gap (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let t0 be a zero of the canonical critical-line completed-xi reading with positive multiplicity r: all derivatives below r vanish and the derivative of order r is nonzero. Every normal jet below r then vanishes, while the depth-r jet is the strictly positive square of the leading Taylor coefficient.

The two final public conjuncts concern the actual norm-squared normal intensity. Its leading transverse term has degree 2r with remainder of order 2r+2; at a simple zero this becomes the squared first derivative times the displacement squared, with quartic remainder.

The proof imports the canonical normal-jet convolution formula. It also uses conjugate reflection to prove evenness of the actual intensity and applies the pinned Taylor remainder theorem to that smooth function.

References

• Truth anchor: D5/S3/Zeros/CriticalZeroTransverseGap.critical_zero_transverse_gap
• Dependency: D5/S3/Zeros/NormalJetFormula