zero_in_critical_strip
plain-language theorem explainer
Any non-trivial zero ρ of the completed Riemann zeta function ξ satisfies 0 < Re(ρ) < 1. Number theorists studying zero distributions or the Riemann Hypothesis would cite this as a standard preliminary constraint. The tactic proof proceeds by contradiction in each direction, mapping candidate zeros outside the strip to the known zero-free region Re ≥ 1 via the functional equation ξ(s) = ξ(1-s).
Claim. If the completed Riemann zeta function ξ vanishes at a complex number ρ with Im(ρ) ≠ 0, then 0 < Re(ρ) < 1.
background
The completed Riemann zeta function ξ (here completedRiemannZeta) is the standard completion of the Riemann zeta function satisfying the functional equation ξ(s) = ξ(1-s). The critical strip refers to the open vertical band 0 < Re(s) < 1 in the complex plane. Non-trivial zeros are those with non-zero imaginary part, excluding the trivial zeros at negative even integers.
proof idea
The tactic proof uses constructor to split the conjunction. For the lower bound, assume Re(ρ) ≤ 0 by contradiction, set s := 1 - ρ, verify Re(s) ≥ 1 and s ≠ 1 (via Im(ρ) ≠ 0), apply the functional equation completedRiemannZeta_one_sub to obtain ξ(s) = 0, then contradict the zero-free lemma completedRiemannZeta_ne_zero_of_re_ge_one. The upper bound assumes Re(ρ) ≥ 1, excludes ρ = 1 similarly, and applies the same zero-free lemma directly.
why it matters
This lemma is a prerequisite for the RH_Statement in the same module, which asserts that non-trivial zeros satisfy Re(ρ) = 1/2. It combines the functional equation with the classical zero-free region Re(s) ≥ 1 (except s=1) to confine zeros to the critical strip. In the Recognition Science monolith it ports a classical number-theoretic fact that may later interface with spectral emergence or phi-ladder structures, though no direct downstream use is recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.