theorem
proved
rh_axiom_replaceable
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.WeakZeroFreeRegion on GitHub at line 101.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
98The conclusion: the RH_conditional_axiom can be replaced by the
99classical ZFR, which is a theorem (not an axiom). -/
100
101theorem rh_axiom_replaceable :
102 Nonempty ZeroFreeRegion := ⟨classical_zfr 1 one_pos⟩
103
104/-! ## Certificate -/
105
106structure WeakZFRCert where
107 classical_exists : Nonempty ZeroFreeRegion
108 defect_gives_zfr : ∀ (db : DefectBudget), ∃ c, 0 < c ∧ ∀ t, 1 < t → c / Real.log t > 0
109
110theorem weak_zfr_cert_exists : Nonempty WeakZFRCert :=
111 ⟨{ classical_exists := rh_axiom_replaceable
112 defect_gives_zfr := defect_implies_zero_free }⟩
113
114end
115
116end IndisputableMonolith.NumberTheory.WeakZeroFreeRegion