pith. machine review for the scientific record. sign in
theorem proved term proof

classical_zfr_suffices

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  84theorem classical_zfr_suffices :
  85    ∃ c : ℝ, 0 < c ∧ Nonempty (ZeroFreeRegion) := by

proof body

Term-mode proof.

  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

depends on (7)

Lean names referenced from this declaration's body.