IndisputableMonolith.NumberTheory.RiemannHypothesis.XiSensorPickPositivity

   1import IndisputableMonolith.NumberTheory.RiemannHypothesis.BRFPlumbing
   2import IndisputableMonolith.NumberTheory.StripZeroFreeRegion
   3
   4/-!
   5  XiSensorPickPositivity.lean
   6
   7  The unconditional written route should not assume bounded defect cost. In
   8  the current formalization that is already RH-equivalent. The right target is
   9  Pick/Schur positivity for the xi-sensor Cayley field.
  10
  11  This module proves the first nontrivial algebraic fact needed by that route:
  12  finite Pick positivity implies the pointwise Schur bound from the one-point
  13  Pick matrix. The analytic step still missing is the theorem that this Schur
  14  bound excludes poles of `xi'/xi` in the right half-strip.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace NumberTheory
  19namespace RiemannHypothesis
  20namespace XiSensorPickPositivity
  21
  22open StripZeroFreeRegion
  23
  24noncomputable section
  25
  26/-- The open right half of the critical strip. -/
  27def RightHalfStrip (s : ℂ) : Prop :=
  28  1 / 2 < s.re ∧ s.re < 1
  29
  30/-- Abstract xi-sensor Cayley field. In the intended application,
  31`X(s) = (2 * (xi'/xi)(s) - 1) / (2 * (xi'/xi)(s) + 1)`. -/
  32abbrev XiCayleyField := ℂ → ℂ
  33
  34/-- A disk coordinate on the right half-strip. We keep it abstract: any
  35conformal chart into the unit disk is acceptable. -/
  36structure HalfStripDiskChart where
  37  φ : ℂ → ℂ
  38  maps_to_disk :
  39    ∀ s : ℂ, RightHalfStrip s → ‖φ s‖ < 1
  40
  41/-! ## A concrete disk chart -/
  42
  43/-- Strict Cayley bound: the standard Cayley transform sends the open right
  44half-plane to the open unit disk. -/
  45theorem norm_cayley_lt_one_of_re_pos {z : ℂ} (hz : 0 < z.re) :
  46    ‖cayley z‖ < 1 := by
  47  have hz1 : z + 1 ≠ 0 := by
  48    intro h
  49    have hzneg : z = (-1 : ℂ) := by
  50      have : z = -(1 : ℂ) := eq_neg_of_add_eq_zero_left h
  51      simpa using this
  52    have : (0 : ℝ) < (-1 : ℂ).re := by simpa [hzneg] using hz
  53    have : (0 : ℝ) < (-1 : ℝ) := by simpa using this
  54    nlinarith
  55  have hpos : 0 < Complex.normSq (z + 1) :=
  56    (Complex.normSq_pos).2 hz1
  57  have hlt : Complex.normSq (z - 1) < Complex.normSq (z + 1) := by
  58    have hdiff :
  59        Complex.normSq (z + 1) - Complex.normSq (z - 1) = 4 * z.re :=
  60      normSq_add_one_sub_normSq_sub_one z
  61    have : 0 < Complex.normSq (z + 1) - Complex.normSq (z - 1) := by
  62      rw [hdiff]
  63      nlinarith
  64    exact sub_pos.mp this
  65  have hnSq : Complex.normSq ((z - 1) / (z + 1)) < 1 := by
  66    have : Complex.normSq (z - 1) / Complex.normSq (z + 1) < 1 :=
  67      (div_lt_one hpos).2 hlt
  68    simpa [Complex.normSq_div] using this
  69  have hsq : ‖(z - 1) / (z + 1)‖ ^ 2 < 1 := by
  70    calc
  71      ‖(z - 1) / (z + 1)‖ ^ 2
  72          = Complex.normSq ((z - 1) / (z + 1)) := by
  73            simpa using (Complex.sq_norm ((z - 1) / (z + 1)))
  74      _ < 1 := hnSq
  75  have hw : 0 ≤ ‖(z - 1) / (z + 1)‖ := norm_nonneg _
  76  have : ‖(z - 1) / (z + 1)‖ < 1 := by nlinarith [hsq, hw]
  77  simpa [cayley] using this
  78
  79/-- Translate the critical line to the imaginary axis before applying Cayley. -/
  80noncomputable def rightHalfPlaneDiskChart : HalfStripDiskChart where
  81  φ := fun s => cayley (s - (1 / 2 : ℂ))
  82  maps_to_disk := by
  83    intro s hs
  84    apply norm_cayley_lt_one_of_re_pos
  85    simp [Complex.sub_re]
  86    simpa [one_div] using hs.1
  87
  88/-- One-point Pick positivity. This is the `N = 1` principal minor of the
  89full Pick matrix. -/
  90def OnePointPickPositive (chart : HalfStripDiskChart)
  91    (X : XiCayleyField) : Prop :=
  92  ∀ s : ℂ, RightHalfStrip s →
  93    0 ≤ (1 - ‖X s‖ ^ 2) / (1 - ‖chart.φ s‖ ^ 2)
  94
  95/-- Full finite Pick positivity, stated as an interface. The one-point field is
  96included explicitly because it is the part we use theorem-grade here. -/
  97structure FinitePickPositive (chart : HalfStripDiskChart)
  98    (X : XiCayleyField) : Prop where
  99  one_point : OnePointPickPositive chart X
 100  finite_matrices_positive : True
 101
 102/-- The Schur bound on the right half-strip. -/
 103def SchurOnRightHalfStrip (X : XiCayleyField) : Prop :=
 104  ∀ s : ℂ, RightHalfStrip s → ‖X s‖ ≤ 1
 105
 106/-- One-point Pick positivity forces the pointwise Schur bound. -/
 107theorem schur_of_onePointPickPositive
 108    (chart : HalfStripDiskChart) (X : XiCayleyField)
 109    (hpick : OnePointPickPositive chart X) :
 110    SchurOnRightHalfStrip X := by
 111  intro s hs
 112  have hden_pos : 0 < 1 - ‖chart.φ s‖ ^ 2 := by
 113    have hφ : ‖chart.φ s‖ < 1 := chart.maps_to_disk s hs
 114    have hφ_nonneg : 0 ≤ ‖chart.φ s‖ := norm_nonneg _
 115    nlinarith
 116  have hfrac : 0 ≤ (1 - ‖X s‖ ^ 2) / (1 - ‖chart.φ s‖ ^ 2) :=
 117    hpick s hs
 118  have hnum_nonneg : 0 ≤ 1 - ‖X s‖ ^ 2 := by
 119    have hmul :
 120        0 ≤ ((1 - ‖X s‖ ^ 2) / (1 - ‖chart.φ s‖ ^ 2)) *
 121          (1 - ‖chart.φ s‖ ^ 2) :=
 122      mul_nonneg hfrac hden_pos.le
 123    field_simp [ne_of_gt hden_pos] at hmul
 124    exact hmul
 125  have hx_nonneg : 0 ≤ ‖X s‖ := norm_nonneg _
 126  nlinarith
 127
 128/-- Full finite Pick positivity implies the Schur bound. -/
 129theorem schur_of_finitePickPositive
 130    (chart : HalfStripDiskChart) (X : XiCayleyField)
 131    (hpick : FinitePickPositive chart X) :
 132    SchurOnRightHalfStrip X :=
 133  schur_of_onePointPickPositive chart X hpick.one_point
 134
 135/-- The remaining analytic theorem: Schur contractivity of the xi-sensor Cayley
 136field excludes poles of `xi'/xi`, hence excludes zeta zeros, in the right
 137half-strip. This is not algebra; it is the analytic removable-singularity /
 138pole-saturation step. -/
 139def XiSchurNoPolesPrinciple (X : XiCayleyField) : Prop :=
 140  SchurOnRightHalfStrip X → CriticalStripZeroFreeBridge
 141
 142/-- Conditional closure: finite Pick positivity plus the Schur no-poles
 143principle gives the critical-strip bridge. -/
 144theorem criticalStripBridge_of_pickPositive
 145    (chart : HalfStripDiskChart) (X : XiCayleyField)
 146    (hpick : FinitePickPositive chart X)
 147    (hnoPoles : XiSchurNoPolesPrinciple X) :
 148    CriticalStripZeroFreeBridge :=
 149  hnoPoles (schur_of_finitePickPositive chart X hpick)
 150
 151/-- Machine-readable status for the xi-sensor Pick route. -/
 152structure XiSensorPickRouteStatus where
 153  pick_to_schur :
 154    ∀ (chart : HalfStripDiskChart) (X : XiCayleyField),
 155      FinitePickPositive chart X → SchurOnRightHalfStrip X
 156  schur_to_zero_free_open :
 157    ∀ X : XiCayleyField, XiSchurNoPolesPrinciple X → Prop
 158
 159def xiSensorPickRouteStatus : XiSensorPickRouteStatus where
 160  pick_to_schur := schur_of_finitePickPositive
 161  schur_to_zero_free_open := fun _ _ => True
 162
 163end
 164
 165end XiSensorPickPositivity
 166end RiemannHypothesis
 167end NumberTheory
 168end IndisputableMonolith
 169