classical_zfr_suffices

formal source

  81  explicit_formula : Prop  -- connects zeros to primes
  82  defect_budget : DefectBudget
  83
  84theorem classical_zfr_suffices :
  85    ∃ c : ℝ, 0 < c ∧ Nonempty (ZeroFreeRegion) := by
  86  use 1, one_pos
  87  exact ⟨classical_zfr 1 one_pos⟩
  88
  89/-! ## Comparison: What Full RH Gives vs What RS Needs
  90
  91| Property | Classical ZFR | Full RH |
  92|----------|--------------|---------|
  93| Error in π(x) | O(x^{1-c/log x}) | O(√x log x) |
  94| Sufficient for RS? | YES | YES (overkill) |
  95| Proved? | YES (1896) | NO |
  96| Axiom needed? | NO | YES (current) |
  97
  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