CriticalStripZeroFree
plain-language theorem explainer
The CriticalStripZeroFree structure packages the assertion that the Riemann zeta function has no zeros for complex s with 1/2 < Re(s) < 1. Number theorists closing the RS-native zeta program in Phase 5 would cite it as the named target property required for RH-quality results. The declaration is a bare structure definition with no proof body or attached lemmas.
Claim. Let $s$ be a complex number. The critical-strip zero-free property is the statement that the Riemann zeta function satisfies $s.re > 1/2$ and $s.re < 1$ implies $zeta(s) neq 0$.
background
The module StripZeroFreeRegion forms Phase 5 of the RS-native zeta program. It records the already-proven zero-free result for Re(s) >= 1 from Mathlib and isolates the open strip statement required for full RH-quality closure. The structure CriticalStripZeroFree packages the strip statement as a named target rather than an asserted theorem.
proof idea
The declaration is a structure definition with an empty proof body. It simply introduces the field zero_free as the universal quantification over the open critical strip.
why it matters
This definition supplies the target for CriticalStripZeroFreeBridge, which states that the nonempty existence of such a witness follows from Mathlib's RiemannHypothesis. It advances the RS zeta program by isolating the strip zero-free step needed before invoking the Recognition Composition Law or phi-ladder constructions. The open question remains whether the full strip statement can be derived internally from the J-uniqueness and eight-tick octave without external input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.