CriticalStripZeroFreeBridge

formal source

 121  zero_free : ∀ s : ℂ, 1/2 < s.re → s.re < 1 → riemannZeta s ≠ 0
 122
 123/-- The critical-strip bridge as a named target. -/
 124def CriticalStripZeroFreeBridge : Prop :=
 125  Nonempty CriticalStripZeroFree
 126
 127/-- Mathlib's `RiemannHypothesis` (every nontrivial nonpole zero is on the
 128critical line) implies the open right half-strip is zero-free. -/
 129theorem criticalStrip_zero_free_of_riemannHypothesis
 130    (hRH : RiemannHypothesis) :
 131    ∀ s : ℂ, 1/2 < s.re → s.re < 1 → riemannZeta s ≠ 0 := by
 132  intro s hlow hhigh hzero
 133  have hs1 : s ≠ 1 := by
 134    intro h
 135    have : s.re = 1 := by simp [h]
 136    linarith
 137  have hntriv : ¬ ∃ n : ℕ, s = -2 * (n + 1) := by
 138    rintro ⟨n, hn⟩
 139    have hre : s.re = -2 * ((n : ℝ) + 1) := by
 140      have := congrArg Complex.re hn
 141      simpa using this
 142    have hpos : (0 : ℝ) < 2 * ((n : ℝ) + 1) := by positivity
 143    have hneg : s.re < 0 := by rw [hre]; linarith
 144    linarith
 145  have hrhalf : s.re = 1 / 2 := hRH s hzero hntriv hs1
 146  linarith
 147
 148/-- Mathlib's RH implies the critical-strip bridge. -/
 149theorem criticalStripZeroFreeBridge_of_riemannHypothesis
 150    (hRH : RiemannHypothesis) :
 151    CriticalStripZeroFreeBridge :=
 152  ⟨{ zero_free := criticalStrip_zero_free_of_riemannHypothesis hRH }⟩
 153
 154/-- Phase 7 honest state: the boundary region is proved, the critical-strip