Countable Rational Flux Criterion

Abstract

Rational rectangles detect every isolated zero in the centered open right half-plane.

Theorem 1.1 (Countable rational flux criterion).

$$\forall flux\in \mathrm{Rat}\left(\right)\to \left(\mathrm{Rat}\left(\right)\to \left(\mathrm{Rat}\left(\right)\to \left(\mathrm{Rat}\left(\right)\to \mathrm{Nat}\left(\right)\right)\right)\right),\left(\left(\forall z\in \mathrm{Complex}\left(\right),\left(centeredXi\left(z\right)=0\wedge \mathrm{re}\left(z\right)>0\right)\Rightarrow \left(\exists x0\in \mathrm{Real}\left(\right),x1\in \mathrm{Real}\left(\right),y0\in \mathrm{Real}\left(\right),y1\in \mathrm{Real}\left(\right),x0>0\wedge \left(x0<\mathrm{re}\left(z\right)\wedge \left(\mathrm{re}\left(z\right)<x1\wedge \left(y0<\mathrm{im}\left(z\right)\wedge \left(\mathrm{im}\left(z\right)<y1\wedge \left(\forall w\in \mathrm{Complex}\left(\right),\left(centeredXi\left(w\right)=0\wedge \mathrm{mem}\left(w,\mathrm{Rectangle}\left(\mathrm{ComplexMk}\left(x0,y0\right),\mathrm{ComplexMk}\left(x1,y1\right)\right)\right)\right)\Rightarrow w=z\right)\right)\right)\right)\right)\right)\right)\wedge \left(\left(\forall a\in \mathrm{Rat}\left(\right),b\in \mathrm{Rat}\left(\right),c\in \mathrm{Rat}\left(\right),d\in \mathrm{Rat}\left(\right),\left(\left(a>0\wedge \left(a<b\wedge c<d\right)\right)\wedge \left(\left(\forall z\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(z,\mathrm{RectangleBorder}\left(\mathrm{ComplexMk}\left(\mathrm{toReal}\left(a\right),\mathrm{toReal}\left(c\right)\right),\mathrm{ComplexMk}\left(\mathrm{toReal}\left(b\right),\mathrm{toReal}\left(d\right)\right)\right)\right)\Rightarrow \left(\neg centeredXi\left(z\right)=0\right)\right)\wedge \left(\forall z\in \mathrm{Complex}\left(\right),centeredXi\left(z\right)=0\Rightarrow \left(\neg \mathrm{mem}\left(z,\mathrm{Rectangle}\left(\mathrm{ComplexMk}\left(\mathrm{toReal}\left(a\right),\mathrm{toReal}\left(c\right)\right),\mathrm{ComplexMk}\left(\mathrm{toReal}\left(b\right),\mathrm{toReal}\left(d\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow flux\left(a,b,c,d\right)=0\right)\wedge \left(\forall z\in \mathrm{Complex}\left(\right),a\in \mathrm{Rat}\left(\right),b\in \mathrm{Rat}\left(\right),c\in \mathrm{Rat}\left(\right),d\in \mathrm{Rat}\left(\right),\left(centeredXi\left(z\right)=0\wedge \left(\left(a>0\wedge \left(a<b\wedge c<d\right)\right)\wedge \left(\mathrm{mem}\left(z,\mathrm{Rectangle}\left(\mathrm{ComplexMk}\left(\mathrm{toReal}\left(a\right),\mathrm{toReal}\left(c\right)\right),\mathrm{ComplexMk}\left(\mathrm{toReal}\left(b\right),\mathrm{toReal}\left(d\right)\right)\right)\right)\wedge \left(\left(\forall w\in \mathrm{Complex}\left(\right),\left(centeredXi\left(w\right)=0\wedge \mathrm{mem}\left(w,\mathrm{Rectangle}\left(\mathrm{ComplexMk}\left(\mathrm{toReal}\left(a\right),\mathrm{toReal}\left(c\right)\right),\mathrm{ComplexMk}\left(\mathrm{toReal}\left(b\right),\mathrm{toReal}\left(d\right)\right)\right)\right)\right)\Rightarrow w=z\right)\wedge \left(\forall z\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(z,\mathrm{RectangleBorder}\left(\mathrm{ComplexMk}\left(\mathrm{toReal}\left(a\right),\mathrm{toReal}\left(c\right)\right),\mathrm{ComplexMk}\left(\mathrm{toReal}\left(b\right),\mathrm{toReal}\left(d\right)\right)\right)\right)\Rightarrow \left(\neg centeredXi\left(z\right)=0\right)\right)\right)\right)\right)\right)\Rightarrow \left(flux\left(a,b,c,d\right)=\mathrm{analyticOrderNatAt}\left(centeredXi,z\right)\wedge 1\le \mathrm{analyticOrderNatAt}\left(centeredXi,z\right)\right)\right)\right)\right)\Rightarrow \left(\left(\forall z\in \mathrm{Complex}\left(\right),centeredXi\left(z\right)=0\Rightarrow \left(\neg \mathrm{re}\left(z\right)>0\right)\right)\iff \left(\forall a\in \mathrm{Rat}\left(\right),b\in \mathrm{Rat}\left(\right),c\in \mathrm{Rat}\left(\right),d\in \mathrm{Rat}\left(\right),\left(\left(a>0\wedge \left(a<b\wedge c<d\right)\right)\wedge \left(\forall z\in \mathrm{Complex}\left(\right),\mathrm{mem}\left(z,\mathrm{RectangleBorder}\left(\mathrm{ComplexMk}\left(\mathrm{toReal}\left(a\right),\mathrm{toReal}\left(c\right)\right),\mathrm{ComplexMk}\left(\mathrm{toReal}\left(b\right),\mathrm{toReal}\left(d\right)\right)\right)\right)\Rightarrow \left(\neg centeredXi\left(z\right)=0\right)\right)\right)\Rightarrow flux\left(a,b,c,d\right)=0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaAnalytic/CountableRationalFluxCriterion.countable_rational_flux_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Axis isolation gives a real rectangle containing only the selected zero. Density of the rationals supplies four rational sides strictly between that zero and the isolating sides. The canonical rectangle boundary then contains no zero, while the selected zero lies in its interior. The public argument-principle law identifies this flux exactly with the positive analytic order of the centered reading F(z) = xi(1/2 + z) at the isolated zero.

References

• Truth anchor: D5/S3/Weil/ZetaAnalytic/CountableRationalFluxCriterion.countable_rational_flux_criterion
• Dependency: D5/S3/Zeros/CompletedZeta