IndisputableMonolith.NumberTheory.StripZeroFreeRegion
StripZeroFreeRegion supplies the classical boundary result that the Riemann zeta function has no zeros for Re(s) >= 1. Researchers building unconditional zero-free strips or RH closure arguments cite it as the base case before extending leftward. The module achieves this by importing the weak zero-free region and zeta-from-theta bridges then re-exporting the Mathlib theorem directly.
claim$zeta(s) neq 0$ for every complex number $s$ with $operatorname{Re}(s) geq 1$.
background
The module belongs to the NumberTheory section of the Recognition Science formalization and sits between the weak zero-free region and the classical extension. Upstream, the WeakZeroFreeRegion module poses the question: Can the RH conditional axiom be eliminated or weakened? The RS approach to the Riemann Hypothesis via the defect-budget bridge may make the full RH axiom unnecessary. The ZetaFromTheta module supplies Phase 4 of the RS-native zeta program, connecting the Recognition Theta program to the completed zeta functional equation without claiming a full theta/Mellin analytic proof.
proof idea
This module imports the weak zero-free region and zeta-from-theta bridges then re-exports the Mathlib boundary theorem; no internal proofs are developed.
why it matters in Recognition Science
The module feeds ClassicalZeroFreeRegion, which tracks B1 of the RH unconditional-closure plan and notes that Mathlib supplies the boundary theorem re-exported here but lacks the logarithmic strip. It also supplies the base for XiSensorPickPositivity, which targets Pick/Schur positivity for the xi-sensor Cayley field on the unconditional route. In the RS framework it anchors the zeta program at the classical line before any critical-strip work.
scope and limits
- Does not prove any zero-free region for Re(s) < 1.
- Does not formalize the Hadamard-de la Vallee-Poussin logarithmic strip.
- Does not connect to the phi-ladder or J-cost constructions.
- Does not assume or derive the Riemann Hypothesis.
used by (2)
depends on (2)
declarations in this module (16)
-
theorem
riemannZeta_ne_zero_re_ge_one -
theorem
riemannZeta_ne_zero_re_gt_one -
structure
BoundaryZeroFreeCert -
def
boundaryZeroFreeCert -
structure
LogZeroFreeStrip -
def
StripZeroFreeBridge -
theorem
riemannZeta_ne_zero_in_log_strip -
structure
StripPhase5Cert -
def
stripPhase5Cert -
theorem
phase5_current_state -
structure
CriticalStripZeroFree -
def
CriticalStripZeroFreeBridge -
theorem
criticalStrip_zero_free_of_riemannHypothesis -
theorem
criticalStripZeroFreeBridge_of_riemannHypothesis -
structure
StripPhase7Cert -
def
stripPhase7Cert