pith. sign in
module module high

IndisputableMonolith.NumberTheory.StripZeroFreeRegion

show as:
view Lean formalization →

This module re-exports Mathlib's classical boundary theorem that the Riemann zeta function has no zeros for Re(s) ≥ 1. It supplies the edge case needed by the Recognition Science zeta program to bridge weak zero-free results and theta-function constructions toward unconditional RH closure. The module itself contains no new proofs and consists of imports plus re-exports.

claim$\zeta(s) \neq 0$ whenever $\operatorname{Re}(s) \geq 1$.

background

The module sits inside the NumberTheory domain of the Recognition Science formalization. It imports WeakZeroFreeRegion, whose doc-comment asks whether the RS defect-budget bridge can eliminate or weaken the full RH conditional axiom, and ZetaFromTheta, which isolates the theta-style Mellin transform bridge to the completed zeta functional equation.

The supplied DOC_COMMENT identifies the module's sole mathematical content as Mathlib's de la Vallée-Poussin/Hadamard line theorem. No new definitions of J-cost, defectDist, or phi-ladder appear here; the module simply makes the classical boundary available to downstream RS arguments.

proof idea

This is a definition module, no proofs. It consists of three imports that bring in the Mathlib theorem riemannZeta_ne_zero_of_one_le_re together with the two RS-native zeta modules.

why it matters in Recognition Science

The module feeds ClassicalZeroFreeRegion (Track B1 of the RH unconditional-closure plan) and XiSensorPickPositivity (the route that avoids assuming bounded defect cost). Its doc-comment cites the boundary theorem that ClassicalZeroFreeRegion notes is already present in Mathlib but not yet extended to a formal logarithmic zero-free strip.

scope and limits

used by (2)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)