euler_product_positive_real
plain-language theorem explainer
For real σ greater than 1 the recognition cost J(σ) is positive, anchoring the Euler product region in the Pick gap analysis of the zeta function. Analysts working on spectral persistence for the Riemann hypothesis cite this to secure the classical half-plane before extending to complex values. The proof is a direct term construction that exhibits (σ-1)/σ as the positive witness and verifies the inequality via chained real-number facts.
Claim. For every real number $σ > 1$ there exists a real number $J(σ) > 0$.
background
The PickGapPersistence module recasts the Riemann hypothesis as persistence of a spectral gap under the Pick operator applied to the zeta function. The J-function is the recognition cost from the foundational forcing chain, satisfying J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and reducing to (x + x^{-1})/2 - 1 on the positive reals. The Euler product region is the half-plane Re(s) > 1 where the zeta function equals the convergent product over primes.
proof idea
The proof is a term-mode construction supplying the explicit witness (σ - 1)/σ. It first obtains 0 < σ by applying lt_trans to zero_lt_one and the hypothesis 1 < σ, then invokes div_pos on the resulting positive numerator and denominator.
why it matters
This result is invoked directly by pick_gap_euler_region, which itself feeds pick_gap_persistence_implies_RH. It closes the real-line positivity step required before the Schur pinch and gap-persistence argument can imply the Riemann hypothesis, consistent with the Euler-product positivity in the T5-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.