RSChainRequirements

formal source

  75The RS number theory chain needs only the classical zero-free region,
  76not the full Riemann Hypothesis. -/
  77
  78structure RSChainRequirements where
  79  zero_free : ZeroFreeRegion
  80  prime_counting : Prop  -- π(x) ~ x/ln(x)
  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