IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D

   1import Mathlib
   2
   3/-!
   4# Edge TT decomposition (4D), algebraic layer
   5
   6QG full-theory campaign, Wave 4 / lane W4-1 (`edge_tt_decomposition`),
   7smallest kernel-checked increment: the **linear-algebra** transverse-traceless
   8decomposition of symmetric `4 × 4` real matrices against a nonzero Euclidean
   9wave covector on `Fin 4`.
  10
  11## Tier tags (binding)
  12
  13* THEOREM: every named result in this file (kernel-checked; no `sorry`, no
  14  `admit`, no new axioms, no `native_decide`, no `: True` shells).
  15* This is the algebraic layer of the ledger closing name
  16  `edge_tt_decomposition`.  It does **not** decompose Regge EDGE
  17  perturbations on a 4D lattice, does **not** prove `S_RS_converges_EH_4d`,
  18  and does **not** flip `gap_action_recovery`.
  19
  20## Conventions (inherited from 3D `IsTTPolarization`)
  21
  22The 3D closer chain uses Euclidean trace, Euclidean transversality, and
  23symmetry.  This module lifts those three conjuncts to `Fin 4` (no Frobenius
  24pin).  Minkowski/null specialization for the Lorentzian continuum is
  25deferred; "two polarizations in 4D" is an explicit independent TT pair on
  26the axis wave vector (unnormalized integer entries).
  27
  28Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Gravity
  33namespace Analysis
  34namespace EdgeTTDecomposition4D
  35
  36open Matrix BigOperators
  37
  38noncomputable section
  39
  40abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
  41
  42def IsSymmetric (H : Mat4) : Prop :=
  43  ∀ i j : Fin 4, H i j = H j i
  44
  45def euclideanTrace (H : Mat4) : ℝ :=
  46  ∑ i : Fin 4, H i i
  47
  48def IsTraceless (H : Mat4) : Prop :=
  49  euclideanTrace H = 0
  50
  51def IsTransverse (m : Fin 4 → ℝ) (H : Mat4) : Prop :=
  52  ∀ i : Fin 4, ∑ j : Fin 4, H i j * m j = 0
  53
  54/-- Algebraic TT: symmetric, Euclidean-traceless, transverse. -/
  55def IsTT (m : Fin 4 → ℝ) (H : Mat4) : Prop :=
  56  IsSymmetric H ∧ IsTraceless H ∧ IsTransverse m H
  57
  58def momentumSq (m : Fin 4 → ℝ) : ℝ :=
  59  ∑ i : Fin 4, m i * m i
  60
  61def gaugePart (m v : Fin 4 → ℝ) : Mat4 :=
  62  fun i j => m i * v j + v i * m j
  63
  64def outerSq (m : Fin 4 → ℝ) : Mat4 :=
  65  fun i j => m i * m j
  66
  67def transverseProjector (m : Fin 4 → ℝ) : Mat4 :=
  68  (1 : Mat4) - (momentumSq m)⁻¹ • outerSq m
  69
  70def load (H : Mat4) (m : Fin 4 → ℝ) : Fin 4 → ℝ :=
  71  fun i => ∑ j : Fin 4, H i j * m j
  72
  73def dot (a b : Fin 4 → ℝ) : ℝ :=
  74  ∑ i : Fin 4, a i * b i
  75
  76def gaugeVector (m : Fin 4 → ℝ) (H : Mat4) : Fin 4 → ℝ :=
  77  fun i =>
  78    let w := load H m
  79    let s := momentumSq m
  80    w i / s - m i * dot w m / (2 * s ^ 2)
  81
  82def gaugeCorrected (m : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
  83  H - gaugePart m (gaugeVector m H)
  84
  85def residualTrace (m : Fin 4 → ℝ) (H : Mat4) : ℝ :=
  86  euclideanTrace (gaugeCorrected m H) / 3
  87
  88def ttProject (m : Fin 4 → ℝ) (H : Mat4) : Mat4 :=
  89  gaugeCorrected m H - residualTrace m H • transverseProjector m
  90
  91/-! ## §1. Elementary identities -/
  92
  93theorem gaugePart_symmetric (m v : Fin 4 → ℝ) :
  94    IsSymmetric (gaugePart m v) := by
  95  intro i j; unfold gaugePart; ring
  96
  97theorem outerSq_symmetric (m : Fin 4 → ℝ) :
  98    IsSymmetric (outerSq m) := by
  99  intro i j; unfold outerSq; ring
 100
 101theorem transverseProjector_symmetric (m : Fin 4 → ℝ) :
 102    IsSymmetric (transverseProjector m) := by
 103  intro i j
 104  unfold transverseProjector
 105  simp only [sub_apply, smul_apply, smul_eq_mul, one_apply]
 106  rw [outerSq_symmetric m i j]
 107  cases' eq_or_ne i j with hij hij
 108  · subst hij; rfl
 109  · rw [if_neg hij, if_neg (Ne.symm hij)]
 110
 111theorem load_gaugePart (m v : Fin 4 → ℝ) (i : Fin 4) :
 112    load (gaugePart m v) m i =
 113      momentumSq m * v i + m i * dot v m := by
 114  unfold load gaugePart momentumSq dot
 115  calc
 116    ∑ j : Fin 4, (m i * v j + v i * m j) * m j
 117        = ∑ j : Fin 4, (m i * (v j * m j) + v i * (m j * m j)) := by
 118      refine Finset.sum_congr rfl fun j _ => by ring
 119    _ = (∑ j : Fin 4, m i * (v j * m j)) +
 120          (∑ j : Fin 4, v i * (m j * m j)) := Finset.sum_add_distrib
 121    _ = m i * ∑ j : Fin 4, v j * m j + v i * ∑ j : Fin 4, m j * m j := by
 122      simp [Finset.mul_sum]
 123    _ = (∑ j : Fin 4, m j * m j) * v i + m i * ∑ j : Fin 4, v j * m j := by
 124      ring
 125
 126theorem load_smul (c : ℝ) (H : Mat4) (m : Fin 4 → ℝ) (i : Fin 4) :
 127    load (c • H) m i = c * load H m i := by
 128  unfold load
 129  simp only [smul_apply, smul_eq_mul, mul_assoc]
 130  exact (Finset.mul_sum Finset.univ (fun j => H i j * m j) c).symm
 131
 132theorem load_sub (A B : Mat4) (m : Fin 4 → ℝ) (i : Fin 4) :
 133    load (A - B) m i = load A m i - load B m i := by
 134  unfold load; simp [sub_mul, Finset.sum_sub_distrib]
 135
 136theorem load_one (m : Fin 4 → ℝ) (i : Fin 4) :
 137    load (1 : Mat4) m i = m i := by
 138  unfold load
 139  simp only [one_apply]
 140  rw [Finset.sum_eq_single (a := i)]
 141  · simp
 142  · intro j _ hj
 143    simp [Ne.symm hj]
 144  · intro hi
 145    exact (hi (Finset.mem_univ i)).elim
 146
 147theorem load_outerSq (m : Fin 4 → ℝ) (i : Fin 4) :
 148    load (outerSq m) m i = momentumSq m * m i := by
 149  unfold load outerSq momentumSq
 150  calc
 151    ∑ j : Fin 4, (m i * m j) * m j
 152        = m i * ∑ j : Fin 4, m j * m j := by
 153      simp [mul_assoc, Finset.mul_sum]
 154    _ = (∑ j : Fin 4, m j * m j) * m i := by ring
 155
 156theorem load_transverseProjector (m : Fin 4 → ℝ) (hm : momentumSq m ≠ 0)
 157    (i : Fin 4) :
 158    load (transverseProjector m) m i = 0 := by
 159  unfold transverseProjector
 160  rw [load_sub, load_one, load_smul, load_outerSq]
 161  field_simp [hm]; ring
 162
 163/-! ## §2. Gauge removal -/
 164
 165theorem dot_gaugeVector (m : Fin 4 → ℝ) (H : Mat4)
 166    (hm : momentumSq m ≠ 0) :
 167    dot (gaugeVector m H) m = dot (load H m) m / (2 * momentumSq m) := by
 168  set w := load H m with hw
 169  set s := momentumSq m with hs
 170  have hs0 : s ≠ 0 := hm
 171  set d := dot w m with hd
 172  -- expand
 173  have hexpand :
 174      dot (gaugeVector m H) m =
 175        ∑ i : Fin 4, (w i / s - m i * d / (2 * s ^ 2)) * m i := by
 176    simp [dot, gaugeVector, w, s, d]
 177  have hsplit :
 178      ∑ i : Fin 4, (w i / s - m i * d / (2 * s ^ 2)) * m i =
 179        ∑ i : Fin 4, (w i / s) * m i -
 180          ∑ i : Fin 4, (m i * d / (2 * s ^ 2)) * m i := by
 181    simp [sub_mul, Finset.sum_sub_distrib]
 182  have h1 : ∑ i : Fin 4, (w i / s) * m i = d / s := by
 183    simp only [d, dot, div_eq_mul_inv, mul_assoc]
 184    -- ∑ (s⁻¹ * wᵢ) * mᵢ = s⁻¹ * ∑ wᵢ mᵢ
 185    have :
 186        ∑ i : Fin 4, s⁻¹ * w i * m i = s⁻¹ * ∑ i : Fin 4, w i * m i := by
 187      simp [mul_assoc, ← Finset.mul_sum]
 188    convert this using 1
 189    · refine Finset.sum_congr rfl fun i _ => by ring
 190    · ring
 191  have h2 : ∑ i : Fin 4, (m i * d / (2 * s ^ 2)) * m i = s * d / (2 * s ^ 2) := by
 192    have :
 193        ∑ i : Fin 4, m i * m i * (d / (2 * s ^ 2)) =
 194          (∑ i : Fin 4, m i * m i) * (d / (2 * s ^ 2)) :=
 195      (Finset.sum_mul _ _ _).symm
 196    calc
 197      ∑ i : Fin 4, (m i * d / (2 * s ^ 2)) * m i
 198          = ∑ i : Fin 4, m i * m i * (d / (2 * s ^ 2)) := by
 199        refine Finset.sum_congr rfl fun i _ => by ring
 200      _ = (∑ i : Fin 4, m i * m i) * (d / (2 * s ^ 2)) := this
 201      _ = s * d / (2 * s ^ 2) := by
 202        simp [s, momentumSq]; ring
 203  calc
 204    dot (gaugeVector m H) m
 205        = ∑ i : Fin 4, (w i / s - m i * d / (2 * s ^ 2)) * m i := hexpand
 206    _ = d / s - s * d / (2 * s ^ 2) := by rw [hsplit, h1, h2]
 207    _ = d / (2 * s) := by field_simp [hs0]; ring
 208    _ = dot (load H m) m / (2 * momentumSq m) := by
 209        simp [d, w, s]
 210
 211theorem load_gaugePart_gaugeVector (m : Fin 4 → ℝ) (H : Mat4)
 212    (hm : momentumSq m ≠ 0) (i : Fin 4) :
 213    load (gaugePart m (gaugeVector m H)) m i = load H m i := by
 214  set w := load H m
 215  set s := momentumSq m
 216  set v := gaugeVector m H
 217  have hs0 : s ≠ 0 := hm
 218  have hL := load_gaugePart m v i
 219  have hdot := dot_gaugeVector m H hm
 220  have hvi : v i = w i / s - m i * dot w m / (2 * s ^ 2) := rfl
 221  have key : s * v i + m i * dot v m = w i := by
 222    rw [hvi, show dot v m = dot w m / (2 * s) from hdot]
 223    field_simp [hs0]; ring
 224  rw [hL]; simpa [s, w, v] using key
 225
 226theorem gaugeCorrected_transverse (m : Fin 4 → ℝ) (H : Mat4)
 227    (hm : momentumSq m ≠ 0) :
 228    IsTransverse m (gaugeCorrected m H) := by
 229  intro i
 230  change load (gaugeCorrected m H) m i = 0
 231  simp [gaugeCorrected, load_sub, load_gaugePart_gaugeVector m H hm]
 232
 233theorem gaugeCorrected_symmetric (m : Fin 4 → ℝ) (H : Mat4)
 234    (hH : IsSymmetric H) :
 235    IsSymmetric (gaugeCorrected m H) := by
 236  intro i j
 237  simp only [gaugeCorrected, sub_apply]
 238  rw [hH i j, gaugePart_symmetric m (gaugeVector m H) i j]
 239
 240/-! ## §3. TT projection -/
 241
 242theorem euclideanTrace_smul (c : ℝ) (H : Mat4) :
 243    euclideanTrace (c • H) = c * euclideanTrace H := by
 244  unfold euclideanTrace
 245  simp only [smul_apply, smul_eq_mul]
 246  exact (Finset.mul_sum Finset.univ (fun i => H i i) c).symm
 247
 248theorem euclideanTrace_sub (A B : Mat4) :
 249    euclideanTrace (A - B) = euclideanTrace A - euclideanTrace B := by
 250  unfold euclideanTrace; simp [Finset.sum_sub_distrib]
 251
 252theorem euclideanTrace_one : euclideanTrace (1 : Mat4) = 4 := by
 253  unfold euclideanTrace
 254  rw [Fin.sum_univ_four]
 255  simp
 256  norm_num
 257
 258theorem euclideanTrace_outerSq (m : Fin 4 → ℝ) :
 259    euclideanTrace (outerSq m) = momentumSq m := rfl
 260
 261theorem euclideanTrace_transverseProjector (m : Fin 4 → ℝ)
 262    (hm : momentumSq m ≠ 0) :
 263    euclideanTrace (transverseProjector m) = 3 := by
 264  unfold transverseProjector
 265  rw [euclideanTrace_sub, euclideanTrace_smul, euclideanTrace_one,
 266    euclideanTrace_outerSq]
 267  field_simp [hm]; ring
 268
 269theorem ttProject_symmetric (m : Fin 4 → ℝ) (H : Mat4)
 270    (hH : IsSymmetric H) :
 271    IsSymmetric (ttProject m H) := by
 272  intro i j
 273  simp only [ttProject, sub_apply, smul_apply, smul_eq_mul]
 274  rw [gaugeCorrected_symmetric m H hH i j,
 275    transverseProjector_symmetric m i j]
 276
 277theorem ttProject_transverse (m : Fin 4 → ℝ) (H : Mat4)
 278    (hm : momentumSq m ≠ 0) :
 279    IsTransverse m (ttProject m H) := by
 280  intro i
 281  change load (ttProject m H) m i = 0
 282  have h1 : load (gaugeCorrected m H) m i = 0 :=
 283    gaugeCorrected_transverse m H hm i
 284  have h2 := load_transverseProjector m hm i
 285  simp [ttProject, load_sub, load_smul, h1, h2]
 286
 287theorem ttProject_traceless (m : Fin 4 → ℝ) (H : Mat4)
 288    (hm : momentumSq m ≠ 0) :
 289    IsTraceless (ttProject m H) := by
 290  unfold IsTraceless ttProject residualTrace
 291  rw [euclideanTrace_sub, euclideanTrace_smul,
 292    euclideanTrace_transverseProjector m hm]
 293  ring
 294
 295theorem ttProject_isTT (m : Fin 4 → ℝ) (H : Mat4)
 296    (hH : IsSymmetric H) (hm : momentumSq m ≠ 0) :
 297    IsTT m (ttProject m H) :=
 298  ⟨ttProject_symmetric m H hH, ttProject_traceless m H hm,
 299    ttProject_transverse m H hm⟩
 300
 301/-- **THEOREM (algebraic `edge_tt_decomposition` layer).**
 302Every symmetric `4 × 4` matrix against a nonzero Euclidean wave covector
 303decomposes as TT + gauge + transverse-trace part. -/
 304theorem exists_edgeTTDecomposition (m : Fin 4 → ℝ) (H : Mat4)
 305    (hH : IsSymmetric H) (hm : momentumSq m ≠ 0) :
 306    H = ttProject m H + gaugePart m (gaugeVector m H) +
 307        residualTrace m H • transverseProjector m ∧
 308      IsTT m (ttProject m H) := by
 309  refine ⟨?_, ttProject_isTT m H hH hm⟩
 310  unfold ttProject gaugeCorrected; abel
 311
 312theorem exists_edgeTTDecomposition' (m : Fin 4 → ℝ) (H : Mat4)
 313    (hH : IsSymmetric H) (hm : momentumSq m ≠ 0) :
 314    ∃ (H_TT : Mat4) (v : Fin 4 → ℝ) (β : ℝ),
 315      H = H_TT + gaugePart m v + β • transverseProjector m ∧
 316        IsTT m H_TT :=
 317  ⟨ttProject m H, gaugeVector m H, residualTrace m H,
 318    exists_edgeTTDecomposition m H hH hm⟩
 319
 320/-! ## §4. Nondegeneracy: two independent unnormalized TT polarizations -/
 321
 322def axisWave : Fin 4 → ℝ
 323  | 0 => 1
 324  | 1 => 0
 325  | 2 => 0
 326  | 3 => 0
 327
 328theorem axisWave_momentumSq : momentumSq axisWave = 1 := by
 329  unfold momentumSq axisWave
 330  simp [Fin.sum_univ_four]
 331
 332/-- Plus polarization `diag(0,0,1,−1)` (unnormalized). -/
 333def axisTTPlus : Mat4
 334  | 0, 0 => 0 | 0, 1 => 0 | 0, 2 => 0 | 0, 3 => 0
 335  | 1, 0 => 0 | 1, 1 => 0 | 1, 2 => 0 | 1, 3 => 0
 336  | 2, 0 => 0 | 2, 1 => 0 | 2, 2 => 1 | 2, 3 => 0
 337  | 3, 0 => 0 | 3, 1 => 0 | 3, 2 => 0 | 3, 3 => -1
 338
 339/-- Cross polarization `H₂₃ = H₃₂ = 1` (unnormalized). -/
 340def axisTTCross : Mat4
 341  | 0, 0 => 0 | 0, 1 => 0 | 0, 2 => 0 | 0, 3 => 0
 342  | 1, 0 => 0 | 1, 1 => 0 | 1, 2 => 0 | 1, 3 => 0
 343  | 2, 0 => 0 | 2, 1 => 0 | 2, 2 => 0 | 2, 3 => 1
 344  | 3, 0 => 0 | 3, 1 => 0 | 3, 2 => 1 | 3, 3 => 0
 345
 346theorem axisTTPlus_isTT : IsTT axisWave axisTTPlus := by
 347  refine ⟨?_, ?_, ?_⟩
 348  · intro i j; fin_cases i <;> fin_cases j <;> rfl
 349  · unfold IsTraceless euclideanTrace axisTTPlus
 350    simp [Fin.sum_univ_four]
 351  · intro i
 352    fin_cases i <;> simp [axisTTPlus, axisWave, Fin.sum_univ_four]
 353
 354theorem axisTTCross_isTT : IsTT axisWave axisTTCross := by
 355  refine ⟨?_, ?_, ?_⟩
 356  · intro i j; fin_cases i <;> fin_cases j <;> rfl
 357  · unfold IsTraceless euclideanTrace axisTTCross
 358    simp [Fin.sum_univ_four]
 359  · intro i
 360    fin_cases i <;> simp [axisTTCross, axisWave, Fin.sum_univ_four]
 361
 362theorem axisTTPlus_ne_zero : axisTTPlus ≠ 0 := by
 363  intro h
 364  have := congrArg (fun M : Mat4 => M 2 2) h
 365  simp [axisTTPlus] at this
 366
 367theorem axisTTCross_ne_zero : axisTTCross ≠ 0 := by
 368  intro h
 369  have := congrArg (fun M : Mat4 => M 2 3) h
 370  simp [axisTTCross] at this
 371
 372theorem axisTT_independent {a b : ℝ}
 373    (h : a • axisTTPlus + b • axisTTCross = 0) :
 374    a = 0 ∧ b = 0 := by
 375  have h22 := congrArg (fun M : Mat4 => M 2 2) h
 376  have h23 := congrArg (fun M : Mat4 => M 2 3) h
 377  simp [axisTTPlus, axisTTCross, smul_eq_mul] at h22 h23
 378  exact ⟨h22, h23⟩
 379
 380/-! ## §5. Decoy and zero-momentum degeneracy -/
 381
 382def decoyLongitudinal : Mat4 :=
 383  gaugePart axisWave fun i => if i = 0 then (1 : ℝ) else 0
 384
 385theorem decoyLongitudinal_symmetric : IsSymmetric decoyLongitudinal :=
 386  gaugePart_symmetric _ _
 387
 388theorem decoyLongitudinal_not_transverse :
 389    ¬ IsTransverse axisWave decoyLongitudinal := by
 390  intro h
 391  have h0 := h 0
 392  simp [decoyLongitudinal, gaugePart, axisWave, Fin.sum_univ_four] at h0
 393
 394theorem decoy_ttProject_isTT :
 395    IsTT axisWave (ttProject axisWave decoyLongitudinal) :=
 396  ttProject_isTT axisWave decoyLongitudinal decoyLongitudinal_symmetric
 397    (by simp [axisWave_momentumSq])
 398
 399theorem decoy_projection_restores_transverse :
 400    IsTransverse axisWave (ttProject axisWave decoyLongitudinal) :=
 401  decoy_ttProject_isTT.2.2
 402
 403theorem zero_wave_momentumSq :
 404    momentumSq (fun _ : Fin 4 => (0 : ℝ)) = 0 := by
 405  unfold momentumSq; simp
 406
 407theorem decomposition_hypothesis_fails_at_zero :
 408    ¬ (momentumSq (fun _ : Fin 4 => (0 : ℝ)) ≠ 0) := by
 409  simp [zero_wave_momentumSq]
 410
 411end
 412
 413end EdgeTTDecomposition4D
 414end Analysis
 415end Gravity
 416end IndisputableMonolith
 417