IndisputableMonolith.Cost.Ndim.RicciScalar

   1import IndisputableMonolith.Cost.Ndim.Core
   2
   3/-!
   4# Ricci scalar equivalence for the 2D cost Hessian metric
   5
   6The Levi-Civita connection on M_x (the Hessian manifold in positive
   7coordinates) has Ricci scalar curvature expressed two ways:
   8
   9* **Z-form** (Section 4.5): rational in Z = x^{2a} y^{2b},
  10* **q-form** (Eq. 4.26): hyperbolic in q = a s + b t.
  11
  12Under Z = e^{2q}, the identities coth q = (Z+1)/(Z−1) and
  13csch q = 2 Z^{1/2}/(Z−1) convert one into the other.
  14
  15We prove the algebraic equivalence by reducing both to a common
  16rational form in w = exp q, then closing with `field_simp` + `ring`.
  17
  18Reference: "Multidimensional Cost Geometry", Washburn–Zlatanović–Beltracchi,
  19Sections 4.5 and 4.6.2.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Cost
  24namespace Ndim
  25
  26noncomputable section
  27
  28/-- The Ricci scalar in (q, r)-coordinates, Eq. (4.26).
  29    Written with sinh/cosh to avoid coth/csch. -/
  30def ricciQ (a b q : ℝ) : ℝ :=
  31  (a + b) * ((a + b) * Real.cosh q - 2 * Real.sinh q) /
  32    (2 * (Real.sinh q) ^ 2 * ((a + b) * Real.cosh q - Real.sinh q) ^ 2)
  33
  34/-- The Ricci scalar in (x, y)-coordinates (Section 4.5),
  35    parametrised by q via Z = exp(2q), Z^{3/2} = exp(3q). -/
  36def ricciZexp (a b q : ℝ) : ℝ :=
  37  let Z := Real.exp (2 * q)
  38  4 * (a + b) * Real.exp (3 * q) *
  39    ((a + b - 2) * Z + (a + b + 2)) /
  40    ((Z - 1) ^ 2 * ((a + b - 1) * Z + (a + b + 1)) ^ 2)
  41
  42/-- Canonical rational form of the Ricci scalar in w = exp q. -/
  43def ricciW (a b w : ℝ) : ℝ :=
  44  4 * (a + b) * w ^ 3 *
  45    ((a + b - 2) * w ^ 2 + (a + b + 2)) /
  46    ((w ^ 2 - 1) ^ 2 * ((a + b - 1) * w ^ 2 + (a + b + 1)) ^ 2)
  47
  48private theorem exp_two_mul (q : ℝ) :
  49    Real.exp (2 * q) = (Real.exp q) ^ 2 := by
  50  rw [show (2 : ℝ) * q = q + q from by ring, Real.exp_add]; ring
  51
  52private theorem exp_three_mul (q : ℝ) :
  53    Real.exp (3 * q) = (Real.exp q) ^ 3 := by
  54  rw [show (3 : ℝ) * q = q + (q + q) from by ring, Real.exp_add, Real.exp_add]; ring
  55
  56/-- The Z-form is `ricciW` evaluated at w = exp q. -/
  57theorem ricciZexp_eq_ricciW (a b q : ℝ) :
  58    ricciZexp a b q = ricciW a b (Real.exp q) := by
  59  unfold ricciZexp ricciW; rw [exp_two_mul, exp_three_mul]
  60
  61/-- The q-form is also `ricciW` at w = exp q. -/
  62theorem ricciQ_eq_ricciW (a b q : ℝ)
  63    (hq : q ≠ 0)
  64    (hLC : (a + b) * Real.cosh q - Real.sinh q ≠ 0) :
  65    ricciQ a b q = ricciW a b (Real.exp q) := by
  66  set w := Real.exp q with hw_def
  67  have hw_pos : 0 < w := Real.exp_pos q
  68  have hw_ne : w ≠ 0 := hw_pos.ne'
  69  have hsinh_ne : Real.sinh q ≠ 0 := Real.sinh_ne_zero.mpr hq
  70  have hcosh_w : Real.cosh q = (w ^ 2 + 1) / (2 * w) := by
  71    rw [Real.cosh_eq, Real.exp_neg]; field_simp; ring
  72  have hsinh_w : Real.sinh q = (w ^ 2 - 1) / (2 * w) := by
  73    rw [Real.sinh_eq, Real.exp_neg]; field_simp; ring
  74  have hw2m1 : w ^ 2 - 1 ≠ 0 := by
  75    intro h; exact hsinh_ne (by rw [hsinh_w, h, zero_div])
  76  have hLCw : (a + b - 1) * w ^ 2 + (a + b + 1) ≠ 0 := by
  77    intro h; apply hLC; rw [hcosh_w, hsinh_w]; field_simp; linarith
  78  show ricciQ a b q = ricciW a b w
  79  unfold ricciQ ricciW
  80  rw [hcosh_w, hsinh_w]
  81  field_simp [hw_ne, hw2m1, hLCw]
  82  ring
  83
  84/-- **Main result**: the two coordinate forms of the Ricci scalar agree. -/
  85theorem ricci_scalar_equiv (a b q : ℝ)
  86    (hq : q ≠ 0)
  87    (hLC : (a + b) * Real.cosh q - Real.sinh q ≠ 0) :
  88    ricciQ a b q = ricciZexp a b q := by
  89  rw [ricciQ_eq_ricciW a b q hq hLC, ricciZexp_eq_ricciW]
  90
  91end
  92
  93end Ndim
  94end Cost
  95end IndisputableMonolith
  96