chart_center_in_euler_region
plain-language theorem explainer
The result establishes that any real σ₀ exceeding 1/2 forces the shifted value σ₀ + 1 to exceed 1. Researchers formalizing the Riemann Hypothesis via Pick spectral gap persistence cite it to locate the chart center inside the absolute-convergence region of the Euler product. The argument is a direct linear-arithmetic reduction of the input inequality.
Claim. If $σ_0 ∈ ℝ$ satisfies $σ_0 > 1/2$, then $σ_0 + 1 > 1$.
background
The module recasts the Riemann Hypothesis as a Pick spectral gap persistence question in operator theory on the zeta function. Central claims include positivity of the gap when the real part is positive, gap positivity throughout the Euler region, and the implication that persistent gaps entail the hypothesis. The present statement supplies the elementary placement of the chart center inside that region.
proof idea
One-line wrapper that applies the linarith tactic to the hypothesis σ₀ > 1/2, yielding the target inequality by elementary real arithmetic.
why it matters
The lemma closes the local step required by pick_gap_persistence_implies_RH and zero_distance_lower_bound, as recorded in the module documentation. It ensures the chart center satisfies the Euler-product condition σ₀ + 1 > 1 whenever σ₀ > 1/2, thereby supporting the persistence argument that links the Pick operator gap to the absence of zeros on the critical line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.