module module high

`IndisputableMonolith.NumberTheory.StripZeroFreeRegion`

This module re-exports Mathlib's classical theorem that the Riemann zeta function has no zeros for Re(s) ≥ 1. It supplies the boundary case required by Recognition Science zero-free region arguments that aim to weaken or eliminate the full RH axiom. The module performs no new proofs and consists of imports plus re-exports from WeakZeroFreeRegion and ZetaFromTheta.

claimThe Riemann zeta function satisfies $ζ(s) ≠ 0$ whenever Re$(s) ≥ 1$.

background

The module operates inside the NumberTheory component of the Recognition Science formalization. It imports WeakZeroFreeRegion, whose documentation asks whether the RH conditional axiom can be eliminated or weakened via the defect-budget bridge, and ZetaFromTheta, which isolates the theta-style Mellin transform bridge to the completed zeta functional equation. The central object is the classical boundary theorem, stated as riemannZeta nonzero on the closed half-plane Re(s) ≥ 1.

proof idea

This is a re-export module with no internal proofs. It pulls the de la Vallée-Poussin/Hadamard line theorem directly from Mathlib and makes it available to downstream zero-free region constructions.

why it matters in Recognition Science

The module supplies the boundary theorem required by ClassicalZeroFreeRegion (which tracks Track B1 of the RH unconditional-closure plan) and by XiSensorPickPositivity (which develops the Pick/Schur positivity route that avoids assuming bounded defect cost). It therefore anchors the classical line result before any logarithmic strip or RS-native extension is attempted.

scope and limits

Does not prove a zero-free strip of positive width to the left of Re(s) = 1.
Does not contain the full Hadamard-de la Vallée-Poussin logarithmic zero-free region.
Does not derive the boundary theorem from Recognition Science primitives; it re-exports the Mathlib statement.
Does not address conditional or unconditional closure of the Riemann Hypothesis itself.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion module_import
IndisputableMonolith.NumberTheory.RiemannHypothesis.XiSensorPickPositivity module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.WeakZeroFreeRegion module_import
IndisputableMonolith.NumberTheory.ZetaFromTheta module_import

declarations in this module (16)

theorem riemannZeta_ne_zero_re_ge_one L32
theorem riemannZeta_ne_zero_re_gt_one L37
structure BoundaryZeroFreeCert L42
def boundaryZeroFreeCert L46
structure LogZeroFreeStrip L58
def StripZeroFreeBridge L69
theorem riemannZeta_ne_zero_in_log_strip L73
structure StripPhase5Cert L86
def stripPhase5Cert L90
theorem phase5_current_state L96
structure CriticalStripZeroFree L120
def CriticalStripZeroFreeBridge L124
theorem criticalStrip_zero_free_of_riemannHypothesis L129
theorem criticalStripZeroFreeBridge_of_riemannHypothesis L149
structure StripPhase7Cert L156
def stripPhase7Cert L163