  83
  84/-- A proven boundary certificate and a named open strip bridge are exactly the
  85honest Phase 5 state. -/
  86structure StripPhase5Cert where
  87  boundary : BoundaryZeroFreeCert
  88  strip_bridge : StripZeroFreeBridge → Prop
  89
  90def stripPhase5Cert : StripPhase5Cert where
  91  boundary := boundaryZeroFreeCert
  92  strip_bridge := fun _ => True
  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. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.