pick_gap_euler_region
plain-language theorem explainer
The theorem asserts that for any real σ₀ greater than 1 the Pick spectral gap of the Riemann zeta function is positive inside the Euler product region. Analytic number theorists pursuing operator-theoretic reformulations of the Riemann Hypothesis cite this step when building gap persistence outside the critical strip. The proof is a direct term-mode extraction that pulls the positivity of the real J-cost from the Euler product lemma and feeds it into the implication from positive real part to positive gap.
Claim. For any real number $σ_0 > 1$, there exists a positive real number $δ > 0$ such that the Pick spectral gap of the Riemann zeta function is positive throughout the Euler product region.
background
The module recasts the Riemann Hypothesis as a Pick spectral gap persistence question in operator theory applied to the zeta function. The J-cost satisfies the Recognition Composition Law (Axiom 2): for positive x, y the identity F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y) holds, which is the multiplicative form of d'Alembert's equation and forces compatibility with the multiplicative structure of the positive reals. The Euler product region is the half-plane Re(s) > 1 where the zeta function equals the product over primes. Upstream lemmas supply the positivity of J on the real line greater than 1 and the direct implication from Re(J) > 0 to a positive Pick gap.
proof idea
The term proof first invokes the euler_product_positive_real lemma on σ₀ > 1 to obtain a real J value together with its positivity witness. It then packages this value as the complex number with zero imaginary part and applies the pick_gap_pos_of_re_pos implication to extract the required positive δ.
why it matters
The result supplies the base case of gap positivity in the Euler region, which is required by the downstream theorem pick_gap_persistence_implies_RH that converts persistence into the Riemann Hypothesis. It therefore closes one link in the chain that begins with the Composition axiom and the PhiForcingDerived J-cost structure and ends with the full equivalence between gap persistence and RH. The step touches the open question of whether the same positivity persists when σ₀ drops below 1 into the critical strip.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.