IndisputableMonolith.NumberTheory.StripZeroFreeRegion

   1import Mathlib
   2import IndisputableMonolith.NumberTheory.WeakZeroFreeRegion
   3import IndisputableMonolith.NumberTheory.ZetaFromTheta
   4
   5/-!
   6  StripZeroFreeRegion.lean
   7
   8  Phase 5 of the RS-native zeta program.
   9
  10  This module does two things:
  11
  12  1. It records the proven Mathlib zero-free result on the line/half-plane
  13     `Re(s) ≥ 1`.
  14  2. It names the genuine strip-zero-free theorem still needed for RH-quality
  15     closure.
  16
  17  We do not assert the strip theorem as proved.  It is packaged as the next
  18  bridge object, with a theorem showing that if the bridge exists then the
  19  corresponding zero-free conclusion follows.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace NumberTheory
  24namespace StripZeroFreeRegion
  25
  26noncomputable section
  27
  28/-! ## 1. Proven classical boundary region -/
  29
  30/-- Mathlib's de la Vallée-Poussin/Hadamard line theorem: `riemannZeta` is
  31nonzero on `Re(s) ≥ 1`. -/
  32theorem riemannZeta_ne_zero_re_ge_one {s : ℂ} (hs : 1 ≤ s.re) :
  33    riemannZeta s ≠ 0 :=
  34  riemannZeta_ne_zero_of_one_le_re hs
  35
  36/-- The corresponding strict half-plane theorem. -/
  37theorem riemannZeta_ne_zero_re_gt_one {s : ℂ} (hs : 1 < s.re) :
  38    riemannZeta s ≠ 0 :=
  39  riemannZeta_ne_zero_of_one_lt_re hs
  40
  41/-- Certificate for the proved boundary zero-free region. -/
  42structure BoundaryZeroFreeCert where
  43  ge_one : ∀ s : ℂ, 1 ≤ s.re → riemannZeta s ≠ 0
  44  gt_one : ∀ s : ℂ, 1 < s.re → riemannZeta s ≠ 0
  45
  46def boundaryZeroFreeCert : BoundaryZeroFreeCert where
  47  ge_one := fun _ hs => riemannZeta_ne_zero_re_ge_one hs
  48  gt_one := fun _ hs => riemannZeta_ne_zero_re_gt_one hs
  49
  50/-! ## 2. The true strip target -/
  51
  52/-- A logarithmic zero-free strip with constants `c` and `T`.
  53
  54For `|Im(s)| ≥ T`, the region
  55`Re(s) > 1 - c / log(|Im(s)|)` is zero-free. This is the classical
  56Hadamard-de la Vallée-Poussin shape, stated as the exact bridge needed by
  57the RS program. -/
  58structure LogZeroFreeStrip where
  59  c : ℝ
  60  T : ℝ
  61  c_pos : 0 < c
  62  T_gt_one : 1 < T
  63  zero_free :
  64    ∀ s : ℂ, T ≤ |s.im| →
  65      1 - c / Real.log |s.im| < s.re →
  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| →
 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
 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
 155bridge is named as a target, and we record that it is no stronger than RH. -/
 156structure StripPhase7Cert where
 157  boundary : BoundaryZeroFreeCert
 158  log_strip_bridge_named : True
 159  critical_strip_bridge_named : True
 160  critical_strip_implied_by_RH :
 161    RiemannHypothesis → CriticalStripZeroFreeBridge
 162
 163def stripPhase7Cert : StripPhase7Cert where
 164  boundary := boundaryZeroFreeCert
 165  log_strip_bridge_named := trivial
 166  critical_strip_bridge_named := trivial
 167  critical_strip_implied_by_RH :=
 168    criticalStripZeroFreeBridge_of_riemannHypothesis
 169
 170end
 171
 172end StripZeroFreeRegion
 173end NumberTheory
 174end IndisputableMonolith
 175