pick_gap_persistence_implies_RH
plain-language theorem explainer
Pick gap persistence for a complex field J implies the Riemann hypothesis in operator form by guaranteeing a uniform positive lower bound on the spectral gap that forces the theta norm strictly below 1 for points with real part exceeding any σ₀ > 1/2. Number theorists working on spectral-gap reformulations of RH would cite this implication as the closing link in the module chain. The proof is a direct term extraction from the persistence hypothesis combined with simplification of the gap definition and a norm non-negativity argument.
Claim. If the map $J : ℂ → ℂ$ satisfies the Pick Gap Persistence property (there exists δ_min > 0 such that for every real σ₀ > 1/2 there exists s₀ with Re(s₀) > σ₀, Re(J(s₀)) > 0, and pick_gap(J(s₀)) ≥ δ_min), then there exists δ > 0 such that for every real σ₀ > 1/2 there exists s ∈ ℂ with Re(s) > σ₀ and ‖θ(J(s))‖ < 1.
background
The module formalizes the Riemann Hypothesis as a Pick spectral gap persistence problem in classical operator theory applied to the Riemann zeta function. The central definition PickGapPersistence asserts the existence of a positive minimal gap δ_min together with a positive real-part condition on J(s₀) for every σ₀ > 1/2, ensuring the Pick gap remains bounded away from zero in the right half-plane. This theorem appears among the fully proved main results listed in the module documentation, alongside pick_gap_pos_of_re_pos, euler_product_positive_real, and schur_pinch.
proof idea
The proof is a term-mode extraction. It obtains the triple (δ_min, positivity, persistence witness) from the hypothesis, refines the outer existential over δ, then applies the witness to each σ₀ > 1/2 to produce s₀. It simplifies the gap inequality via the pick_gap definition and finishes with linarith using non-negativity of the theta norm to obtain the strict bound less than 1.
why it matters
This declaration supplies the direct implication from Pick Gap Persistence to the Riemann Hypothesis, completing the list of main results in the module documentation. It thereby closes the operator-theoretic reformulation of RH inside the Recognition Science number-theory development. No downstream uses are recorded and no open questions are addressed; the result stands fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.