StripZeroFreeBridge

formal source

  66        riemannZeta s ≠ 0
  67
  68/-- The strip theorem as the next named bridge. -/
  69def StripZeroFreeBridge : Prop :=
  70  Nonempty LogZeroFreeStrip
  71
  72/-- Any strip bridge gives the corresponding zero-free conclusion. -/
  73theorem riemannZeta_ne_zero_in_log_strip
  74    (bridge : StripZeroFreeBridge) :
  75    ∃ c T : ℝ, 0 < c ∧ 1 < T ∧
  76      ∀ s : ℂ, T ≤ |s.im| →
  77        1 - c / Real.log |s.im| < s.re →
  78          riemannZeta s ≠ 0 := by
  79  rcases bridge with ⟨strip⟩
  80  exact ⟨strip.c, strip.T, strip.c_pos, strip.T_gt_one, strip.zero_free⟩
  81
  82/-! ## 3. Relation to the weak zero-free-region module -/
  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| →