IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelGlue

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochData4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DKernelCert
   5import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumAssemble
   6
   7/-!
   8# Algebraic glue: Array-sum m^2 coeffs <-> Int fold <-> scale-32 tables
   9
  10Lifts the kernel `decide` Int certificates to the Q coefficient tables used by
  11`ReggeExactMidpointM2TTIdentity4D`.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Gravity
  16namespace Analysis
  17namespace ReggeExactMidpointM2TTIdentity4D
  18namespace KernelGlue
  19
  20open ReggeExactFlatHessianBlochData4D
  21open ReggeExactFlatHessianBlochSymbol4D (CouplingIdx)
  22open KernelCert
  23open BigOperators
  24
  25set_option maxHeartbeats 80000000
  26
  27/-- Old Array/Finset definition of the bi-quadratic coefficient. -/
  28def m2CoeffSum (a b c d i j : Fin 4) : ℚ :=
  29  Finset.sum (Finset.univ : Finset CouplingIdx) fun idx =>
  30    (-(1 / 4) : ℚ) * ((couplingTable[idx].num : ℚ) / (couplingTable[idx].den : ℚ)) *
  31      (couplingTable[idx].De a : ℚ) * (couplingTable[idx].De b : ℚ) *
  32      (couplingTable[idx].Dep c : ℚ) * (couplingTable[idx].Dep d : ℚ) *
  33      ((couplingTable[idx].delta2 i : ℚ) / 2) *
  34      ((couplingTable[idx].delta2 j : ℚ) / 2)
  35
  36/-- Explicit table as scale-32 Int cast (replaces the giant match). -/
  37def explicitM2CoeffZ (a b c d i j : Fin 4) : ℚ :=
  38  (explicitZ a b c d i j : ℚ) / 32
  39
  40/-- Closed table as scale-32 Int cast. -/
  41def closedCoeffZ (a b c d i j : Fin 4) : ℚ :=
  42  (closedZ a b c d i j : ℚ) / 32
  43
  44private theorem toCZ_De (c : Coupling) (a : Fin 4) : De (toCZ c) a = c.De a := by
  45  fin_cases a <;> rfl
  46
  47private theorem toCZ_Dep (c : Coupling) (a : Fin 4) : Dep (toCZ c) a = c.Dep a := by
  48  fin_cases a <;> rfl
  49
  50private theorem toCZ_D2 (c : Coupling) (a : Fin 4) : D2 (toCZ c) a = c.delta2 a := by
  51  fin_cases a <;> rfl
  52
  53/-- Per-coupling rational term equals Int contrib / 256, assuming `den | 16`. -/
  54theorem termQ_eq_contrib_div (c : Coupling) (a b cd d i j : Fin 4)
  55    (hd : c.den ∣ 16) (hden : c.den ≠ 0) :
  56    (-(1 / 4) : ℚ) * ((c.num : ℚ) / (c.den : ℚ)) *
  57        (c.De a : ℚ) * (c.De b : ℚ) * (c.Dep cd : ℚ) * (c.Dep d : ℚ) *
  58        ((c.delta2 i : ℚ) / 2) * ((c.delta2 j : ℚ) / 2) =
  59      (contrib (toCZ c) a b cd d i j : ℚ) / 256 := by
  60  have hdenQ : (c.den : ℚ) ≠ 0 := by exact_mod_cast hden
  61  have hNat : ((16 / c.den : Nat) : ℚ) = (16 : ℚ) / (c.den : ℚ) := by
  62    simpa using (Nat.cast_div (m := 16) (n := c.den) hd hdenQ).symm
  63  unfold contrib
  64  simp only [toCZ_De, toCZ_Dep, toCZ_D2, hNat]
  65  push_cast
  66  field_simp [hdenQ]
  67  ring
  68
  69/-- Every den on the generated CZ list divides 16 and is nonzero. -/
  70theorem cz_den_dvd_sixteen (t : CZ) (ht : t ∈ couplingZList) :
  71    t.den ∣ 16 ∧ t.den ≠ 0 := by
  72  revert t ht
  73  decide
  74
  75theorem coupling_den_dvd_sixteen (c : Coupling) (hc : c ∈ couplingTable.toList) :
  76    c.den ∣ 16 ∧ c.den ≠ 0 := by
  77  have hb := couplingZList_bridge
  78  have : toCZ c ∈ couplingZList := by
  79    have := List.mem_map_of_mem (f := toCZ) hc
  80    simpa [hb] using this
  81  simpa [toCZ] using cz_den_dvd_sixteen (toCZ c) this
  82
  83private theorem sum_map_contrib_eq_m2Num (a b c d i j : Fin 4) :
  84    (couplingZList.map (fun t => contrib t a b c d i j)).sum =
  85      m2Num a b c d i j := by
  86  unfold m2Num
  87  induction couplingZList with
  88  | nil => simp
  89  | cons t ts ih =>
  90    simp [List.sum_cons, List.foldl, ih]
  91    abel
  92
  93private theorem toList_sum_eq_finset_sum (a b c d i j : Fin 4) :
  94    (couplingTable.toList.map fun coup =>
  95        (-(1 / 4) : ℚ) * ((coup.num : ℚ) / (coup.den : ℚ)) *
  96          (coup.De a : ℚ) * (coup.De b : ℚ) *
  97          (coup.Dep c : ℚ) * (coup.Dep d : ℚ) *
  98          ((coup.delta2 i : ℚ) / 2) * ((coup.delta2 j : ℚ) / 2)).sum =
  99      m2CoeffSum a b c d i j := by
 100  unfold m2CoeffSum
 101  have hArr :
 102      couplingTable.toList =
 103        List.ofFn fun idx : CouplingIdx => couplingTable[idx] := by
 104    simpa using (Array.toList_eq_ofFn (xs := couplingTable)).symm
 105  simp [hArr, List.map_ofFn, List.sum_ofFn]
 106
 107/-- Finset Array sum equals the bridged Int fold / 256. -/
 108theorem m2CoeffSum_eq_m2Num_div (a b c d i j : Fin 4) :
 109    m2CoeffSum a b c d i j = (m2Num a b c d i j : ℚ) / 256 := by
 110  rw [← toList_sum_eq_finset_sum]
 111  have hmap :
 112      (couplingTable.toList.map fun coup =>
 113          (-(1 / 4) : ℚ) * ((coup.num : ℚ) / (coup.den : ℚ)) *
 114            (coup.De a : ℚ) * (coup.De b : ℚ) *
 115            (coup.Dep c : ℚ) * (coup.Dep d : ℚ) *
 116            ((coup.delta2 i : ℚ) / 2) * ((coup.delta2 j : ℚ) / 2)) =
 117        couplingZList.map fun t => (contrib t a b c d i j : ℚ) / 256 := by
 118    have hb := couplingZList_bridge
 119    have h1 :
 120        (couplingTable.toList.map fun coup =>
 121            (-(1 / 4) : ℚ) * ((coup.num : ℚ) / (coup.den : ℚ)) *
 122              (coup.De a : ℚ) * (coup.De b : ℚ) *
 123              (coup.Dep c : ℚ) * (coup.Dep d : ℚ) *
 124              ((coup.delta2 i : ℚ) / 2) * ((coup.delta2 j : ℚ) / 2)) =
 125          couplingTable.toList.map fun coup =>
 126            (contrib (toCZ coup) a b c d i j : ℚ) / 256 := by
 127      refine List.map_congr_left.mpr fun coup hc => ?_
 128      obtain ⟨hdvd, hne⟩ := coupling_den_dvd_sixteen coup hc
 129      exact termQ_eq_contrib_div coup a b c d i j hdvd hne
 130    have h2 :
 131        (couplingTable.toList.map fun coup =>
 132            (contrib (toCZ coup) a b c d i j : ℚ) / 256) =
 133          (couplingTable.toList.map toCZ).map fun t =>
 134            (contrib t a b c d i j : ℚ) / 256 := by
 135      simp [List.map_map, Function.comp]
 136    rw [h1, h2, hb]
 137  rw [hmap]
 138  have hdiv :
 139      (couplingZList.map fun t => (contrib t a b c d i j : ℚ) / 256).sum =
 140        ((couplingZList.map fun t => contrib t a b c d i j).sum : ℚ) / 256 := by
 141    simp [List.sum_map_div]
 142  rw [hdiv, sum_map_contrib_eq_m2Num]
 143
 144/-- m2CoeffSum equals the scale-32 explicit table. -/
 145theorem m2CoeffSum_eq_explicitM2CoeffZ :
 146    ∀ (a b c d i j : Fin 4),
 147      m2CoeffSum a b c d i j = explicitM2CoeffZ a b c d i j := by
 148  intro a b c d i j
 149  rw [m2CoeffSum_eq_m2Num_div, explicitM2CoeffZ, m2Num_eq_eight_explicitZ]
 150  push_cast
 151  ring
 152
 153/-- ite closedCoeff equals scale-32 closedZ. -/
 154theorem closedCoeff_eq_closedCoeffZ :
 155    ∀ (a b c d i j : Fin 4),
 156      ((if a = c ∧ b = d ∧ i = j then -(1 / 8) else 0) +
 157          (if a = c ∧ b = i ∧ d = j then (1 / 4) else 0) +
 158          (if a = b ∧ c = d ∧ i = j then (1 / 8) else 0) +
 159          (if a = b ∧ c = i ∧ d = j then -(1 / 4) else 0) : ℚ) =
 160        closedCoeffZ a b c d i j := by
 161  intro a b c d i j
 162  unfold closedCoeffZ closedZ
 163  split_ifs <;> norm_num
 164
 165/-- Scaling lemma for the order-4 flip average. -/
 166theorem sym4_scale
 167    (C : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Int)
 168    (a b c d i j : Fin 4) :
 169    ((C a b c d i j : ℚ) / 32 + (C b a c d i j : ℚ) / 32 +
 170        (C a b d c i j : ℚ) / 32 + (C b a d c i j : ℚ) / 32) / 4 =
 171      (sym4Z C a b c d i j : ℚ) / 32 := by
 172  unfold sym4Z
 173  push_cast
 174  ring
 175
 176/-- Scaling lemma for the full order-8 symmetrization. -/
 177theorem symFull_scale
 178    (C : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Int)
 179    (a b c d i j : Fin 4) :
 180    (((C a b c d i j : ℚ) / 32 + (C b a c d i j : ℚ) / 32 +
 181            (C a b d c i j : ℚ) / 32 + (C b a d c i j : ℚ) / 32) / 4 +
 182        ((C c d a b i j : ℚ) / 32 + (C d c a b i j : ℚ) / 32 +
 183            (C c d b a i j : ℚ) / 32 + (C d c b a i j : ℚ) / 32) / 4) / 2 =
 184      (symFullZ C a b c d i j : ℚ) / 32 := by
 185  unfold symFullZ sym4Z
 186  push_cast
 187  ring
 188
 189/-- Pointwise symFull equality on the scale-32 tables. -/
 190theorem symFullZ_rat_explicit_eq_closed :
 191    ∀ (a b c d i j : Fin 4),
 192      (symFullZ explicitZ a b c d i j : ℚ) / 32 =
 193        (symFullZ closedZ a b c d i j : ℚ) / 32 := by
 194  intro a b c d i j
 195  rw [symFullZ_explicit_eq_closed]
 196
 197end KernelGlue
 198end ReggeExactMidpointM2TTIdentity4D
 199end Analysis
 200end Gravity
 201end IndisputableMonolith
 202