module module

`IndisputableMonolith.NumberTheory.StripZeroFreeRegion`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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