`weak_zfr_cert_exists`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.WeakZeroFreeRegion
domain: NumberTheory
line: 110 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.WeakZeroFreeRegion on GitHub at line 110.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.