IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbolZero4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochData4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
   4
   5/-!
   6# Exact midpoint Bloch symbol vanishes at zero momentum
   7
   8Proves `∀ H, exactMidpointBlochSymbolZero H = 0` by expanding the
   9zero-momentum trig polynomial as a quartic form
  10`∑_{a,b,c,d} Q_abcd H_ab H_cd` with rational coefficients `Q_abcd`
  11read from `couplingTable`, then discharging `Q_abcd = 0` for all
  12index quadruples by `native_decide` over `ℚ`.
  13
  14Inhabits `TypedResidual_midpointBloch_symbolZero` (same forall).
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Gravity
  19namespace Analysis
  20namespace ReggeExactFlatHessianBlochSymbolZero4D
  21
  22open ReggeExactFlatHessianBlochData4D
  23open ReggeExactFlatHessianBlochSymbol4D
  24open BigOperators
  25
  26set_option maxRecDepth 4096
  27set_option maxHeartbeats 4000000
  28
  29/-! ## §1. Rational quartic coefficients (computable) -/
  30
  31/-- Computable rational coupling weight (Data.`Coupling.s` is marked
  32noncomputable by section). -/
  33def couplingS (coup : Coupling) : ℚ :=
  34  (coup.num : ℚ) / (coup.den : ℚ)
  35
  36theorem couplingS_eq_s (coup : Coupling) : couplingS coup = coup.s := rfl
  37
  38/-- Quartic coefficient of the zero-momentum symbol:
  39`Q_abcd = ∑_i (1/2) s_i (De_i)_a (De_i)_b (Dep_i)_c (Dep_i)_d`. -/
  40def qCoeff (a b c d : Fin 4) : ℚ :=
  41  ∑ i : CouplingIdx,
  42    (1 / 2 : ℚ) * couplingS couplingTable[i] *
  43      (couplingTable[i].De a : ℚ) * (couplingTable[i].De b : ℚ) *
  44      (couplingTable[i].Dep c : ℚ) * (couplingTable[i].Dep d : ℚ)
  45
  46/-- **THEOREM:** every rational quartic coefficient vanishes. -/
  47theorem qCoeff_eq_zero : ∀ (a b c d : Fin 4), qCoeff a b c d = 0 := by
  48  native_decide
  49
  50noncomputable section
  51
  52/-! ## §2. Expand symbolZero through the quartic form -/
  53
  54/-- One coupling's real monomial coefficient before summing over the table. -/
  55def couplingMonomial (coup : Coupling) (a b c d : Fin 4) : ℝ :=
  56  (1 / 2 : ℝ) * (couplingS coup : ℝ) *
  57    (coup.De a : ℝ) * (coup.De b : ℝ) * (coup.Dep c : ℝ) * (coup.Dep d : ℝ)
  58
  59private theorem edgeStrain_mul_edgeStrain (H : Mat4) (De Dep : Fin 4 → ℤ) :
  60    edgeStrain H De * edgeStrain H Dep =
  61      ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
  62        H a b * H c d * (De a : ℝ) * (De b : ℝ) * (Dep c : ℝ) * (Dep d : ℝ) := by
  63  unfold edgeStrain
  64  simp_rw [Finset.sum_mul, Finset.mul_sum]
  65  refine Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ =>
  66    Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => ?_
  67  ring
  68
  69private theorem couplingWeight_eq_quartic (H : Mat4) (coup : Coupling) :
  70    couplingWeight H coup =
  71      ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
  72        couplingMonomial coup a b c d * H a b * H c d := by
  73  unfold couplingWeight couplingMonomial
  74  rw [← couplingS_eq_s]
  75  have hre :
  76      (1 / 2 : ℝ) * (couplingS coup : ℝ) * edgeStrain H coup.De * edgeStrain H coup.Dep =
  77        ((1 / 2 : ℝ) * (couplingS coup : ℝ)) *
  78          (edgeStrain H coup.De * edgeStrain H coup.Dep) := by
  79    ring
  80  rw [hre, edgeStrain_mul_edgeStrain]
  81  simp_rw [Finset.mul_sum]
  82  refine Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ =>
  83    Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => ?_
  84  ring
  85
  86private theorem qCoeff_cast_eq_sum (a b c d : Fin 4) :
  87    (qCoeff a b c d : ℝ) =
  88      ∑ i : CouplingIdx, couplingMonomial couplingTable[i] a b c d := by
  89  unfold qCoeff couplingMonomial
  90  rw [Rat.cast_sum]
  91  refine Finset.sum_congr rfl fun _ _ => ?_
  92  push_cast
  93  ring
  94
  95private theorem sum_comm_idx_fin4
  96    {α : Type*} [AddCommMonoid α]
  97    (f : CouplingIdx → Fin 4 → Fin 4 → Fin 4 → Fin 4 → α) :
  98    (∑ i : CouplingIdx, ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
  99        f i a b c d) =
 100      ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
 101        ∑ i : CouplingIdx, f i a b c d := by
 102  rw [Finset.sum_comm]
 103  refine Finset.sum_congr rfl fun _ _ => ?_
 104  rw [Finset.sum_comm]
 105  refine Finset.sum_congr rfl fun _ _ => ?_
 106  rw [Finset.sum_comm]
 107  refine Finset.sum_congr rfl fun _ _ => ?_
 108  rw [Finset.sum_comm]
 109
 110private theorem factor_HabHcd (H : Mat4) (a b c d : Fin 4) :
 111    (∑ i : CouplingIdx,
 112        couplingMonomial couplingTable[i] a b c d * H a b * H c d) =
 113      (qCoeff a b c d : ℝ) * H a b * H c d := by
 114  have hα :
 115      ∀ i : CouplingIdx,
 116        couplingMonomial couplingTable[i] a b c d * H a b * H c d =
 117          couplingMonomial couplingTable[i] a b c d * (H a b * H c d) := by
 118    intro i; ring
 119  simp_rw [hα]
 120  rw [← Finset.sum_mul, ← qCoeff_cast_eq_sum]
 121  ring
 122
 123private theorem sum_weight_eq_sum_quartic_terms (H : Mat4) :
 124    (∑ i : CouplingIdx, couplingWeight H couplingTable[i]) =
 125      ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
 126        (qCoeff a b c d : ℝ) * H a b * H c d := by
 127  refine (Finset.sum_congr rfl fun i _ =>
 128    couplingWeight_eq_quartic H couplingTable[i]).trans ?_
 129  refine (sum_comm_idx_fin4
 130      (fun (i : CouplingIdx) (a b c d : Fin 4) =>
 131        couplingMonomial (couplingTable[i]) a b c d * H a b * H c d)).trans ?_
 132  refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
 133    Finset.sum_congr rfl fun c _ => Finset.sum_congr rfl fun d _ =>
 134      factor_HabHcd H a b c d
 135
 136/-- Zero-momentum symbol equals the quartic form with coefficients `qCoeff`. -/
 137theorem exactMidpointBlochSymbolZero_eq_quartic (H : Mat4) :
 138    exactMidpointBlochSymbolZero H =
 139      ∑ a : Fin 4, ∑ b : Fin 4, ∑ c : Fin 4, ∑ d : Fin 4,
 140        (qCoeff a b c d : ℝ) * H a b * H c d := by
 141  unfold exactMidpointBlochSymbolZero couplingWeightIdx
 142  exact sum_weight_eq_sum_quartic_terms H
 143
 144/-! ## §3. Main theorem -/
 145
 146/-- **THEOREM:** the exact midpoint Bloch symbol vanishes at zero momentum. -/
 147theorem exactMidpointBlochSymbolZero_eq_zero (H : Mat4) :
 148    exactMidpointBlochSymbolZero H = 0 := by
 149  rw [exactMidpointBlochSymbolZero_eq_quartic]
 150  refine Finset.sum_eq_zero fun a _ => Finset.sum_eq_zero fun b _ =>
 151    Finset.sum_eq_zero fun c _ => Finset.sum_eq_zero fun d _ => ?_
 152  simp [qCoeff_eq_zero a b c d]
 153
 154/-- Inhabits `TypedResidual_midpointBloch_symbolZero`
 155(`∀ H, exactMidpointBlochSymbolZero H = 0`). -/
 156theorem typedResidual_midpointBloch_symbolZero :
 157    ∀ H : Mat4, exactMidpointBlochSymbolZero H = 0 :=
 158  exactMidpointBlochSymbolZero_eq_zero
 159
 160end
 161
 162end ReggeExactFlatHessianBlochSymbolZero4D
 163end Analysis
 164end Gravity
 165end IndisputableMonolith
 166