IndisputableMonolith.NumberTheory.ZeroCompositionLaw

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Foundation.DiscretenessForcing
   4import IndisputableMonolith.NumberTheory.ZeroLocationCost
   5import IndisputableMonolith.NumberTheory.XiJBridge
   6
   7/-!
   8# The Composition Law for Zeta Zeros
   9
  10## The Core Discovery
  11
  12The Recognition Composition Law (RCL) — the unique functional equation
  13satisfied by J(x) = ½(x + x⁻¹) − 1 — induces a **composition law on
  14zeta zero defects**.
  15
  16Given a nontrivial zero ρ of ζ(s) with deviation η = Re(ρ) − 1/2, define:
  17
  18  d₀ = J(e^{2η}) = cosh(2η) − 1
  19
  20The functional equation ξ(s) = ξ(1−s) pairs ρ with 1−ρ. Applying the
  21RCL to this pair yields a **self-composition** that amplifies defect:
  22
  23  d₁ = J(e^{4η}) = cosh(4η) − 1 = 2d₀(d₀ + 2)
  24
  25Iterating:
  26
  27  dₙ = cosh(2ⁿ⁺¹η) − 1,    dₙ₊₁ = 2dₙ(dₙ + 2)
  28
  29This is the **composition law for zeta zeros**: the RCL forces each
  30off-critical zero to generate a cascade of exponentially growing defect.
  31
  32## Main Results
  33
  341. `defectIterate_succ`: the recurrence dₙ₊₁ = 2dₙ(dₙ+2) from RCL
  352. `defectIterate_four_mul_le`: dₙ₊₁ ≥ 4dₙ (amplification)
  363. `defectIterate_exponential_lower`: dₙ ≥ 4ⁿ · d₀
  374. `defectIterate_unbounded`: off-critical zeros produce divergent defect
  38-/
  39
  40namespace IndisputableMonolith
  41namespace NumberTheory
  42
  43open Real Cost
  44
  45noncomputable section
  46
  47/-! ## §1. The iterated defect sequence -/
  48
  49/-- The iterated defect at level n: dₙ(t) = cosh(2ⁿ · t) − 1.
  50
  51    For a zeta zero with deviation η = Re(ρ)−1/2, set t = 2η.
  52    Then d₀ = cosh(2η)−1 is the zero's defect, and dₙ is the
  53    n-th iterate under the RCL self-composition. -/
  54def defectIterate (t : ℝ) (n : ℕ) : ℝ := Real.cosh ((2 : ℝ) ^ n * t) - 1
  55
  56/-- dₙ(0) = 0 for all n: on the critical line, all iterates vanish. -/
  57@[simp] theorem defectIterate_zero_param (n : ℕ) : defectIterate 0 n = 0 := by
  58  simp [defectIterate, Real.cosh_zero]
  59
  60/-- d₀(t) = cosh(t) − 1 = J_log(t). -/
  61theorem defectIterate_zero_eq_J_log (t : ℝ) :
  62    defectIterate t 0 = Foundation.DiscretenessForcing.J_log t := by
  63  simp [defectIterate, Foundation.DiscretenessForcing.J_log]
  64
  65/-- dₙ ≥ 0 for all n and t (from cosh ≥ 1). -/
  66theorem defectIterate_nonneg (t : ℝ) (n : ℕ) : 0 ≤ defectIterate t n := by
  67  simp only [defectIterate]
  68  linarith [Real.one_le_cosh ((2 : ℝ) ^ n * t)]
  69
  70/-- d₀ > 0 for t ≠ 0 (off the critical line). -/
  71theorem defectIterate_zero_pos {t : ℝ} (ht : t ≠ 0) : 0 < defectIterate t 0 := by
  72  rw [defectIterate_zero_eq_J_log]
  73  exact Foundation.DiscretenessForcing.J_log_pos ht
  74
  75/-! ## §2. The recurrence from the RCL -/
  76
  77/-- **The composition recurrence.**
  78
  79    dₙ₊₁ = 2 · dₙ · (dₙ + 2)
  80
  81    This is forced by the Recognition Composition Law: applying the
  82    RCL to the pair (e^{2ⁿt}, e^{−2ⁿt}) yields the cosh double-angle
  83    formula, which is exactly this recurrence.
  84
  85    Mathematical content:
  86      cosh(2·u) = 2cosh²(u) − 1
  87      ⟹ cosh(2u)−1 = 2(cosh u − 1)(cosh u + 1)
  88                    = 2·(cosh u − 1)·((cosh u − 1) + 2) -/
  89theorem defectIterate_succ (t : ℝ) (n : ℕ) :
  90    defectIterate t (n + 1) = 2 * defectIterate t n * (defectIterate t n + 2) := by
  91  simp only [defectIterate]
  92  rw [show (2 : ℝ) ^ (n + 1) * t = 2 * ((2 : ℝ) ^ n * t) from by rw [pow_succ]; ring]
  93  have hd := Real.cosh_two_mul ((2 : ℝ) ^ n * t)
  94  have hs := Real.cosh_sq ((2 : ℝ) ^ n * t)
  95  set c := Real.cosh ((2 : ℝ) ^ n * t)
  96  set s := Real.sinh ((2 : ℝ) ^ n * t)
  97  have lhs : Real.cosh (2 * ((2 : ℝ) ^ n * t)) - 1 = 2 * c ^ 2 - 2 := by linarith
  98  have rhs_eq : 2 * (c - 1) * (c - 1 + 2) = 2 * c ^ 2 - 2 := by ring
  99  linarith
 100
 101/-- The recurrence in "squared ratio" form:
 102    dₙ₊₁ = 2(dₙ² + 2dₙ) = 2dₙ² + 4dₙ. -/
 103theorem defectIterate_succ' (t : ℝ) (n : ℕ) :
 104    defectIterate t (n + 1) = 2 * (defectIterate t n) ^ 2 + 4 * defectIterate t n := by
 105  rw [defectIterate_succ]; ring
 106
 107/-! ## §3. Defect amplification -/
 108
 109/-- **Each iteration at least quadruples the defect.**
 110    dₙ₊₁ ≥ 4·dₙ  (from dₙ ≥ 0 ⟹ dₙ+2 ≥ 2). -/
 111theorem defectIterate_four_mul_le (t : ℝ) (n : ℕ) :
 112    4 * defectIterate t n ≤ defectIterate t (n + 1) := by
 113  rw [defectIterate_succ]
 114  have hd : 0 ≤ defectIterate t n := defectIterate_nonneg t n
 115  nlinarith [sq_nonneg (defectIterate t n)]
 116
 117/-- **Exponential lower bound.** dₙ ≥ 4ⁿ · d₀.
 118
 119    Each iteration quadruples the defect, so after n iterations
 120    the defect has grown by a factor of at least 4ⁿ. -/
 121theorem defectIterate_exponential_lower (t : ℝ) (n : ℕ) :
 122    (4 : ℝ) ^ n * defectIterate t 0 ≤ defectIterate t n := by
 123  induction n with
 124  | zero => simp
 125  | succ n ih =>
 126    calc (4 : ℝ) ^ (n + 1) * defectIterate t 0
 127        = 4 * ((4 : ℝ) ^ n * defectIterate t 0) := by ring
 128      _ ≤ 4 * defectIterate t n := by nlinarith
 129      _ ≤ defectIterate t (n + 1) := defectIterate_four_mul_le t n
 130
 131/-- 1 ≤ 4^n for all n. -/
 132private theorem one_le_four_pow (n : ℕ) : (1 : ℝ) ≤ (4 : ℝ) ^ n := by
 133  induction n with
 134  | zero => simp
 135  | succ k ih =>
 136    rw [pow_succ]
 137    nlinarith [pow_nonneg (show (0:ℝ) ≤ 4 from by norm_num) k]
 138
 139/-- The sequence is monotonically nondecreasing from level 0. -/
 140theorem defectIterate_mono {t : ℝ} (ht : t ≠ 0) (n : ℕ) :
 141    defectIterate t 0 ≤ defectIterate t n := by
 142  have h := defectIterate_exponential_lower t n
 143  have hd0 : 0 < defectIterate t 0 := defectIterate_zero_pos ht
 144  nlinarith [one_le_four_pow n]
 145
 146/-! ## §4. Divergence -/
 147
 148/-- Helper: n+1 ≤ 4^(n+1) for all n. -/
 149private theorem nat_succ_le_pow_four (m : ℕ) : (m : ℝ) + 1 ≤ (4 : ℝ) ^ (m + 1) := by
 150  induction m with
 151  | zero => norm_num
 152  | succ k ih =>
 153    rw [pow_succ]; push_cast
 154    nlinarith [pow_nonneg (show (0:ℝ) ≤ 4 from by norm_num) (k + 1)]
 155
 156/-- **Off-critical zeros produce divergent defect cascades.**
 157
 158    For any t ≠ 0 (deviation from critical line), the iterated defect
 159    sequence grows without bound. This is the key obstruction: the RCL
 160    forces an off-critical zero to generate unbounded cost, which cannot
 161    be accommodated by any finite carrier budget.
 162
 163    Proof: dₙ ≥ 4ⁿ · d₀ with d₀ > 0, and 4ⁿ → ∞. -/
 164theorem defectIterate_unbounded {t : ℝ} (ht : t ≠ 0) (C : ℝ) :
 165    ∃ n : ℕ, C < defectIterate t n := by
 166  have hd0 : 0 < defectIterate t 0 := defectIterate_zero_pos ht
 167  have hexp := defectIterate_exponential_lower t
 168  suffices h : ∃ n : ℕ, C < (4 : ℝ) ^ n * defectIterate t 0 by
 169    obtain ⟨n, hn⟩ := h
 170    exact ⟨n, lt_of_lt_of_le hn (hexp n)⟩
 171  set k := ⌈C / defectIterate t 0⌉₊ + 1
 172  refine ⟨k, ?_⟩
 173  have h1 : C / defectIterate t 0 ≤ ↑(⌈C / defectIterate t 0⌉₊) := Nat.le_ceil _
 174  have h2 : (↑(⌈C / defectIterate t 0⌉₊) : ℝ) + 1 ≤ (4 : ℝ) ^ k :=
 175    nat_succ_le_pow_four _
 176  rw [show C = C / defectIterate t 0 * defectIterate t 0 from by
 177    field_simp]
 178  exact mul_lt_mul_of_pos_right (by linarith) hd0
 179
 180/-! ## §5. Connection to the zero-location defect -/
 181
 182/-- For a zeta zero ρ, the iterated defect at level 0 equals the
 183    zero-location defect from ZeroLocationCost. -/
 184theorem defectIterate_zero_eq_zeroDefect (ρ : ℂ) :
 185    defectIterate (zeroDeviation ρ) 0 = zeroDefect ρ := by
 186  rw [defectIterate_zero_eq_J_log, zeroDefect_eq_J_log]
 187
 188/-- **The composition law for zeta zeros, final form.**
 189
 190    If ρ is off the critical line, the iterated composition defect
 191    diverges, generating arbitrarily large cost values from a single zero. -/
 192theorem zero_composition_diverges (ρ : ℂ) (hρ : ¬OnCriticalLine ρ) (C : ℝ) :
 193    ∃ n : ℕ, C < defectIterate (zeroDeviation ρ) n := by
 194  apply defectIterate_unbounded
 195  exact (zeroDeviation_eq_zero_iff_on_critical_line ρ).not.mpr hρ
 196
 197end
 198
 199end NumberTheory
 200end IndisputableMonolith
 201