defect_implies_zero_free

formal source

  65  defect_positive : 0 < total_defect
  66  defect_bounded : total_defect ≤ 1  -- normalized
  67
  68theorem defect_implies_zero_free (db : DefectBudget) :
  69    ∃ c : ℝ, 0 < c ∧ ∀ t, 1 < t → c / Real.log t > 0 := by
  70  use db.total_defect
  71  exact ⟨db.defect_positive, fun t ht => div_pos db.defect_positive (Real.log_pos ht)⟩
  72
  73/-! ## RS Chain Sufficiency
  74
  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