Rouche Zero-Count Stability

Abstract

A strict boundary perturbation preserves the rectangle zero count with analytic multiplicity.

Theorem 1.1 (The straight-line homotopy is nonvanishing on the boundary).

$$\forall f\in \mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right),g\in \mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right),z\in \mathrm{Complex}\left(\right),w\in \mathrm{Complex}\left(\right),\left(\forall s\in \mathrm{Complex}\left(\right),s\in \mathrm{RectangleBorder}\left(z,w\right)\Rightarrow \Vert f\left(s\right)-g\left(s\right)\Vert <\Vert g\left(s\right)\Vert \right)\Rightarrow \left(\forall t\in \mathrm{Real}\left(\right),t\in \mathrm{Icc}\left(0,1\right)\Rightarrow \left(\forall s\in \mathrm{Complex}\left(\right),s\in \mathrm{RectangleBorder}\left(z,w\right)\Rightarrow g\left(s\right)+\mathrm{ofReal}\left(t\right)\cdot \left(f\left(s\right)-g\left(s\right)\right)\ne 0\right)\right)$$

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

Source. Repository-derived.

Commentary.

The strict boundary estimate and the interval bound on the homotopy parameter force the perturbation term to have norm strictly below the base value, so their sum cannot vanish.

Theorem 1.2 (The normalized logarithmic-derivative contour integral is continuous).

$$\forall f\in \mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right),g\in \mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right),z\in \mathrm{Complex}\left(\right),w\in \mathrm{Complex}\left(\right),\left(\mathrm{re}\left(z\right)<\mathrm{re}\left(w\right)\wedge \left(\mathrm{im}\left(z\right)<\mathrm{im}\left(w\right)\wedge \left(\mathrm{AnalyticOnNhd}\left(\mathrm{Complex}\left(\right),f,\mathrm{Rectangle}\left(z,w\right)\right)\wedge \left(\mathrm{AnalyticOnNhd}\left(\mathrm{Complex}\left(\right),g,\mathrm{Rectangle}\left(z,w\right)\right)\wedge \left(\forall s\in \mathrm{Complex}\left(\right),s\in \mathrm{RectangleBorder}\left(z,w\right)\Rightarrow \Vert f\left(s\right)-g\left(s\right)\Vert <\Vert g\left(s\right)\Vert \right)\right)\right)\right)\right)\Rightarrow \mathrm{ContinuousOn}\left((t:\mathrm{Real}\left(\right)\mapsto {\mathrm{RectangleIntegral}}^{\prime }\left((s:\mathrm{Complex}\left(\right)\mapsto \mathrm{logDeriv}\left((u:\mathrm{Complex}\left(\right)\mapsto g\left(u\right)+\mathrm{ofReal}\left(t\right)\cdot \left(f\left(u\right)-g\left(u\right)\right)),s\right)),z,w\right)),\mathrm{Icc}\left(0,1\right)\right)$$

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

Source. Repository-derived.

Commentary.

Projection to the closed parameter interval extends the boundary integrand continuously. Mathlib’s parametric interval-integral continuity theorem applies to each of the four rectangle sides, and the normalized contour combination remains continuous.

Theorem 1.3 (Rectangle Rouche zero-count stability).

$$\forall f\in \mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right),g\in \mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right),z\in \mathrm{Complex}\left(\right),w\in \mathrm{Complex}\left(\right),Zf\in \mathrm{Finset}\left(\mathrm{Complex}\left(\right)\right),Zg\in \mathrm{Finset}\left(\mathrm{Complex}\left(\right)\right),\left(\left(\mathrm{re}\left(z\right)<\mathrm{re}\left(w\right)\wedge \left(\mathrm{im}\left(z\right)<\mathrm{im}\left(w\right)\wedge \left(\mathrm{AnalyticOnNhd}\left(\mathrm{Complex}\left(\right),f,\mathrm{Rectangle}\left(z,w\right)\right)\wedge \left(\mathrm{AnalyticOnNhd}\left(\mathrm{Complex}\left(\right),g,\mathrm{Rectangle}\left(z,w\right)\right)\wedge \left(\forall s\in \mathrm{Complex}\left(\right),s\in \mathrm{RectangleBorder}\left(z,w\right)\Rightarrow \Vert f\left(s\right)-g\left(s\right)\Vert <\Vert g\left(s\right)\Vert \right)\right)\right)\right)\right)\wedge \left(\left(\forall s\in \mathrm{Complex}\left(\right),s\in \mathrm{Rectangle}\left(z,w\right)\Rightarrow \left(f\left(s\right)=0\iff s\in Zf\right)\right)\wedge \left(\mathrm{toSet}\left(Zf\right)\subseteq \mathrm{Rectangle}\left(z,w\right)\wedge \left(\left(\forall s\in \mathrm{Complex}\left(\right),s\in \mathrm{Rectangle}\left(z,w\right)\Rightarrow \left(g\left(s\right)=0\iff s\in Zg\right)\right)\wedge \mathrm{toSet}\left(Zg\right)\subseteq \mathrm{Rectangle}\left(z,w\right)\right)\right)\right)\right)\Rightarrow \sum _{rho\in Zf}\mathrm{analyticOrderNatAt}\left(f,rho\right)=\sum _{rho\in Zg}\mathrm{analyticOrderNatAt}\left(g,rho\right)$$

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

Source. Repository-derived.

Commentary.

Boundary nonvanishing and contour-integral continuity put the normalized logarithmic-derivative integral in the discrete range of integer casts throughout the connected parameter interval. It is therefore constant, and the rectangle argument principle identifies its two endpoint values with the stated multiplicity sums.

References

• Truth anchor: D5/S3/Weil/ZetaAnalytic/RoucheZeroCount.continuousOn_rectangleIntegral_logDeriv_straightLine
• Truth anchor: D5/S3/Weil/ZetaAnalytic/RoucheZeroCount.homotopy_nonvanishing_on_rectangleBorder
• Truth anchor: D5/S3/Weil/ZetaAnalytic/RoucheZeroCount.rectangle_zero_count_eq_of_norm_sub_lt