phase5_current_state

formal source

  93
  94/-- The current unconditional zero-free region available to the RS zeta program
  95is the boundary region `Re ≥ 1`; the logarithmic strip is the named bridge. -/
  96theorem phase5_current_state :
  97    (∀ s : ℂ, 1 ≤ s.re → riemannZeta s ≠ 0) ∧
  98      (StripZeroFreeBridge → ∃ c T : ℝ, 0 < c ∧ 1 < T ∧
  99        ∀ s : ℂ, T ≤ |s.im| →
 100          1 - c / Real.log |s.im| < s.re →
 101            riemannZeta s ≠ 0) := by
 102  exact ⟨fun s hs => riemannZeta_ne_zero_re_ge_one hs,
 103    riemannZeta_ne_zero_in_log_strip⟩
 104
 105/-! ## 4. Phase 7: critical-strip zero-free bridge
 106
 107The `LogZeroFreeStrip` above is the classical de la Vallée-Poussin shape and
 108is not enough to close the recovered RH chain. The chain is built around
 109witnessed defect sensors with `1/2 < Re(ρ) < 1`, so vacuous closure requires
 110zero-freeness on the open right half of the critical strip. That bridge is
 111the actual analytic input sitting between the recovered chain and a
 112million-dollar theorem.
 113
 114We name it explicitly here. We do not inhabit it. We do prove that it is
 115implied by Mathlib's formal Riemann hypothesis, so callers can see the
 116irreducible analytic content. -/
 117
 118/-- Critical-strip zero-free witness: `riemannZeta s ≠ 0` for every
 119`s` with `1/2 < Re(s) < 1`. -/
 120structure CriticalStripZeroFree where
 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