structure
definition
StripPhase7Cert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.StripZeroFreeRegion on GitHub at line 156.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
153
154/-- Phase 7 honest state: the boundary region is proved, the critical-strip
155bridge is named as a target, and we record that it is no stronger than RH. -/
156structure StripPhase7Cert where
157 boundary : BoundaryZeroFreeCert
158 log_strip_bridge_named : True
159 critical_strip_bridge_named : True
160 critical_strip_implied_by_RH :
161 RiemannHypothesis → CriticalStripZeroFreeBridge
162
163def stripPhase7Cert : StripPhase7Cert where
164 boundary := boundaryZeroFreeCert
165 log_strip_bridge_named := trivial
166 critical_strip_bridge_named := trivial
167 critical_strip_implied_by_RH :=
168 criticalStripZeroFreeBridge_of_riemannHypothesis
169
170end
171
172end StripZeroFreeRegion
173end NumberTheory
174end IndisputableMonolith