IndisputableMonolith.NumberTheory.ZeroLocationCost

   1import Mathlib
   2import IndisputableMonolith.Foundation.LawOfExistence
   3import IndisputableMonolith.Foundation.DiscretenessForcing
   4
   5/-!
   6# Zero Location Cost
   7
   8This module formalizes the RS dictionary between zeta-zero location and
   9zero-defect cost:
  10
  11* `zeroDeviation ρ = 2 (Re ρ - 1/2)`
  12* `zeroDefect ρ = defect (exp (zeroDeviation ρ))`
  13
  14The critical line `Re ρ = 1/2` is therefore exactly the zero-defect locus.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace NumberTheory
  19
  20open scoped ComplexConjugate
  21
  22noncomputable section
  23
  24/-- The critical-line predicate for a complex point. -/
  25def OnCriticalLine (ρ : ℂ) : Prop :=
  26  ρ.re = 1 / 2
  27
  28/-- Reflection across the line `Re(s) = 1/2`. -/
  29def functionalReflection (ρ : ℂ) : ℂ :=
  30  1 - ρ
  31
  32/-- Reflection across the line `Re(s) = 1/2`, composed with conjugation. -/
  33def criticalReflection (ρ : ℂ) : ℂ :=
  34  1 - conj ρ
  35
  36/-- The real deviation of `ρ` from the critical line, expressed in the
  37log-coordinate scale compatible with the RS defect functional. -/
  38def zeroDeviation (ρ : ℂ) : ℝ :=
  39  2 * (ρ.re - 1 / 2)
  40
  41/-- The RS defect attached to the zero-location deviation of `ρ`. -/
  42def zeroDefect (ρ : ℂ) : ℝ :=
  43  Foundation.LawOfExistence.defect (Real.exp (zeroDeviation ρ))
  44
  45/-- The zero-location defect is exactly `J_log` evaluated on the deviation. -/
  46theorem zeroDefect_eq_J_log (ρ : ℂ) :
  47    zeroDefect ρ =
  48      Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
  49  simpa [zeroDefect] using
  50    (Foundation.DiscretenessForcing.J_log_eq_J_exp (zeroDeviation ρ)).symm
  51
  52/-- Expanded closed form for the zero-location defect. -/
  53theorem zeroDefect_eq_cosh_sub_one (ρ : ℂ) :
  54    zeroDefect ρ = Real.cosh (zeroDeviation ρ) - 1 := by
  55  simpa [Foundation.DiscretenessForcing.J_log] using zeroDefect_eq_J_log ρ
  56
  57/-- A point lies on the critical line exactly when its zero deviation is zero. -/
  58theorem zeroDeviation_eq_zero_iff_on_critical_line (ρ : ℂ) :
  59    zeroDeviation ρ = 0 ↔ OnCriticalLine ρ := by
  60  unfold zeroDeviation OnCriticalLine
  61  constructor
  62  · intro h
  63    linarith
  64  · intro h
  65    linarith
  66
  67/-- The zero-location defect vanishes exactly on the critical line. -/
  68theorem zeroDefect_zero_iff_on_critical_line (ρ : ℂ) :
  69    zeroDefect ρ = 0 ↔ OnCriticalLine ρ := by
  70  rw [zeroDefect_eq_J_log]
  71  constructor
  72  · intro h
  73    have hz :
  74        zeroDeviation ρ = 0 :=
  75      (Foundation.DiscretenessForcing.J_log_eq_zero_iff).mp h
  76    exact (zeroDeviation_eq_zero_iff_on_critical_line ρ).mp hz
  77  · intro h
  78    have hz : zeroDeviation ρ = 0 :=
  79      (zeroDeviation_eq_zero_iff_on_critical_line ρ).mpr h
  80    exact (Foundation.DiscretenessForcing.J_log_eq_zero_iff).mpr hz
  81
  82/-- Off the critical line, the zero-location defect is strictly positive. -/
  83theorem zeroDefect_pos_iff_off_critical_line (ρ : ℂ) :
  84    0 < zeroDefect ρ ↔ ¬ OnCriticalLine ρ := by
  85  rw [zeroDefect_eq_J_log]
  86  constructor
  87  · intro h hline
  88    have hzero :
  89        Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) = 0 :=
  90      (Foundation.DiscretenessForcing.J_log_eq_zero_iff).mpr
  91        ((zeroDeviation_eq_zero_iff_on_critical_line ρ).mpr hline)
  92    linarith
  93  · intro hline
  94    have hneq : zeroDeviation ρ ≠ 0 := by
  95      intro hz
  96      exact hline ((zeroDeviation_eq_zero_iff_on_critical_line ρ).mp hz)
  97    exact Foundation.DiscretenessForcing.J_log_pos hneq
  98
  99/-- The zero-location defect is nonnegative everywhere. -/
 100theorem zeroDefect_nonneg (ρ : ℂ) : 0 ≤ zeroDefect ρ := by
 101  rw [zeroDefect_eq_J_log]
 102  exact Foundation.DiscretenessForcing.J_log_nonneg (zeroDeviation ρ)
 103
 104@[simp] theorem functionalReflection_re (ρ : ℂ) :
 105    (functionalReflection ρ).re = 1 - ρ.re := by
 106  simp [functionalReflection]
 107
 108@[simp] theorem criticalReflection_re (ρ : ℂ) :
 109    (criticalReflection ρ).re = 1 - ρ.re := by
 110  simp [criticalReflection]
 111
 112@[simp] theorem zeroDeviation_functionalReflection (ρ : ℂ) :
 113    zeroDeviation (functionalReflection ρ) = -zeroDeviation ρ := by
 114  unfold zeroDeviation functionalReflection
 115  simp
 116  linarith
 117
 118@[simp] theorem zeroDeviation_conj (ρ : ℂ) :
 119    zeroDeviation (conj ρ) = zeroDeviation ρ := by
 120  simp [zeroDeviation]
 121
 122@[simp] theorem zeroDeviation_criticalReflection (ρ : ℂ) :
 123    zeroDeviation (criticalReflection ρ) = -zeroDeviation ρ := by
 124  unfold zeroDeviation criticalReflection
 125  simp
 126  linarith
 127
 128/-- Reflection across `Re(s) = 1/2` preserves the zero-location defect. -/
 129theorem zeroDefect_invariant_under_functional_reflection (ρ : ℂ) :
 130    zeroDefect (functionalReflection ρ) = zeroDefect ρ := by
 131  calc
 132    zeroDefect (functionalReflection ρ)
 133        =
 134          Foundation.DiscretenessForcing.J_log
 135            (zeroDeviation (functionalReflection ρ)) := zeroDefect_eq_J_log _
 136    _ = Foundation.DiscretenessForcing.J_log (-zeroDeviation ρ) := by
 137          rw [zeroDeviation_functionalReflection]
 138    _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
 139          exact Foundation.DiscretenessForcing.J_log_symmetric (zeroDeviation ρ)
 140    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 141
 142/-- Conjugation preserves the zero-location defect. -/
 143theorem zeroDefect_invariant_under_conjugation (ρ : ℂ) :
 144    zeroDefect (conj ρ) = zeroDefect ρ := by
 145  calc
 146    zeroDefect (conj ρ)
 147        =
 148          Foundation.DiscretenessForcing.J_log
 149            (zeroDeviation (conj ρ)) := zeroDefect_eq_J_log _
 150    _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
 151          rw [zeroDeviation_conj]
 152    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 153
 154/-- Reflection plus conjugation preserves the zero-location defect. -/
 155theorem zeroDefect_invariant_under_reflection (ρ : ℂ) :
 156    zeroDefect (criticalReflection ρ) = zeroDefect ρ := by
 157  calc
 158    zeroDefect (criticalReflection ρ)
 159        =
 160          Foundation.DiscretenessForcing.J_log
 161            (zeroDeviation (criticalReflection ρ)) := zeroDefect_eq_J_log _
 162    _ = Foundation.DiscretenessForcing.J_log (-zeroDeviation ρ) := by
 163          rw [zeroDeviation_criticalReflection]
 164    _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
 165          exact Foundation.DiscretenessForcing.J_log_symmetric (zeroDeviation ρ)
 166    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 167
 168end
 169
 170end NumberTheory
 171end IndisputableMonolith
 172