IndisputableMonolith.Cost.RealTraceRoot

   1/-
   2# Principal branch of the doubled-trace root
   3
   4Algebraic core for real-valued character extraction. A doubled trace `t ≥ 2`
   5has principal root `realTraceRoot t = (t + √(t² − 4))/2 ≥ 1`, recovering the
   6character value whose trace is `t`. Under the cosh-addition formula the branch
   7multiplies. Mathlib only; no PRC imports.
   8-/
   9
  10import Mathlib
  11
  12namespace IndisputableMonolith
  13namespace Cost
  14namespace RealTraceRoot
  15
  16/-- The principal (≥ 1) root of `X² - t X + 1 = 0`, for `t ≥ 2`. -/
  17noncomputable def realTraceRoot (t : ℝ) : ℝ :=
  18  (t + Real.sqrt (t ^ 2 - 4)) / 2
  19
  20theorem realTraceRoot_sq_sub_four_nonneg {t : ℝ} (ht : 2 ≤ t) :
  21    0 ≤ t ^ 2 - 4 := by nlinarith
  22
  23theorem realTraceRoot_one : realTraceRoot 2 = 1 := by
  24  simp [realTraceRoot, show (2 : ℝ) ^ 2 - 4 = 0 by norm_num, Real.sqrt_zero]
  25
  26theorem realTraceRoot_ge_one {t : ℝ} (ht : 2 ≤ t) : 1 ≤ realTraceRoot t := by
  27  have hs : 0 ≤ Real.sqrt (t ^ 2 - 4) := Real.sqrt_nonneg _
  28  simp only [realTraceRoot]
  29  linarith
  30
  31theorem realTraceRoot_pos {t : ℝ} (ht : 2 ≤ t) : 0 < realTraceRoot t :=
  32  lt_of_lt_of_le zero_lt_one (realTraceRoot_ge_one ht)
  33
  34theorem realTraceRoot_add_inv {t : ℝ} (ht : 2 ≤ t) :
  35    realTraceRoot t + (realTraceRoot t)⁻¹ = t := by
  36  have hsq : Real.sqrt (t ^ 2 - 4) ^ 2 = t ^ 2 - 4 :=
  37    Real.sq_sqrt (realTraceRoot_sq_sub_four_nonneg ht)
  38  have hne : realTraceRoot t ≠ 0 := ne_of_gt (realTraceRoot_pos ht)
  39  have hinv : (realTraceRoot t)⁻¹ = (t - Real.sqrt (t ^ 2 - 4)) / 2 := by
  40    have hprod :
  41        realTraceRoot t * ((t - Real.sqrt (t ^ 2 - 4)) / 2) = 1 := by
  42      simp only [realTraceRoot]
  43      field_simp
  44      nlinarith [hsq]
  45    have := congrArg (fun z : ℝ => z / realTraceRoot t) hprod
  46    field_simp [hne] at this ⊢
  47    linarith
  48  rw [hinv]
  49  simp only [realTraceRoot]
  50  ring
  51
  52/-- **Multiplication of principal branches.** If `a, b ≥ 2` and
  53`u = (a b + √(a²−4)√(b²−4))/2`, then
  54`realTraceRoot u = realTraceRoot a * realTraceRoot b`. -/
  55theorem realTraceRoot_mul {a b : ℝ} (ha : 2 ≤ a) (hb : 2 ≤ b) :
  56    realTraceRoot ((a * b + Real.sqrt (a ^ 2 - 4) * Real.sqrt (b ^ 2 - 4)) / 2) =
  57      realTraceRoot a * realTraceRoot b := by
  58  set sa := Real.sqrt (a ^ 2 - 4)
  59  set sb := Real.sqrt (b ^ 2 - 4)
  60  have hsa : 0 ≤ sa := Real.sqrt_nonneg _
  61  have hsb : 0 ≤ sb := Real.sqrt_nonneg _
  62  have hsqa : sa ^ 2 = a ^ 2 - 4 := by
  63    simpa [sa] using Real.sq_sqrt (realTraceRoot_sq_sub_four_nonneg ha)
  64  have hsqb : sb ^ 2 = b ^ 2 - 4 := by
  65    simpa [sb] using Real.sq_sqrt (realTraceRoot_sq_sub_four_nonneg hb)
  66  set u := (a * b + sa * sb) / 2
  67  -- √(u² − 4) = (a sb + b sa) / 2
  68  have hdisc : u ^ 2 - 4 = ((a * sb + b * sa) / 2) ^ 2 := by
  69    have h : 4 * (u ^ 2 - 4) = (a * sb + b * sa) ^ 2 := by
  70      simp only [u]
  71      nlinarith [hsqa, hsqb]
  72    have h4 : (4 : ℝ) ≠ 0 := by norm_num
  73    calc
  74      u ^ 2 - 4 = (4 * (u ^ 2 - 4)) / 4 := by ring
  75      _ = (a * sb + b * sa) ^ 2 / 4 := by rw [h]
  76      _ = ((a * sb + b * sa) / 2) ^ 2 := by ring
  77  have hsqrt : Real.sqrt (u ^ 2 - 4) = (a * sb + b * sa) / 2 := by
  78    have hnn : 0 ≤ (a * sb + b * sa) / 2 := by positivity
  79    rw [hdisc]
  80    exact Real.sqrt_sq hnn
  81  -- both sides equal (ab + a sb + b sa + sa sb) / 4
  82  simp only [realTraceRoot, hsqrt, u, sa, sb]
  83  field_simp
  84  ring
  85
  86/-- Given `u + v = a b` and `(u - v)² = (a²−4)(b²−4)` with `v ≤ u`, the larger
  87trace is the cosh-addition value. -/
  88theorem larger_trace_of_diff_sq {a b u v : ℝ}
  89    (ha : 2 ≤ a) (hb : 2 ≤ b)
  90    (hsum : u + v = a * b)
  91    (hdiffsq : (u - v) ^ 2 = (a ^ 2 - 4) * (b ^ 2 - 4))
  92    (hulev : v ≤ u) :
  93    u = (a * b + Real.sqrt (a ^ 2 - 4) * Real.sqrt (b ^ 2 - 4)) / 2 := by
  94  have hnonnega : 0 ≤ a ^ 2 - 4 := realTraceRoot_sq_sub_four_nonneg ha
  95  have hprod_sqrt :
  96      Real.sqrt ((a ^ 2 - 4) * (b ^ 2 - 4)) =
  97        Real.sqrt (a ^ 2 - 4) * Real.sqrt (b ^ 2 - 4) :=
  98    Real.sqrt_mul hnonnega (b ^ 2 - 4)
  99  have huv : u - v = Real.sqrt (a ^ 2 - 4) * Real.sqrt (b ^ 2 - 4) := by
 100    have := congrArg Real.sqrt hdiffsq
 101    rwa [Real.sqrt_sq (sub_nonneg.mpr hulev), hprod_sqrt] at this
 102  linarith
 103
 104/-! ## Multiplicative d'Alembert algebra (doubled-trace units)
 105
 106Pure algebra for `g (x*y) + g (x/y) = 2 * g x * g y` with `g 1 = 1`, and the
 107trace form `T (x*y) + T (x/y) = T x * T y` with `T 1 = 2` via `g = T/2`. -/
 108
 109/-- **Multiplicative duplication.** From the product law at `(x, x)` with `g 1 = 1`. -/
 110theorem mulDAlembert_duplication {g : ℝ → ℝ}
 111    (hd : ∀ x y, x ≠ 0 → y ≠ 0 → g (x * y) + g (x / y) = 2 * g x * g y)
 112    (h1 : g 1 = 1) :
 113    ∀ x, x ≠ 0 → g (x * x) = 2 * (g x) ^ 2 - 1 := by
 114  intro x hx
 115  have h := hd x x hx hx
 116  rw [div_self hx, h1] at h
 117  linarith
 118
 119/-- **Product identity.** Apply the law to arguments `(x*y)` and `(x/y)`. -/
 120theorem mulDAlembert_prod {g : ℝ → ℝ}
 121    (hd : ∀ x y, x ≠ 0 → y ≠ 0 → g (x * y) + g (x / y) = 2 * g x * g y) :
 122    ∀ x y, x ≠ 0 → y ≠ 0 →
 123      g (x * x) + g (y * y) = 2 * g (x * y) * g (x / y) := by
 124  intro x y hx hy
 125  have hxy : x * y ≠ 0 := mul_ne_zero hx hy
 126  have hxdy : x / y ≠ 0 := div_ne_zero hx hy
 127  have h := hd (x * y) (x / y) hxy hxdy
 128  have hprod : (x * y) * (x / y) = x * x := by field_simp [hy]
 129  have hquot : (x * y) / (x / y) = y * y := by field_simp [hy]
 130  rw [hprod, hquot] at h
 131  linarith
 132
 133/-- **Difference square.** Sum law, product identity, and duplication on `x`, `y`. -/
 134theorem mulDAlembert_diff_sq {g : ℝ → ℝ}
 135    (hd : ∀ x y, x ≠ 0 → y ≠ 0 → g (x * y) + g (x / y) = 2 * g x * g y)
 136    (h1 : g 1 = 1) :
 137    ∀ x y, x ≠ 0 → y ≠ 0 →
 138      (g (x * y) - g (x / y)) ^ 2
 139        = 4 * ((g x) ^ 2 - 1) * ((g y) ^ 2 - 1) := by
 140  intro x y hx hy
 141  have hsum := hd x y hx hy
 142  have hprod := mulDAlembert_prod hd x y hx hy
 143  have hdx := mulDAlembert_duplication hd h1 x hx
 144  have hdy := mulDAlembert_duplication hd h1 y hy
 145  rw [hdx, hdy] at hprod
 146  have expand : (g (x * y) - g (x / y)) ^ 2
 147      = (g (x * y) + g (x / y)) ^ 2 - 2 * (2 * g (x * y) * g (x / y)) := by ring
 148  rw [expand, hsum, ← hprod]
 149  ring
 150
 151/-- **Difference square in doubled-trace units** (`T 1 = 2`, reduce via `g = T/2`). -/
 152theorem mulDAlembert_diff_sq_trace {T : ℝ → ℝ}
 153    (hd : ∀ x y, x ≠ 0 → y ≠ 0 → T (x * y) + T (x / y) = T x * T y)
 154    (h2 : T 1 = 2) :
 155    ∀ x y, x ≠ 0 → y ≠ 0 →
 156      (T (x * y) - T (x / y)) ^ 2
 157        = (T x ^ 2 - 4) * (T y ^ 2 - 4) := by
 158  intro x y hx hy
 159  set g := fun z => T z / 2
 160  have hg :
 161      ∀ u v, u ≠ 0 → v ≠ 0 → g (u * v) + g (u / v) = 2 * g u * g v := by
 162    intro u v hu hv
 163    simp only [g]
 164    have := hd u v hu hv
 165    field_simp
 166    linarith
 167  have hg1 : g 1 = 1 := by simp [g, h2]
 168  have hsq := mulDAlembert_diff_sq hg hg1 x y hx hy
 169  simp only [g] at hsq
 170  have hl : (T (x * y) / 2 - T (x / y) / 2) ^ 2
 171      = (T (x * y) - T (x / y)) ^ 2 / 4 := by ring
 172  have hr : 4 * ((T x / 2) ^ 2 - 1) * ((T y / 2) ^ 2 - 1)
 173      = (T x ^ 2 - 4) * (T y ^ 2 - 4) / 4 := by ring
 174  rw [hl, hr] at hsq
 175  have h4 : (4 : ℝ) ≠ 0 := by norm_num
 176  field_simp at hsq
 177  exact hsq
 178
 179#print axioms realTraceRoot_mul
 180#print axioms realTraceRoot_add_inv
 181#print axioms larger_trace_of_diff_sq
 182#print axioms mulDAlembert_duplication
 183#print axioms mulDAlembert_prod
 184#print axioms mulDAlembert_diff_sq
 185#print axioms mulDAlembert_diff_sq_trace
 186
 187end RealTraceRoot
 188end Cost
 189end IndisputableMonolith
 190