zero_distance_lower_bound
plain-language theorem explainer
The theorem shows that for chart center real part σ₀ > 1/2 and any β ≤ 1 the quantity σ₀ + 1 - β is at least 1/2. Analysts working on the Riemann Hypothesis through Pick spectral gap persistence cite the bound to keep zeros outside a forbidden neighborhood of the chart center. The argument is a direct linear-arithmetic reduction of the two input inequalities.
Claim. Let σ₀ ∈ ℝ satisfy σ₀ > 1/2 and let β ∈ ℝ satisfy β ≤ 1. Then σ₀ + 1 - β ≥ 1/2.
background
The PickGapPersistence module recasts the Riemann Hypothesis as persistence of a spectral gap under the Pick operator applied to the zeta function. The chart center σ₀ > 1/2 lies in the Euler region where the real part of J is positive, and β supplies an upper bound on the real part of candidate zeros. The module already establishes that positive real part of J forces a positive Pick gap and that the gap remains positive throughout the Euler region.
proof idea
The proof is a one-line wrapper that invokes the linarith tactic on the hypotheses 1/2 < σ₀ and β ≤ 1.
why it matters
The bound appears among the fully proved results that support pick_gap_persistence_implies_RH. It guarantees that no zero can lie closer than distance 1/2 to the chart center, closing the geometric control needed for the persistence argument to imply the Riemann Hypothesis. The result therefore sits at the interface between the operator-theoretic reformulation and the classical zero-free region.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.