riemannZeta_ne_zero_re_gt_one
plain-language theorem explainer
The theorem states that the Riemann zeta function has no zeros in the open half-plane where the real part of its argument exceeds one. Number theorists working on zero distributions or the Riemann hypothesis would cite this as the classical strict half-plane result. The proof is a one-line term application of the Mathlib lemma that handles the strict real-part inequality.
Claim. If $1 < {Re}(s)$ for a complex number $s$, then the Riemann zeta function satisfies $zeta(s) neq 0$.
background
This declaration sits inside Phase 5 of the RS-native zeta program. The module records the established zero-free region for the Riemann zeta function on the closed half-plane Re(s) >= 1 and distinguishes it from the deeper strip result still required for Riemann-hypothesis-quality closure. The local setting treats the half-plane statements as already available from Mathlib while packaging the genuine strip theorem as a future bridge object.
proof idea
The proof is a direct term-mode application of the Mathlib lemma riemannZeta_ne_zero_of_one_lt_re to the hypothesis that the real part of s exceeds one.
why it matters
The result supplies the strict half-plane case to the boundaryZeroFreeCert definition, which packages both the closed and open zero-free regions for later strip arguments. It records the classical half-plane fact inside the Recognition Science zeta program before the bridge to the critical-strip zero-free theorem is constructed. The module doc-comment notes that the genuine strip result remains unproved and is left as the next bridge object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.