criticalStrip_zero_free_of_riemannHypothesis
plain-language theorem explainer
Mathlib's RiemannHypothesis implies the Riemann zeta function has no zeros in the open strip between real parts one half and one. Number theorists bridging analytic number theory to Recognition Science would cite this as the direct translation of the hypothesis into a zero-free region. The proof proceeds by contradiction, ruling out the pole at one and trivial zeros, applying the hypothesis to force real part exactly one half, then obtaining a linear arithmetic contradiction.
Claim. Assuming the Riemann hypothesis (every nontrivial non-pole zero lies on the critical line), the Riemann zeta function satisfies $riemannZeta(s) ≠ 0$ for all complex $s$ with $1/2 < Re(s) < 1$.
background
The module StripZeroFreeRegion forms Phase 5 of the RS-native zeta program. It records the already-proven zero-free result on the half-plane Re(s) ≥ 1 and packages the missing critical-strip statement as a bridge object. The local setting treats the Riemann zeta function via its functional equation and theta-function representation imported from ZetaFromTheta. The upstream result supplies a classical bridge structure that records defect and energy meanings for traceability, though the present theorem relies only on the Mathlib definition of RiemannHypothesis.
proof idea
The tactic proof assumes a zero s in the open strip and proceeds by contradiction. It first excludes s = 1 by showing the real part would equal 1, violating the strict inequalities. It next excludes the trivial zeros at negative even integers by deriving a negative real part. The hypothesis is then applied directly to conclude that the real part equals exactly 1/2, after which linarith produces the contradiction.
why it matters
This theorem supplies the zero-free property inside the bridge object criticalStripZeroFreeBridge_of_riemannHypothesis, which in turn feeds the Phase 7 honest state of the Recognition Science zeta program. It directly implements the DOC_COMMENT claim that Mathlib's RiemannHypothesis yields the open right half-strip zero-free. The result touches the open question of whether the full Riemann hypothesis can be established inside the Recognition framework rather than imported from Mathlib.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.