zeros_isolated_of_holomorphic
plain-language theorem explainer
Zeros of a non-constant holomorphic function on a connected open set in the complex plane are isolated. Number theorists formalizing the Riemann Hypothesis via Pick spectral gap persistence cite this to ensure zeros of the zeta function and related operators cannot accumulate inside the critical strip. The proof first converts differentiability on an open set to analyticity at the zero, then splits on the isolated zeros principle and invokes the identity theorem on the preconnected domain to rule out the identically zero case.
Claim. Let $f : U → ℂ$ be differentiable on an open preconnected set $U ⊆ ℂ$ that is not identically zero. If $f(ρ) = 0$ for some $ρ ∈ U$, then $f(s) ≠ 0$ for all $s$ in some punctured neighborhood of $ρ$ inside $U$.
background
The module formalizes the Riemann Hypothesis as a Pick spectral gap persistence problem for the zeta function in operator theory. It proves several supporting statements including positivity of the gap in the Euler region, the Schur pinch excluding zeros, and the implication from gap persistence to RH. The local setting treats the zeta function and auxiliary holomorphic maps on domains in the complex plane, with the J-cost and phi-ladder machinery from the broader Recognition Science framework supplying the underlying constants and forcing chain.
proof idea
The term proof first obtains AnalyticAt ℂ f ρ from DifferentiableOn.analyticAt applied to the open neighborhood of ρ. It then cases on AnalyticAt.eventually_eq_zero_or_eventually_ne_zero. The identically-zero branch produces an exfalso by constructing AnalyticOnNhd, applying eqOn_zero_of_preconnected_of_eventuallyEq_zero to reach f ≡ 0 on U, and contradicting the supplied non-vanishing point. The remaining branch directly yields the required eventual non-vanishing in the punctured neighborhood.
why it matters
This lemma supplies the isolated-zeros fact required by the module's main results, including pick_gap_persistence_implies_RH and zero_distance_lower_bound. It closes the complex-analytic prerequisite that lets the Pick operator analysis proceed without zero accumulation, consistent with the Recognition Science reduction of RH to spectral-gap persistence on the phi-ladder. The result touches no open scaffolding; it is a fully proved helper that feeds the chain from T5 J-uniqueness through the Euler-product region to the final RH implication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.