IndisputableMonolith.Cost.Ndim.Connections

   1import IndisputableMonolith.Cost.Ndim.Core
   2
   3/-!
   4# Affine connections in `x`- and `t`-coordinates
   5
   6The `t = log x` coordinates are affine-flat by construction. When pulled back
   7to `x`-coordinates, the same flat connection acquires the familiar diagonal
   8Christoffel term `Γⁱ_{ii} = -1 / xᵢ`.
   9
  10This module records those coefficient formulas and proves the basic projective
  11equivalence dichotomy: the one-dimensional case is projectively equivalent to
  12the zero connection, while in dimensions `n ≥ 2` this fails.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Cost
  17namespace Ndim
  18
  19/-- The Kronecker delta on `Fin n`. -/
  20def delta {n : ℕ} (i j : Fin n) : ℝ :=
  21  if i = j then 1 else 0
  22
  23/-- The flat affine connection in `x`-coordinates. -/
  24def xFlatConnection {n : ℕ} (_x : Vec n) (_i _j _k : Fin n) : ℝ := 0
  25
  26/-- The flat `t`-connection pulled back through `tᵢ = log xᵢ`. -/
  27noncomputable def tPulledConnection {n : ℕ} (x : Vec n) (i j k : Fin n) : ℝ :=
  28  if i = j ∧ j = k then -(x i)⁻¹ else 0
  29
  30/-- Projective equivalence to the zero connection. -/
  31def ProjectivelyEquivalentToZeroAt {n : ℕ}
  32    (Γ : Fin n → Fin n → Fin n → ℝ) : Prop :=
  33  ∃ ψ : Vec n, ∀ i j k : Fin n,
  34    Γ i j k = delta i j * ψ k + delta i k * ψ j
  35
  36@[simp] theorem xFlatConnection_apply {n : ℕ} (x : Vec n) (i j k : Fin n) :
  37    xFlatConnection x i j k = 0 := rfl
  38
  39theorem tPulledConnection_diag {n : ℕ} (x : Vec n) (i : Fin n) :
  40    tPulledConnection x i i i = -(x i)⁻¹ := by
  41  unfold tPulledConnection
  42  simp
  43
  44theorem tPulledConnection_offDiag {n : ℕ} (x : Vec n) {i j k : Fin n}
  45    (hijk : ¬ (i = j ∧ j = k)) :
  46    tPulledConnection x i j k = 0 := by
  47  unfold tPulledConnection
  48  simp [hijk]
  49
  50theorem projectivelyEquivalent_one_dim {x : Vec 1} :
  51    ProjectivelyEquivalentToZeroAt (tPulledConnection x) := by
  52  refine ⟨fun _ => -((x 0)⁻¹) / 2, ?_⟩
  53  intro i j k
  54  fin_cases i
  55  fin_cases j
  56  fin_cases k
  57  simp [delta, tPulledConnection]
  58
  59theorem not_projectivelyEquivalentToZeroAt_tPulledConnection {n : ℕ}
  60    (hn : 2 ≤ n) (x : Vec n) (hx : ∀ i : Fin n, x i ≠ 0) :
  61    ¬ ProjectivelyEquivalentToZeroAt (tPulledConnection x) := by
  62  let i0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hn⟩
  63  let i1 : Fin n := ⟨1, lt_of_lt_of_le (by decide : 1 < 2) hn⟩
  64  have hi01 : i0 ≠ i1 := by
  65    simp [i0, i1]
  66  intro hproj
  67  rcases hproj with ⟨ψ, hψ⟩
  68  have hpsi1 : ψ i1 = 0 := by
  69    have h := hψ i0 i0 i1
  70    simpa [eq_comm, delta, tPulledConnection, hi01] using h
  71  have hdiag : tPulledConnection x i1 i1 i1 = delta i1 i1 * ψ i1 + delta i1 i1 * ψ i1 := by
  72    simpa using hψ i1 i1 i1
  73  have hxinv_zero : (x i1)⁻¹ = 0 := by
  74    have h' : -(x i1)⁻¹ = 0 := by
  75      simpa [delta, tPulledConnection, hpsi1] using hdiag
  76    exact neg_eq_zero.mp h'
  77  exact (inv_ne_zero (hx i1)) hxinv_zero
  78
  79end Ndim
  80end Cost
  81end IndisputableMonolith
  82