IndisputableMonolith.NumberTheory.RiemannHypothesis.BRFPlumbing

   1import Mathlib
   2
   3/-!
   4# Riemann Hypothesis (BRF route): Cayley / Schur plumbing
   5
   6This file formalizes the **purely algebraic** part of the bounded-real / Schur/Herglotz route
   7appearing in `docs/primes/Riemann-proofs/Riemann-active.txt`:
   8
   9- A function `H` is (half-plane) **Herglotz** when `0 ≤ Re H`.
  10- Its Cayley transform `Θ = (H - 1)/(H + 1)` is **Schur** when `‖Θ‖ ≤ 1`.
  11
  12The key point for the RH route is that this step is *fully unconditional* and requires
  13no analytic number theory—only complex algebra.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace NumberTheory
  18namespace RiemannHypothesis
  19
  20open scoped Real
  21
  22/-!
  23## Cayley transform: right half-plane → unit disk
  24-/
  25
  26/-- The Cayley transform sending the right half-plane to the unit disk:
  27`cayley H = (H - 1)/(H + 1)`. -/
  28noncomputable def cayley (H : ℂ) : ℂ :=
  29  (H - 1) / (H + 1)
  30
  31theorem normSq_add_one_sub_normSq_sub_one (z : ℂ) :
  32    Complex.normSq (z + 1) - Complex.normSq (z - 1) = 4 * z.re := by
  33  -- Expand `normSq` into re/im coordinates.
  34  simp [Complex.normSq_apply]
  35  ring
  36
  37/-- If `Re z ≥ 0`, then the Cayley transform lies in the closed unit disk. -/
  38theorem norm_cayley_le_one_of_re_nonneg {z : ℂ} (hz : 0 ≤ z.re) :
  39    ‖cayley z‖ ≤ 1 := by
  40  -- `z ≠ -1`, hence `z + 1 ≠ 0`, hence `normSq (z+1) > 0`.
  41  have hz1 : z + 1 ≠ 0 := by
  42    intro h
  43    have hzneg : z = (-1 : ℂ) := by
  44      have : z = -(1 : ℂ) := eq_neg_of_add_eq_zero_left h
  45      simpa using this
  46    have : (0 : ℝ) ≤ (-1 : ℂ).re := by simpa [hzneg] using hz
  47    -- contradiction: `0 ≤ -1`
  48    have : (0 : ℝ) ≤ (-1 : ℝ) := by simpa using this
  49    nlinarith
  50  have hpos : 0 < Complex.normSq (z + 1) :=
  51    (Complex.normSq_pos).2 hz1
  52
  53  -- Show `normSq (z-1) ≤ normSq (z+1)` by an explicit identity.
  54  have hle : Complex.normSq (z - 1) ≤ Complex.normSq (z + 1) := by
  55    have : 0 ≤ Complex.normSq (z + 1) - Complex.normSq (z - 1) := by
  56      have : 0 ≤ 4 * z.re := by nlinarith [hz]
  57      simpa [normSq_add_one_sub_normSq_sub_one z] using this
  58    exact (sub_nonneg).1 this
  59
  60  -- Convert `normSq` control into a norm bound via `‖z‖^2 = normSq z`.
  61  have hnSq : Complex.normSq ((z - 1) / (z + 1)) ≤ 1 := by
  62    have : Complex.normSq (z - 1) / Complex.normSq (z + 1) ≤ 1 :=
  63      (div_le_one hpos).2 hle
  64    simpa [Complex.normSq_div] using this
  65  have hsq : ‖(z - 1) / (z + 1)‖ ^ 2 ≤ 1 := by
  66    -- Avoid `simp` rewriting the goal into an `abs`-form; use a direct `calc`.
  67    calc
  68      ‖(z - 1) / (z + 1)‖ ^ 2 = Complex.normSq ((z - 1) / (z + 1)) := by
  69        simpa using (Complex.sq_norm ((z - 1) / (z + 1)))
  70      _ ≤ 1 := hnSq
  71  have hw : 0 ≤ ‖(z - 1) / (z + 1)‖ := norm_nonneg _
  72  -- `0 ≤ ‖w‖` and `‖w‖^2 ≤ 1` implies `‖w‖ ≤ 1`.
  73  have : ‖(z - 1) / (z + 1)‖ ≤ 1 := by nlinarith [hsq, hw]
  74  simpa [cayley] using this
  75
  76/-- If the Cayley transform lies in the closed unit disk and `z ≠ -1`,
  77then `Re z ≥ 0`. -/
  78theorem re_nonneg_of_norm_cayley_le_one {z : ℂ} (hz : z ≠ (-1 : ℂ))
  79    (h : ‖cayley z‖ ≤ 1) :
  80    0 ≤ z.re := by
  81  have hz1 : z + 1 ≠ 0 := by
  82    intro h0
  83    have : z = (-1 : ℂ) := by
  84      have : z = -(1 : ℂ) := eq_neg_of_add_eq_zero_left h0
  85      simpa using this
  86    exact hz this
  87  have hpos : 0 < Complex.normSq (z + 1) :=
  88    (Complex.normSq_pos).2 hz1
  89
  90  -- Square the norm inequality to reach a `normSq` inequality.
  91  have hnSq_ratio : Complex.normSq ((z - 1) / (z + 1)) ≤ 1 := by
  92    have hw : 0 ≤ ‖(z - 1) / (z + 1)‖ := norm_nonneg _
  93    have hsq : ‖(z - 1) / (z + 1)‖ ^ 2 ≤ 1 := by
  94      have h' : ‖(z - 1) / (z + 1)‖ ≤ 1 := by
  95        simpa [cayley] using h
  96      -- `linarith` struggles with squares; `nlinarith` works.
  97      nlinarith [h', hw]
  98    -- Convert using `‖w‖^2 = normSq w` without `simp` rewriting into an `abs`-form.
  99    calc
 100      Complex.normSq ((z - 1) / (z + 1))
 101          = ‖(z - 1) / (z + 1)‖ ^ 2 := by
 102            simpa using (Complex.sq_norm ((z - 1) / (z + 1))).symm
 103      _ ≤ 1 := hsq
 104  have hratio : Complex.normSq (z - 1) / Complex.normSq (z + 1) ≤ 1 := by
 105    simpa [Complex.normSq_div] using hnSq_ratio
 106  have hle : Complex.normSq (z - 1) ≤ Complex.normSq (z + 1) :=
 107    (div_le_one hpos).1 hratio
 108
 109  have : 0 ≤ Complex.normSq (z + 1) - Complex.normSq (z - 1) :=
 110    (sub_nonneg).2 hle
 111  have : 0 ≤ 4 * z.re := by
 112    simpa [normSq_add_one_sub_normSq_sub_one z] using this
 113  nlinarith
 114
 115/-!
 116## Paper-compatible `Θ = (2J - 1)/(2J + 1)`
 117-/
 118
 119/-- The BRF Cayley transform used in the RH manuscripts: `Θ(J) = (2J-1)/(2J+1)`. -/
 120noncomputable def theta (J : ℂ) : ℂ :=
 121  cayley (2 * J)
 122
 123theorem norm_theta_le_one_of_re_nonneg {J : ℂ} (hJ : 0 ≤ J.re) :
 124    ‖theta J‖ ≤ 1 := by
 125  -- `Re (2J) = 2 * Re J`
 126  have : 0 ≤ (2 * J).re := by
 127    simpa using (mul_nonneg (by norm_num : (0 : ℝ) ≤ 2) hJ)
 128  simpa [theta] using (norm_cayley_le_one_of_re_nonneg (z := 2 * J) this)
 129
 130theorem re_nonneg_of_norm_theta_le_one {J : ℂ} (hJ : 2 * J ≠ (-1 : ℂ))
 131    (hθ : ‖theta J‖ ≤ 1) :
 132    0 ≤ J.re := by
 133  have : 0 ≤ (2 * J).re :=
 134    re_nonneg_of_norm_cayley_le_one (z := 2 * J) (hz := hJ) (by simpa [theta] using hθ)
 135  -- Divide by the positive constant `2`.
 136  have : 0 ≤ (2 : ℝ) * J.re := by simpa using this
 137  nlinarith
 138
 139end RiemannHypothesis
 140end NumberTheory
 141end IndisputableMonolith
 142