IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion

   1import IndisputableMonolith.NumberTheory.StripZeroFreeRegion
   2
   3/-!
   4  ClassicalZeroFreeRegion.lean
   5
   6  Track B1 of the RH unconditional-closure plan.
   7
   8  Mathlib currently gives the boundary theorem
   9  `riemannZeta_ne_zero_of_one_le_re`, re-exported in
  10  `StripZeroFreeRegion.lean`. It does not yet contain a formal
  11  Hadamard-de la Vallee-Poussin logarithmic zero-free strip.
  12
  13  This module starts the classical port without pretending that the hard
  14  analytic theorem is already in the library:
  15
  16  * it proves the elementary trigonometric positivity kernel
  17    `3 + 4 cos θ + cos 2θ = 2(cos θ + 1)^2 ≥ 0`;
  18  * it isolates the exact analytic input whose proof would inhabit
  19    `LogZeroFreeStrip`;
  20  * it provides the conversion from that input to `StripZeroFreeBridge`.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace NumberTheory
  25namespace ClassicalZeroFreeRegion
  26
  27open StripZeroFreeRegion
  28
  29noncomputable section
  30
  31/-! ## 1. The de la Vallee-Poussin positivity kernel -/
  32
  33/-- The classical nonnegative trigonometric kernel used in the
  34Hadamard-de la Vallee-Poussin argument. -/
  35theorem deLaValleePoussin_trig_kernel_eq_square (θ : ℝ) :
  36    3 + 4 * Real.cos θ + Real.cos (2 * θ) =
  37      2 * (Real.cos θ + 1) ^ 2 := by
  38  rw [Real.cos_two_mul]
  39  ring
  40
  41/-- Positivity of the de la Vallee-Poussin trigonometric kernel. -/
  42theorem deLaValleePoussin_trig_kernel_nonneg (θ : ℝ) :
  43    0 ≤ 3 + 4 * Real.cos θ + Real.cos (2 * θ) := by
  44  rw [deLaValleePoussin_trig_kernel_eq_square θ]
  45  nlinarith [sq_nonneg (Real.cos θ + 1)]
  46
  47/-! ## 2. Exact analytic input needed for the logarithmic strip -/
  48
  49/-- The classical Hadamard-de la Vallee-Poussin zero-free strip, stated in the
  50same shape as `StripZeroFreeRegion.LogZeroFreeStrip`.
  51
  52This is intentionally a structure, not an axiom. Supplying an inhabitant is the
  53real Mathlib-grade analytic work: logarithmic derivative estimates for `ζ`,
  54the positivity kernel above, and control of the pole at `s = 1`. -/
  55structure DeLaValleePoussinZeroFreeRegion where
  56  c : ℝ
  57  T : ℝ
  58  c_pos : 0 < c
  59  T_gt_one : 1 < T
  60  zero_free :
  61    ∀ s : ℂ, T ≤ |s.im| →
  62      1 - c / Real.log |s.im| < s.re →
  63        riemannZeta s ≠ 0
  64
  65/-- The classical zero-free-region input directly inhabits the Phase 5
  66`LogZeroFreeStrip` bridge object. -/
  67def logZeroFreeStrip_of_deLaValleePoussin
  68    (zfr : DeLaValleePoussinZeroFreeRegion) :
  69    LogZeroFreeStrip where
  70  c := zfr.c
  71  T := zfr.T
  72  c_pos := zfr.c_pos
  73  T_gt_one := zfr.T_gt_one
  74  zero_free := zfr.zero_free
  75
  76/-- The de la Vallee-Poussin theorem, once formalized, supplies the named
  77`StripZeroFreeBridge`. -/
  78theorem stripZeroFreeBridge_of_deLaValleePoussin
  79    (zfr : DeLaValleePoussinZeroFreeRegion) :
  80    StripZeroFreeBridge :=
  81  ⟨logZeroFreeStrip_of_deLaValleePoussin zfr⟩
  82
  83/-! ## 3. B1 status bundle -/
  84
  85/-- Machine-readable Track B1 status. The elementary positivity kernel is
  86proved; the remaining field is exactly the classical analytic zero-free-region
  87input. -/
  88structure ClassicalZeroFreeRegionAttackSurface where
  89  trig_kernel_nonneg :
  90    ∀ θ : ℝ, 0 ≤ 3 + 4 * Real.cos θ + Real.cos (2 * θ)
  91  open_deLaValleePoussin :
  92    DeLaValleePoussinZeroFreeRegion → StripZeroFreeBridge
  93
  94def classicalZeroFreeRegionAttackSurface :
  95    ClassicalZeroFreeRegionAttackSurface where
  96  trig_kernel_nonneg := deLaValleePoussin_trig_kernel_nonneg
  97  open_deLaValleePoussin := stripZeroFreeBridge_of_deLaValleePoussin
  98
  99end
 100
 101end ClassicalZeroFreeRegion
 102end NumberTheory
 103end IndisputableMonolith
 104