PickGapPersistence
plain-language theorem explainer
PickGapPersistence defines the property that a map J from complex numbers to complex numbers maintains a uniform positive lower bound on the Pick gap whenever the real part exceeds any vertical line Re(s) = σ₀ > 1/2, with the witness point also satisfying Re J > 0. Analysts reformulating the Riemann Hypothesis in terms of spectral margins for the zeta function cite this definition when reducing zero-free regions to gap persistence. The definition is expressed as a direct existential statement over a minimal gap size δ_min together with a quant-
Claim. Let $J : ℂ → ℂ$. The map $J$ satisfies Pick gap persistence if there exists $δ_{min} > 0$ such that for every real $σ_0 > 1/2$ there is a point $s_0$ with Re$(s_0) > σ_0$, Re$(J(s_0)) > 0$, and $1 - ‖θ(J(s_0))‖ ≥ δ_{min}$, where the Pick gap is the quantity $1 - ‖θ(J_val)‖$.
background
The Pick gap at a point is defined as 1 minus the norm of theta applied to the J value, supplying the margin by which |Ξ| < 1. This module recasts the Riemann Hypothesis as a Pick spectral gap persistence problem in classical operator theory applied to the zeta function, with the J-field serving as the central object. The upstream sibling pick_gap supplies the concrete expression 1 - ‖theta J_val‖ and the companion result pick_gap_pos_of_re_pos shows that Re J > 0 forces the gap itself to be positive.
proof idea
As a definition the body directly encodes the required persistence by asserting existence of a uniform δ_min > 0 and then, for each σ₀ > 1/2, a witness s₀ obeying Re s₀ > σ₀, Re(J s₀) > 0 and pick_gap(J s₀) ≥ δ_min. No lemmas are applied; the statement is the literal translation of the property into quantifiers over the real line and the complex plane.
why it matters
The definition supplies the hypothesis for the downstream theorem pick_gap_persistence_implies_RH, which concludes that gap persistence forces the Riemann Hypothesis, and it is also invoked by RH_reduces_to_euler_product_at_three_halves to reduce the problem to a computable constant. It occupies the central position in the module's chain that converts spectral-gap persistence into a zero-free statement for the zeta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.