IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   5
   6/-!
   7# Transported all-orbit m² evaluation certificates
   8
   9Closes the raw all-orbit moment on `axisTTPlus` / `symbolDir`:
  10
  11  `m2TransportedAllOrbitMoment axisTTPlus symbolDir = -5/2`
  12
  13by integer (or radical-cancelled integer) per-orbit certificates, then sum.
  14Also proves gauge vanishing on `decoyGauge`, and the distinct-hinge
  15weighted moment (`1/r_τ`):
  16
  17  `m2TransportedAllOrbitMomentDistinctHinge axisTTPlus symbolDir = -1/4`
  18
  19(`-3/6 + 2/4 + (-3/2)/6`), with decoy gauge still `0`.
  20
  21Orbit slices on plus (THEOREM):
  22t11 = -3, t12 = +2, t13 = -3/2, t21 = t31 = t22 = 0.
  23
  24Also closes `axisTTCross` / `symbolDir` distinct-hinge isotropy:
  25
  26  `m2TransportedAllOrbitMomentDistinctHinge axisTTCross symbolDir = -1/4`
  27
  28(raw all-orbit on cross is `0`; orbit slices differ from plus, but the
  29`1/r_τ` fold matches).  Normalized plus/cross both give raw `-1/8`.
  30
  31Axis-aligned ray `e0Dir=(1,0,0,0)` is now Lean-certified: plus
  32distinct-hinge `0`, cross `-1/8` (normalized `-1/16`).  Plus/cross agree
  33on `symbolDir` and disagree on bare `e0` (OPEN
  34`Regge4DContinuumIsotropyBlockedOnAxisMode`).
  35
  36Full cosine two-jet `A0*K2 + A2*K0` (§12): slotwise `K0 = 0` on
  37`axisTTPlus` / `axisTTCross` (integer certificates), so full = trunc on
  38every direction; e0 anisotropy and plus vanishing are **not** repaired
  39(`Regge4DFullTwoJetRestoresE0PlusVanishing` / `...E0Isotropy` status false).
  40External probe receipt:
  41`state/qg_full_theory/probe_fulljet_distinct_hinge_20260721.json`.
  42
  43Does **not** flip `gap_action_recovery`.
  44-/
  45
  46namespace IndisputableMonolith
  47namespace Gravity
  48namespace Analysis
  49namespace ReggeBlochTransportedAllOrbitM2Eval4D
  50
  51open BigOperators
  52open ReggeEdgeStencil4D
  53open ReggeHinge4DOrbitClassification
  54open ReggeBlochFold4D
  55open ReggeBlochM2Symbol4D
  56open ReggeBlochOrbitTransport4D
  57open ReggeBlochTransportedAllOrbit4D
  58open ReggeBlochAllOrbitSymbol4D (isOrbit isOrbit_t11_iff_isT11 phaseScaleDir)
  59open ReggeFlat4DHessianAssembly
  60open EdgeTTDecomposition4D (axisTTPlus axisTTCross)
  61
  62abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
  63-- decoyGauge lives in ReggeEdgeStencil4D (already opened above)
  64
  65noncomputable section
  66
  67/-! ## §1. Pushforward reindex helpers -/
  68
  69theorem sum_mul_pushforward (v w : Fin 15 → ℝ) (p : Fin 24) :
  70    (∑ d : Fin 15, pushforwardClass v p d * w d) =
  71      ∑ d0 : Fin 15, v d0 * w (permClass p d0) := by
  72  unfold pushforwardClass
  73  simp_rw [Finset.sum_mul]
  74  rw [Finset.sum_comm]
  75  refine Finset.sum_congr rfl fun d0 _ => ?_
  76  have h : ∀ d : Fin 15,
  77      (if permClass p d0 = d then v d0 else 0) * w d =
  78        if permClass p d0 = d then v d0 * w d else 0 := by
  79    intro d; split_ifs <;> simp
  80  simp_rw [h]
  81  rw [Finset.sum_ite_eq]
  82  simp
  83
  84theorem sum_mul_pushforward_weighted (v w f : Fin 15 → ℝ) (p : Fin 24) :
  85    (∑ d : Fin 15, pushforwardClass v p d * w d * f d) =
  86      ∑ d0 : Fin 15, v d0 * w (permClass p d0) * f (permClass p d0) := by
  87  unfold pushforwardClass
  88  simp_rw [mul_assoc, Finset.sum_mul]
  89  rw [Finset.sum_comm]
  90  refine Finset.sum_congr rfl fun d0 _ => ?_
  91  have h : ∀ d : Fin 15,
  92      (if permClass p d0 = d then v d0 else 0) * (w d * f d) =
  93        if permClass p d0 = d then v d0 * (w d * f d) else 0 := by
  94    intro d; split_ifs <;> simp
  95  simp_rw [h]
  96  rw [Finset.sum_ite_eq]
  97  simp [mul_assoc]
  98
  99private lemma sum_div_const_st (c : ℝ) (f : Fin 24 → Fin 10 → ℝ) :
 100    (∑ s : Fin 24, ∑ t : Fin 10, f s t / c) =
 101      (∑ s : Fin 24, ∑ t : Fin 10, f s t) / c := by
 102  simp_rw [div_eq_mul_inv, ← Finset.sum_mul]
 103
 104private lemma sum_six_orbits (f : HingeOrbitType → ℝ) :
 105    (∑ ty : HingeOrbitType, f ty) =
 106      f .t11 + f .t12 + f .t21 + f .t13 + f .t31 + f .t22 := by
 107  have h : (Finset.univ : Finset HingeOrbitType) =
 108      insert HingeOrbitType.t11
 109        (insert HingeOrbitType.t12
 110          (insert HingeOrbitType.t21
 111            (insert HingeOrbitType.t13
 112              (insert HingeOrbitType.t31
 113                (insert HingeOrbitType.t22 (∅ : Finset HingeOrbitType)))))) := by
 114    decide
 115  simp [h, Finset.sum_insert]
 116  ring
 117
 118/-! ## §2. Integer area seeds (radical factored out) -/
 119
 120def area12Z (d : Fin 15) : ℤ :=
 121  match d with | ⟨0, _⟩ => 2 | ⟨5, _⟩ => 1 | _ => 0
 122
 123def area21Z (d : Fin 15) : ℤ :=
 124  match d with | ⟨2, _⟩ => 1 | ⟨3, _⟩ => 2 | _ => 0
 125
 126def area13Z (d : Fin 15) : ℤ :=
 127  match d with | ⟨0, _⟩ => 3 | ⟨13, _⟩ => 1 | _ => 0
 128
 129def area31Z (d : Fin 15) : ℤ :=
 130  match d with | ⟨6, _⟩ => 1 | ⟨7, _⟩ => 3 | _ => 0
 131
 132def area22Z (d : Fin 15) : ℤ :=
 133  match d with | ⟨2, _⟩ => 1 | ⟨11, _⟩ => 1 | _ => 0
 134
 135theorem areaCov12_eq_z (d : Fin 15) :
 136    areaCov12 d = Real.sqrt 2 * (area12Z d : ℝ) / 8 := by
 137  fin_cases d <;> simp [areaCov12, area12Z] <;> ring
 138
 139theorem areaCov21_eq_z (d : Fin 15) :
 140    areaCov21 d = Real.sqrt 2 * (area21Z d : ℝ) / 8 := by
 141  fin_cases d <;> simp [areaCov21, area21Z] <;> ring
 142
 143theorem areaCov13_eq_z (d : Fin 15) :
 144    areaCov13 d = Real.sqrt 3 * (area13Z d : ℝ) / 12 := by
 145  fin_cases d <;> simp [areaCov13, area13Z] <;> ring
 146
 147theorem areaCov31_eq_z (d : Fin 15) :
 148    areaCov31 d = Real.sqrt 3 * (area31Z d : ℝ) / 12 := by
 149  fin_cases d <;> simp [areaCov31, area31Z] <;> ring
 150
 151theorem areaCov22_eq_z (d : Fin 15) :
 152    areaCov22 d = (area22Z d : ℝ) / 4 := by
 153  fin_cases d <;> simp [areaCov22, area22Z] <;> norm_num
 154
 155/-! ## §3. Per-orbit slot certificates -/
 156
 157def slotAZ12 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 158  ∑ d0 : Fin 15, area12Z d0 * cz (permClass (orbitCoveringPerm .t12 s t) d0)
 159
 160def slotAZ21 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 161  ∑ d0 : Fin 15, area21Z d0 * cz (permClass (orbitCoveringPerm .t21 s t) d0)
 162
 163def slotAZ13 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 164  ∑ d0 : Fin 15, area13Z d0 * cz (permClass (orbitCoveringPerm .t13 s t) d0)
 165
 166def slotAZ31 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 167  ∑ d0 : Fin 15, area31Z d0 * cz (permClass (orbitCoveringPerm .t31 s t) d0)
 168
 169def slotAZ22 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 170  ∑ d0 : Fin 15, area22Z d0 * cz (permClass (orbitCoveringPerm .t22 s t) d0)
 171
 172def slotKppOrbit (sign : Fin 15 → ℤ) (cz : Fin 15 → ℤ)
 173    (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) : ℤ :=
 174  ∑ d0 : Fin 15,
 175    sign d0 * cz (permClass (orbitCoveringPerm ty s t) d0) *
 176      ((phase2Nat s t (permClass (orbitCoveringPerm ty s t) d0) : ℕ) : ℤ) ^ 2
 177
 178def m2OrbitCertZ12 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 179  if isOrbit .t12 s t then -slotAZ12 cz s t * slotKppOrbit kernel12Sign cz .t12 s t
 180  else 0
 181
 182def m2OrbitCertZ21 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 183  if isOrbit .t21 s t then -slotAZ21 cz s t * slotKppOrbit kernel12Sign cz .t21 s t
 184  else 0
 185
 186def m2OrbitCertZ13 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 187  if isOrbit .t13 s t then -slotAZ13 cz s t * slotKppOrbit kernel13Sign cz .t13 s t
 188  else 0
 189
 190def m2OrbitCertZ31 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 191  if isOrbit .t31 s t then -slotAZ31 cz s t * slotKppOrbit kernel13Sign cz .t31 s t
 192  else 0
 193
 194def m2OrbitCertZ22 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 195  if isOrbit .t22 s t then -slotAZ22 cz s t * slotKppOrbit kernel22Sign cz .t22 s t
 196  else 0
 197
 198/-! ## §4. Slot coefficient = certificate / denom -/
 199
 200private lemma sqrt2_mul_self : Real.sqrt 2 * Real.sqrt 2 = (2 : ℝ) := by
 201  simpa [pow_two] using Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)
 202
 203private lemma sqrt3_mul_self : Real.sqrt 3 * Real.sqrt 3 = (3 : ℝ) := by
 204  simpa [pow_two] using Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)
 205
 206private lemma radical2_slot_arith (AZ Kpp : ℤ) :
 207    Real.sqrt 2 * (AZ : ℝ) / 8 *
 208        (-(1 / 2 : ℝ) * (Real.sqrt 2 * (Kpp : ℝ) / 8)) =
 209      ((-AZ * Kpp : ℤ) : ℝ) / 64 := by
 210  have hs := sqrt2_mul_self
 211  ring_nf
 212  rw [show (Real.sqrt 2) ^ 2 = (2 : ℝ) by simpa [pow_two] using hs]
 213  push_cast; ring
 214
 215private lemma radical3_slot_arith (AZ Kpp : ℤ) :
 216    Real.sqrt 3 * (AZ : ℝ) / 12 *
 217        (-(1 / 2 : ℝ) * (Real.sqrt 3 * (Kpp : ℝ) / 4)) =
 218      ((-AZ * Kpp : ℤ) : ℝ) / 32 := by
 219  have hs := sqrt3_mul_self
 220  ring_nf
 221  rw [show (Real.sqrt 3) ^ 2 = (3 : ℝ) by simpa [pow_two] using hs]
 222  push_cast; ring
 223
 224private lemma area_push_sqrt2 (areaZ : Fin 15 → ℤ) (cz : Fin 15 → ℤ)
 225    (p : Fin 24) (H : Mat4) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
 226    (area : Fin 15 → ℝ)
 227    (harea : ∀ d, area d = Real.sqrt 2 * (areaZ d : ℝ) / 8) :
 228    (∑ d0 : Fin 15, area d0 * classCoeff H (permClass p d0)) =
 229      Real.sqrt 2 *
 230        (∑ d0 : Fin 15, areaZ d0 * cz (permClass p d0) : ℤ) / 8 := by
 231  simp_rw [harea, hH]
 232  calc
 233    (∑ d0 : Fin 15,
 234        Real.sqrt 2 * (areaZ d0 : ℝ) / 8 * (cz (permClass p d0) : ℝ)) =
 235        Real.sqrt 2 / 8 *
 236          ∑ d0 : Fin 15,
 237            (areaZ d0 : ℝ) * (cz (permClass p d0) : ℝ) := by
 238      refine Eq.trans ?_ (Finset.mul_sum _ _ _).symm
 239      refine Finset.sum_congr rfl fun d0 _ => by ring
 240    _ = Real.sqrt 2 *
 241          (∑ d0 : Fin 15, areaZ d0 * cz (permClass p d0) : ℤ) / 8 := by
 242      rw [Int.cast_sum]
 243      push_cast; ring
 244
 245private lemma area_push_sqrt3 (areaZ : Fin 15 → ℤ) (cz : Fin 15 → ℤ)
 246    (p : Fin 24) (H : Mat4) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
 247    (area : Fin 15 → ℝ)
 248    (harea : ∀ d, area d = Real.sqrt 3 * (areaZ d : ℝ) / 12) :
 249    (∑ d0 : Fin 15, area d0 * classCoeff H (permClass p d0)) =
 250      Real.sqrt 3 *
 251        (∑ d0 : Fin 15, areaZ d0 * cz (permClass p d0) : ℤ) / 12 := by
 252  simp_rw [harea, hH]
 253  calc
 254    (∑ d0 : Fin 15,
 255        Real.sqrt 3 * (areaZ d0 : ℝ) / 12 * (cz (permClass p d0) : ℝ)) =
 256        Real.sqrt 3 / 12 *
 257          ∑ d0 : Fin 15,
 258            (areaZ d0 : ℝ) * (cz (permClass p d0) : ℝ) := by
 259      refine Eq.trans ?_ (Finset.mul_sum _ _ _).symm
 260      refine Finset.sum_congr rfl fun d0 _ => by ring
 261    _ = Real.sqrt 3 *
 262          (∑ d0 : Fin 15, areaZ d0 * cz (permClass p d0) : ℤ) / 12 := by
 263      rw [Int.cast_sum]
 264      push_cast; ring
 265
 266private lemma ker_push_sqrt2_half (cz : Fin 15 → ℤ) (p : Fin 24)
 267    (H : Mat4) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
 268    (s : Fin 24) (t : Fin 10) :
 269    (∑ d0 : Fin 15,
 270        ReggeHinge4DStarKernel12.fullStarClassKernel d0 *
 271          classCoeff H (permClass p d0) *
 272            (phaseScaleDir symbolDir (hingeBase s t) (permClass p d0)) ^ 2) =
 273      Real.sqrt 2 *
 274        (∑ d0 : Fin 15,
 275            kernel12Sign d0 * cz (permClass p d0) *
 276              ((phase2Nat s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 8 := by
 277  simp_rw [kernel12_eq_sign, hH, phaseScaleDir_symbolDir, phaseScale_eq_phase2Nat]
 278  calc
 279    (∑ d0 : Fin 15,
 280        ((kernel12Sign d0 : ℝ) * (Real.sqrt 2 / 2)) *
 281          (cz (permClass p d0) : ℝ) *
 282            (((phase2Nat s t (permClass p d0) : ℕ) : ℝ) / 2) ^ 2) =
 283        Real.sqrt 2 / 8 *
 284          ∑ d0 : Fin 15,
 285            (kernel12Sign d0 : ℝ) * (cz (permClass p d0) : ℝ) *
 286              ((phase2Nat s t (permClass p d0) : ℕ) : ℝ) ^ 2 := by
 287      refine Eq.trans ?_ (Finset.mul_sum _ _ _).symm
 288      refine Finset.sum_congr rfl fun d0 _ => by ring
 289    _ = Real.sqrt 2 *
 290          (∑ d0 : Fin 15,
 291              kernel12Sign d0 * cz (permClass p d0) *
 292                ((phase2Nat s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 8 := by
 293      rw [Int.cast_sum]
 294      push_cast; ring
 295
 296private lemma ker_push_sqrt3 (cz : Fin 15 → ℤ) (p : Fin 24)
 297    (H : Mat4) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
 298    (s : Fin 24) (t : Fin 10) :
 299    (∑ d0 : Fin 15,
 300        ReggeHinge4DStarKernel13.fullStarClassKernel d0 *
 301          classCoeff H (permClass p d0) *
 302            (phaseScaleDir symbolDir (hingeBase s t) (permClass p d0)) ^ 2) =
 303      Real.sqrt 3 *
 304        (∑ d0 : Fin 15,
 305            kernel13Sign d0 * cz (permClass p d0) *
 306              ((phase2Nat s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 4 := by
 307  simp_rw [kernel13_eq_sign, hH, phaseScaleDir_symbolDir, phaseScale_eq_phase2Nat]
 308  calc
 309    (∑ d0 : Fin 15,
 310        ((kernel13Sign d0 : ℝ) * Real.sqrt 3) *
 311          (cz (permClass p d0) : ℝ) *
 312            (((phase2Nat s t (permClass p d0) : ℕ) : ℝ) / 2) ^ 2) =
 313        Real.sqrt 3 / 4 *
 314          ∑ d0 : Fin 15,
 315            (kernel13Sign d0 : ℝ) * (cz (permClass p d0) : ℝ) *
 316              ((phase2Nat s t (permClass p d0) : ℕ) : ℝ) ^ 2 := by
 317      refine Eq.trans ?_ (Finset.mul_sum _ _ _).symm
 318      refine Finset.sum_congr rfl fun d0 _ => by ring
 319    _ = Real.sqrt 3 *
 320          (∑ d0 : Fin 15,
 321              kernel13Sign d0 * cz (permClass p d0) *
 322                ((phase2Nat s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 4 := by
 323      rw [Int.cast_sum]
 324      push_cast; ring
 325
 326theorem m2TransportedOrbitSlotCoeff_t12_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 327    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 328    m2TransportedOrbitSlotCoeff .t12 H symbolDir s t =
 329      (m2OrbitCertZ12 cz s t : ℝ) / 64 := by
 330  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
 331    m2OrbitCertZ12
 332  by_cases ht : isOrbit .t12 s t
 333  · simp only [ht, ite_true]
 334    set p := orbitCoveringPerm .t12 s t with hp
 335    have hA :
 336        (∑ d : Fin 15, slotOrbitAreaCov .t12 s t d * classCoeff H d) =
 337          Real.sqrt 2 * (slotAZ12 cz s t : ℝ) / 8 := by
 338      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 339      rw [sum_mul_pushforward, ← hp]
 340      simpa [slotAZ12, hp] using
 341        area_push_sqrt2 area12Z cz p H hH areaCov12 areaCov12_eq_z
 342    have hK :
 343        (∑ d : Fin 15,
 344            slotOrbitDeficitKer .t12 s t d * classCoeff H d *
 345              (phaseScaleDir symbolDir (hingeBase s t) d) ^ 2) =
 346          Real.sqrt 2 * (slotKppOrbit kernel12Sign cz .t12 s t : ℝ) / 8 := by
 347      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel]
 348      rw [sum_mul_pushforward_weighted, ← hp]
 349      simpa [slotKppOrbit, hp] using ker_push_sqrt2_half cz p H hH s t
 350    rw [hA, hK]
 351    exact radical2_slot_arith (slotAZ12 cz s t)
 352      (slotKppOrbit kernel12Sign cz .t12 s t)
 353  · simp [ht]
 354
 355theorem m2TransportedOrbitSlotCoeff_t21_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 356    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 357    m2TransportedOrbitSlotCoeff .t21 H symbolDir s t =
 358      (m2OrbitCertZ21 cz s t : ℝ) / 64 := by
 359  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
 360    m2OrbitCertZ21
 361  by_cases ht : isOrbit .t21 s t
 362  · simp only [ht, ite_true]
 363    set p := orbitCoveringPerm .t21 s t with hp
 364    have hA :
 365        (∑ d : Fin 15, slotOrbitAreaCov .t21 s t d * classCoeff H d) =
 366          Real.sqrt 2 * (slotAZ21 cz s t : ℝ) / 8 := by
 367      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 368      rw [sum_mul_pushforward, ← hp]
 369      simpa [slotAZ21, hp] using
 370        area_push_sqrt2 area21Z cz p H hH areaCov21 areaCov21_eq_z
 371    have hK :
 372        (∑ d : Fin 15,
 373            slotOrbitDeficitKer .t21 s t d * classCoeff H d *
 374              (phaseScaleDir symbolDir (hingeBase s t) d) ^ 2) =
 375          Real.sqrt 2 * (slotKppOrbit kernel12Sign cz .t21 s t : ℝ) / 8 := by
 376      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel,
 377        kernel21]
 378      rw [sum_mul_pushforward_weighted, ← hp]
 379      simpa [slotKppOrbit, hp] using ker_push_sqrt2_half cz p H hH s t
 380    rw [hA, hK]
 381    exact radical2_slot_arith (slotAZ21 cz s t)
 382      (slotKppOrbit kernel12Sign cz .t21 s t)
 383  · simp [ht]
 384
 385theorem m2TransportedOrbitSlotCoeff_t13_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 386    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 387    m2TransportedOrbitSlotCoeff .t13 H symbolDir s t =
 388      (m2OrbitCertZ13 cz s t : ℝ) / 32 := by
 389  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
 390    m2OrbitCertZ13
 391  by_cases ht : isOrbit .t13 s t
 392  · simp only [ht, ite_true]
 393    set p := orbitCoveringPerm .t13 s t with hp
 394    have hA :
 395        (∑ d : Fin 15, slotOrbitAreaCov .t13 s t d * classCoeff H d) =
 396          Real.sqrt 3 * (slotAZ13 cz s t : ℝ) / 12 := by
 397      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 398      rw [sum_mul_pushforward, ← hp]
 399      simpa [slotAZ13, hp] using
 400        area_push_sqrt3 area13Z cz p H hH areaCov13 areaCov13_eq_z
 401    have hK :
 402        (∑ d : Fin 15,
 403            slotOrbitDeficitKer .t13 s t d * classCoeff H d *
 404              (phaseScaleDir symbolDir (hingeBase s t) d) ^ 2) =
 405          Real.sqrt 3 * (slotKppOrbit kernel13Sign cz .t13 s t : ℝ) / 4 := by
 406      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel]
 407      rw [sum_mul_pushforward_weighted, ← hp]
 408      simpa [slotKppOrbit, hp] using ker_push_sqrt3 cz p H hH s t
 409    rw [hA, hK]
 410    exact radical3_slot_arith (slotAZ13 cz s t)
 411      (slotKppOrbit kernel13Sign cz .t13 s t)
 412  · simp [ht]
 413
 414theorem m2TransportedOrbitSlotCoeff_t31_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 415    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 416    m2TransportedOrbitSlotCoeff .t31 H symbolDir s t =
 417      (m2OrbitCertZ31 cz s t : ℝ) / 32 := by
 418  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
 419    m2OrbitCertZ31
 420  by_cases ht : isOrbit .t31 s t
 421  · simp only [ht, ite_true]
 422    set p := orbitCoveringPerm .t31 s t with hp
 423    have hA :
 424        (∑ d : Fin 15, slotOrbitAreaCov .t31 s t d * classCoeff H d) =
 425          Real.sqrt 3 * (slotAZ31 cz s t : ℝ) / 12 := by
 426      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 427      rw [sum_mul_pushforward, ← hp]
 428      simpa [slotAZ31, hp] using
 429        area_push_sqrt3 area31Z cz p H hH areaCov31 areaCov31_eq_z
 430    have hK :
 431        (∑ d : Fin 15,
 432            slotOrbitDeficitKer .t31 s t d * classCoeff H d *
 433              (phaseScaleDir symbolDir (hingeBase s t) d) ^ 2) =
 434          Real.sqrt 3 * (slotKppOrbit kernel13Sign cz .t31 s t : ℝ) / 4 := by
 435      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel,
 436        kernel31]
 437      rw [sum_mul_pushforward_weighted, ← hp]
 438      simpa [slotKppOrbit, hp] using ker_push_sqrt3 cz p H hH s t
 439    rw [hA, hK]
 440    exact radical3_slot_arith (slotAZ31 cz s t)
 441      (slotKppOrbit kernel13Sign cz .t31 s t)
 442  · simp [ht]
 443
 444theorem m2TransportedOrbitSlotCoeff_t22_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 445    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 446    m2TransportedOrbitSlotCoeff .t22 H symbolDir s t =
 447      (m2OrbitCertZ22 cz s t : ℝ) / 32 := by
 448  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
 449    m2OrbitCertZ22
 450  by_cases ht : isOrbit .t22 s t
 451  · simp only [ht, ite_true]
 452    set p := orbitCoveringPerm .t22 s t with hp
 453    have hA :
 454        (∑ d : Fin 15, slotOrbitAreaCov .t22 s t d * classCoeff H d) =
 455          (slotAZ22 cz s t : ℝ) / 4 := by
 456      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 457      rw [sum_mul_pushforward, ← hp]
 458      unfold slotAZ22
 459      simp_rw [areaCov22_eq_z, hH]
 460      calc
 461        (∑ d0 : Fin 15,
 462            (area22Z d0 : ℝ) / 4 * (cz (permClass p d0) : ℝ)) =
 463            (∑ d0 : Fin 15, (area22Z d0 : ℝ) * (cz (permClass p d0) : ℝ)) /
 464              4 := by
 465          rw [Finset.sum_div]
 466          refine Finset.sum_congr rfl fun d0 _ => by ring
 467        _ = (∑ d0 : Fin 15, area22Z d0 * cz (permClass p d0) : ℤ) / 4 := by
 468          rw [Int.cast_sum]; push_cast; rfl
 469    have hK :
 470        (∑ d : Fin 15,
 471            slotOrbitDeficitKer .t22 s t d * classCoeff H d *
 472              (phaseScaleDir symbolDir (hingeBase s t) d) ^ 2) =
 473          (slotKppOrbit kernel22Sign cz .t22 s t : ℝ) / 4 := by
 474      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel]
 475      rw [sum_mul_pushforward_weighted, ← hp]
 476      unfold slotKppOrbit
 477      simp_rw [kernel22_eq_sign, hH, phaseScaleDir_symbolDir,
 478        phaseScale_eq_phase2Nat]
 479      calc
 480        (∑ d0 : Fin 15,
 481            (kernel22Sign d0 : ℝ) * (cz (permClass p d0) : ℝ) *
 482              (((phase2Nat s t (permClass p d0) : ℕ) : ℝ) / 2) ^ 2) =
 483            (∑ d0 : Fin 15,
 484                (kernel22Sign d0 : ℝ) * (cz (permClass p d0) : ℝ) *
 485                  ((phase2Nat s t (permClass p d0) : ℕ) : ℝ) ^ 2) / 4 := by
 486          rw [Finset.sum_div]
 487          refine Finset.sum_congr rfl fun d0 _ => by ring
 488        _ = (∑ d0 : Fin 15,
 489                kernel22Sign d0 * cz (permClass p d0) *
 490                  ((phase2Nat s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 4 := by
 491          rw [Int.cast_sum]; push_cast; rfl
 492    rw [hA, hK]
 493    push_cast; ring
 494  · simp [ht]
 495
 496/-! ## §5. Decidable integer sums -/
 497
 498set_option maxRecDepth 12000 in
 499set_option maxHeartbeats 8000000 in
 500theorem sum_m2OrbitCertZ12_axis :
 501    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ12 axisTTPlusCoeffZ s t) =
 502      (128 : ℤ) := by
 503  decide
 504
 505set_option maxRecDepth 12000 in
 506set_option maxHeartbeats 8000000 in
 507theorem sum_m2OrbitCertZ21_axis :
 508    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ21 axisTTPlusCoeffZ s t) =
 509      (0 : ℤ) := by
 510  decide
 511
 512set_option maxRecDepth 12000 in
 513set_option maxHeartbeats 8000000 in
 514theorem sum_m2OrbitCertZ13_axis :
 515    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ13 axisTTPlusCoeffZ s t) =
 516      (-48 : ℤ) := by
 517  decide
 518
 519set_option maxRecDepth 12000 in
 520set_option maxHeartbeats 8000000 in
 521theorem sum_m2OrbitCertZ31_axis :
 522    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ31 axisTTPlusCoeffZ s t) =
 523      (0 : ℤ) := by
 524  decide
 525
 526set_option maxRecDepth 12000 in
 527set_option maxHeartbeats 8000000 in
 528theorem sum_m2OrbitCertZ22_axis :
 529    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ22 axisTTPlusCoeffZ s t) =
 530      (0 : ℤ) := by
 531  decide
 532
 533set_option maxRecDepth 12000 in
 534set_option maxHeartbeats 8000000 in
 535theorem sum_m2OrbitCertZ12_gauge :
 536    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ12 decoyGaugeCoeffZ s t) =
 537      (0 : ℤ) := by
 538  decide
 539
 540set_option maxRecDepth 12000 in
 541set_option maxHeartbeats 8000000 in
 542theorem sum_m2OrbitCertZ21_gauge :
 543    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ21 decoyGaugeCoeffZ s t) =
 544      (0 : ℤ) := by
 545  decide
 546
 547set_option maxRecDepth 12000 in
 548set_option maxHeartbeats 8000000 in
 549theorem sum_m2OrbitCertZ13_gauge :
 550    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ13 decoyGaugeCoeffZ s t) =
 551      (0 : ℤ) := by
 552  decide
 553
 554set_option maxRecDepth 12000 in
 555set_option maxHeartbeats 8000000 in
 556theorem sum_m2OrbitCertZ31_gauge :
 557    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ31 decoyGaugeCoeffZ s t) =
 558      (0 : ℤ) := by
 559  decide
 560
 561set_option maxRecDepth 12000 in
 562set_option maxHeartbeats 8000000 in
 563theorem sum_m2OrbitCertZ22_gauge :
 564    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ22 decoyGaugeCoeffZ s t) =
 565      (0 : ℤ) := by
 566  decide
 567
 568/-! ## §6. Per-orbit moment evaluations -/
 569
 570theorem m2TransportedOrbitMoment_t12_axis :
 571    m2TransportedOrbitMoment .t12 axisTTPlus symbolDir = (2 : ℝ) := by
 572  unfold m2TransportedOrbitMoment
 573  simp_rw [m2TransportedOrbitSlotCoeff_t12_eq_cert axisTTPlus axisTTPlusCoeffZ
 574    classCoeff_axisTTPlus_int]
 575  have hsum :
 576      (∑ s : Fin 24, ∑ t : Fin 10,
 577          (m2OrbitCertZ12 axisTTPlusCoeffZ s t : ℝ)) = (128 : ℝ) := by
 578    simpa [Int.cast_sum] using
 579      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ12_axis
 580  rw [sum_div_const_st, hsum]; norm_num
 581
 582theorem m2TransportedOrbitMoment_t21_axis :
 583    m2TransportedOrbitMoment .t21 axisTTPlus symbolDir = (0 : ℝ) := by
 584  unfold m2TransportedOrbitMoment
 585  simp_rw [m2TransportedOrbitSlotCoeff_t21_eq_cert axisTTPlus axisTTPlusCoeffZ
 586    classCoeff_axisTTPlus_int]
 587  have hsum :
 588      (∑ s : Fin 24, ∑ t : Fin 10,
 589          (m2OrbitCertZ21 axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
 590    simpa [Int.cast_sum] using
 591      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ21_axis
 592  rw [sum_div_const_st, hsum]; norm_num
 593
 594theorem m2TransportedOrbitMoment_t13_axis :
 595    m2TransportedOrbitMoment .t13 axisTTPlus symbolDir = (-3 / 2 : ℝ) := by
 596  unfold m2TransportedOrbitMoment
 597  simp_rw [m2TransportedOrbitSlotCoeff_t13_eq_cert axisTTPlus axisTTPlusCoeffZ
 598    classCoeff_axisTTPlus_int]
 599  have hsum :
 600      (∑ s : Fin 24, ∑ t : Fin 10,
 601          (m2OrbitCertZ13 axisTTPlusCoeffZ s t : ℝ)) = (-48 : ℝ) := by
 602    simpa [Int.cast_sum] using
 603      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ13_axis
 604  rw [sum_div_const_st, hsum]; norm_num
 605
 606theorem m2TransportedOrbitMoment_t31_axis :
 607    m2TransportedOrbitMoment .t31 axisTTPlus symbolDir = (0 : ℝ) := by
 608  unfold m2TransportedOrbitMoment
 609  simp_rw [m2TransportedOrbitSlotCoeff_t31_eq_cert axisTTPlus axisTTPlusCoeffZ
 610    classCoeff_axisTTPlus_int]
 611  have hsum :
 612      (∑ s : Fin 24, ∑ t : Fin 10,
 613          (m2OrbitCertZ31 axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
 614    simpa [Int.cast_sum] using
 615      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ31_axis
 616  rw [sum_div_const_st, hsum]; norm_num
 617
 618theorem m2TransportedOrbitMoment_t22_axis :
 619    m2TransportedOrbitMoment .t22 axisTTPlus symbolDir = (0 : ℝ) := by
 620  unfold m2TransportedOrbitMoment
 621  simp_rw [m2TransportedOrbitSlotCoeff_t22_eq_cert axisTTPlus axisTTPlusCoeffZ
 622    classCoeff_axisTTPlus_int]
 623  have hsum :
 624      (∑ s : Fin 24, ∑ t : Fin 10,
 625          (m2OrbitCertZ22 axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
 626    simpa [Int.cast_sum] using
 627      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ22_axis
 628  rw [sum_div_const_st, hsum]; norm_num
 629
 630theorem m2TransportedOrbitMoment_t11_axis :
 631    m2TransportedOrbitMoment .t11 axisTTPlus symbolDir = (-3 : ℝ) := by
 632  rw [m2TransportedOrbitMoment_t11, m2Symbol_axisTTPlus]
 633
 634/-! ## §7. All-orbit axis evaluation -/
 635
 636theorem m2TransportedAllOrbitMoment_axisTTPlus_symbolDir :
 637    m2TransportedAllOrbitMoment axisTTPlus symbolDir = (-5 / 2 : ℝ) := by
 638  unfold m2TransportedAllOrbitMoment
 639  rw [sum_six_orbits]
 640  rw [m2TransportedOrbitMoment_t11_axis, m2TransportedOrbitMoment_t12_axis,
 641    m2TransportedOrbitMoment_t21_axis, m2TransportedOrbitMoment_t13_axis,
 642    m2TransportedOrbitMoment_t31_axis, m2TransportedOrbitMoment_t22_axis]
 643  norm_num
 644
 645theorem M2TransportedAllOrbitAxisSymbolDirEvalOpen_holds :
 646    M2TransportedAllOrbitAxisSymbolDirEvalOpen :=
 647  m2TransportedAllOrbitMoment_axisTTPlus_symbolDir
 648
 649/-! ## §8. Gauge vanishing -/
 650
 651theorem m2TransportedOrbitMoment_t12_gauge :
 652    m2TransportedOrbitMoment .t12 decoyGauge symbolDir = (0 : ℝ) := by
 653  unfold m2TransportedOrbitMoment
 654  simp_rw [m2TransportedOrbitSlotCoeff_t12_eq_cert decoyGauge decoyGaugeCoeffZ
 655    classCoeff_decoyGauge_int]
 656  have hsum :
 657      (∑ s : Fin 24, ∑ t : Fin 10,
 658          (m2OrbitCertZ12 decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 659    simpa [Int.cast_sum] using
 660      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ12_gauge
 661  rw [sum_div_const_st, hsum]; norm_num
 662
 663theorem m2TransportedOrbitMoment_t21_gauge :
 664    m2TransportedOrbitMoment .t21 decoyGauge symbolDir = (0 : ℝ) := by
 665  unfold m2TransportedOrbitMoment
 666  simp_rw [m2TransportedOrbitSlotCoeff_t21_eq_cert decoyGauge decoyGaugeCoeffZ
 667    classCoeff_decoyGauge_int]
 668  have hsum :
 669      (∑ s : Fin 24, ∑ t : Fin 10,
 670          (m2OrbitCertZ21 decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 671    simpa [Int.cast_sum] using
 672      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ21_gauge
 673  rw [sum_div_const_st, hsum]; norm_num
 674
 675theorem m2TransportedOrbitMoment_t13_gauge :
 676    m2TransportedOrbitMoment .t13 decoyGauge symbolDir = (0 : ℝ) := by
 677  unfold m2TransportedOrbitMoment
 678  simp_rw [m2TransportedOrbitSlotCoeff_t13_eq_cert decoyGauge decoyGaugeCoeffZ
 679    classCoeff_decoyGauge_int]
 680  have hsum :
 681      (∑ s : Fin 24, ∑ t : Fin 10,
 682          (m2OrbitCertZ13 decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 683    simpa [Int.cast_sum] using
 684      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ13_gauge
 685  rw [sum_div_const_st, hsum]; norm_num
 686
 687theorem m2TransportedOrbitMoment_t31_gauge :
 688    m2TransportedOrbitMoment .t31 decoyGauge symbolDir = (0 : ℝ) := by
 689  unfold m2TransportedOrbitMoment
 690  simp_rw [m2TransportedOrbitSlotCoeff_t31_eq_cert decoyGauge decoyGaugeCoeffZ
 691    classCoeff_decoyGauge_int]
 692  have hsum :
 693      (∑ s : Fin 24, ∑ t : Fin 10,
 694          (m2OrbitCertZ31 decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 695    simpa [Int.cast_sum] using
 696      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ31_gauge
 697  rw [sum_div_const_st, hsum]; norm_num
 698
 699theorem m2TransportedOrbitMoment_t22_gauge :
 700    m2TransportedOrbitMoment .t22 decoyGauge symbolDir = (0 : ℝ) := by
 701  unfold m2TransportedOrbitMoment
 702  simp_rw [m2TransportedOrbitSlotCoeff_t22_eq_cert decoyGauge decoyGaugeCoeffZ
 703    classCoeff_decoyGauge_int]
 704  have hsum :
 705      (∑ s : Fin 24, ∑ t : Fin 10,
 706          (m2OrbitCertZ22 decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 707    simpa [Int.cast_sum] using
 708      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ22_gauge
 709  rw [sum_div_const_st, hsum]; norm_num
 710
 711theorem m2TransportedOrbitMoment_t11_gauge :
 712    m2TransportedOrbitMoment .t11 decoyGauge symbolDir = (0 : ℝ) := by
 713  rw [m2TransportedOrbitMoment_t11, m2Symbol_decoyGauge]
 714
 715theorem m2TransportedAllOrbitMoment_decoyGauge_symbolDir :
 716    m2TransportedAllOrbitMoment decoyGauge symbolDir = (0 : ℝ) := by
 717  unfold m2TransportedAllOrbitMoment
 718  rw [sum_six_orbits]
 719  rw [m2TransportedOrbitMoment_t11_gauge, m2TransportedOrbitMoment_t12_gauge,
 720    m2TransportedOrbitMoment_t21_gauge, m2TransportedOrbitMoment_t13_gauge,
 721    m2TransportedOrbitMoment_t31_gauge, m2TransportedOrbitMoment_t22_gauge]
 722  ring
 723
 724/-! ## §9. Distinct-hinge weight `1/r_τ` -/
 725
 726theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir :
 727    m2TransportedAllOrbitMomentDistinctHinge axisTTPlus symbolDir =
 728      (-1 / 4 : ℝ) := by
 729  unfold m2TransportedAllOrbitMomentDistinctHinge
 730  rw [sum_six_orbits]
 731  simp only [orbitStarSize]
 732  rw [m2TransportedOrbitMoment_t11_axis, m2TransportedOrbitMoment_t12_axis,
 733    m2TransportedOrbitMoment_t21_axis, m2TransportedOrbitMoment_t13_axis,
 734    m2TransportedOrbitMoment_t31_axis, m2TransportedOrbitMoment_t22_axis]
 735  -- `-3/6 + 2/4 + (-3/2)/6 + 0 + 0 + 0 = -1/4`
 736  norm_num
 737
 738theorem M2DistinctHingeAxisSymbolDirEvalOpen_holds :
 739    M2DistinctHingeAxisSymbolDirEvalOpen :=
 740  m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir
 741
 742theorem m2TransportedAllOrbitMomentDistinctHinge_decoyGauge_symbolDir :
 743    m2TransportedAllOrbitMomentDistinctHinge decoyGauge symbolDir =
 744      (0 : ℝ) := by
 745  unfold m2TransportedAllOrbitMomentDistinctHinge
 746  rw [sum_six_orbits]
 747  simp only [orbitStarSize]
 748  rw [m2TransportedOrbitMoment_t11_gauge, m2TransportedOrbitMoment_t12_gauge,
 749    m2TransportedOrbitMoment_t21_gauge, m2TransportedOrbitMoment_t13_gauge,
 750    m2TransportedOrbitMoment_t31_gauge, m2TransportedOrbitMoment_t22_gauge]
 751  ring
 752
 753/-- Frobenius-normalized axis plus: factor `(1/√2)² = 1/2` on the
 754distinct-hinge raw `-1/4` yields raw moment `-1/8`.  After `/|symbolDir|²`
 755the continuum face is `-1/16`; EH Tendsto to `-1/4` remains OPEN
 756(residual factor 4; no fitted rescale). -/
 757theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTPlusNormalized_symbolDir :
 758    m2TransportedAllOrbitMomentDistinctHinge
 759        ((Real.sqrt 2)⁻¹ • axisTTPlus) symbolDir =
 760      (-1 / 8 : ℝ) := by
 761  rw [m2TransportedAllOrbitMomentDistinctHinge_smul,
 762    m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir,
 763    inv_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
 764  norm_num
 765
 766/-! ## §10. Axis TT cross certificates on `symbolDir` -/
 767
 768set_option maxRecDepth 12000 in
 769set_option maxHeartbeats 8000000 in
 770theorem sum_m2SlotCertZ_cross :
 771    (∑ s : Fin 24, ∑ t : Fin 10, m2SlotCertZ axisTTCrossCoeffZ s t) =
 772      (0 : ℤ) := by
 773  decide
 774
 775set_option maxRecDepth 12000 in
 776set_option maxHeartbeats 8000000 in
 777theorem sum_m2OrbitCertZ12_cross :
 778    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ12 axisTTCrossCoeffZ s t) =
 779      (-256 : ℤ) := by
 780  decide
 781
 782set_option maxRecDepth 12000 in
 783set_option maxHeartbeats 8000000 in
 784theorem sum_m2OrbitCertZ21_cross :
 785    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ21 axisTTCrossCoeffZ s t) =
 786      (-64 : ℤ) := by
 787  decide
 788
 789set_option maxRecDepth 12000 in
 790set_option maxHeartbeats 8000000 in
 791theorem sum_m2OrbitCertZ13_cross :
 792    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ13 axisTTCrossCoeffZ s t) =
 793      (48 : ℤ) := by
 794  decide
 795
 796set_option maxRecDepth 12000 in
 797set_option maxHeartbeats 8000000 in
 798theorem sum_m2OrbitCertZ31_cross :
 799    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ31 axisTTCrossCoeffZ s t) =
 800      (48 : ℤ) := by
 801  decide
 802
 803set_option maxRecDepth 12000 in
 804set_option maxHeartbeats 8000000 in
 805theorem sum_m2OrbitCertZ22_cross :
 806    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ22 axisTTCrossCoeffZ s t) =
 807      (64 : ℤ) := by
 808  decide
 809
 810theorem m2Symbol_axisTTCross : m2Symbol axisTTCross = (0 : ℝ) := by
 811  unfold m2Symbol
 812  simp_rw [m2SlotCoeff_eq_cert axisTTCross axisTTCrossCoeffZ
 813    classCoeff_axisTTCross_int]
 814  have hsum :
 815      (∑ s : Fin 24, ∑ t : Fin 10,
 816          (m2SlotCertZ axisTTCrossCoeffZ s t : ℝ)) = (0 : ℝ) := by
 817    simpa [Int.cast_sum] using
 818      congrArg (fun n : ℤ => (n : ℝ)) sum_m2SlotCertZ_cross
 819  rw [sum_div_const_st, hsum]; norm_num
 820
 821theorem m2TransportedOrbitMoment_t11_cross :
 822    m2TransportedOrbitMoment .t11 axisTTCross symbolDir = (0 : ℝ) := by
 823  rw [m2TransportedOrbitMoment_t11, m2Symbol_axisTTCross]
 824
 825theorem m2TransportedOrbitMoment_t12_cross :
 826    m2TransportedOrbitMoment .t12 axisTTCross symbolDir = (-4 : ℝ) := by
 827  unfold m2TransportedOrbitMoment
 828  simp_rw [m2TransportedOrbitSlotCoeff_t12_eq_cert axisTTCross axisTTCrossCoeffZ
 829    classCoeff_axisTTCross_int]
 830  have hsum :
 831      (∑ s : Fin 24, ∑ t : Fin 10,
 832          (m2OrbitCertZ12 axisTTCrossCoeffZ s t : ℝ)) = (-256 : ℝ) := by
 833    simpa [Int.cast_sum] using
 834      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ12_cross
 835  rw [sum_div_const_st, hsum]; norm_num
 836
 837theorem m2TransportedOrbitMoment_t21_cross :
 838    m2TransportedOrbitMoment .t21 axisTTCross symbolDir = (-1 : ℝ) := by
 839  unfold m2TransportedOrbitMoment
 840  simp_rw [m2TransportedOrbitSlotCoeff_t21_eq_cert axisTTCross axisTTCrossCoeffZ
 841    classCoeff_axisTTCross_int]
 842  have hsum :
 843      (∑ s : Fin 24, ∑ t : Fin 10,
 844          (m2OrbitCertZ21 axisTTCrossCoeffZ s t : ℝ)) = (-64 : ℝ) := by
 845    simpa [Int.cast_sum] using
 846      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ21_cross
 847  rw [sum_div_const_st, hsum]; norm_num
 848
 849theorem m2TransportedOrbitMoment_t13_cross :
 850    m2TransportedOrbitMoment .t13 axisTTCross symbolDir = (3 / 2 : ℝ) := by
 851  unfold m2TransportedOrbitMoment
 852  simp_rw [m2TransportedOrbitSlotCoeff_t13_eq_cert axisTTCross axisTTCrossCoeffZ
 853    classCoeff_axisTTCross_int]
 854  have hsum :
 855      (∑ s : Fin 24, ∑ t : Fin 10,
 856          (m2OrbitCertZ13 axisTTCrossCoeffZ s t : ℝ)) = (48 : ℝ) := by
 857    simpa [Int.cast_sum] using
 858      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ13_cross
 859  rw [sum_div_const_st, hsum]; norm_num
 860
 861theorem m2TransportedOrbitMoment_t31_cross :
 862    m2TransportedOrbitMoment .t31 axisTTCross symbolDir = (3 / 2 : ℝ) := by
 863  unfold m2TransportedOrbitMoment
 864  simp_rw [m2TransportedOrbitSlotCoeff_t31_eq_cert axisTTCross axisTTCrossCoeffZ
 865    classCoeff_axisTTCross_int]
 866  have hsum :
 867      (∑ s : Fin 24, ∑ t : Fin 10,
 868          (m2OrbitCertZ31 axisTTCrossCoeffZ s t : ℝ)) = (48 : ℝ) := by
 869    simpa [Int.cast_sum] using
 870      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ31_cross
 871  rw [sum_div_const_st, hsum]; norm_num
 872
 873theorem m2TransportedOrbitMoment_t22_cross :
 874    m2TransportedOrbitMoment .t22 axisTTCross symbolDir = (2 : ℝ) := by
 875  unfold m2TransportedOrbitMoment
 876  simp_rw [m2TransportedOrbitSlotCoeff_t22_eq_cert axisTTCross axisTTCrossCoeffZ
 877    classCoeff_axisTTCross_int]
 878  have hsum :
 879      (∑ s : Fin 24, ∑ t : Fin 10,
 880          (m2OrbitCertZ22 axisTTCrossCoeffZ s t : ℝ)) = (64 : ℝ) := by
 881    simpa [Int.cast_sum] using
 882      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ22_cross
 883  rw [sum_div_const_st, hsum]; norm_num
 884
 885/-- Raw all-orbit (unweighted) on cross / symbolDir is `0`
 886(`0-4-1+3/2+3/2+2`), unlike plus `-5/2`. -/
 887theorem m2TransportedAllOrbitMoment_axisTTCross_symbolDir :
 888    m2TransportedAllOrbitMoment axisTTCross symbolDir = (0 : ℝ) := by
 889  unfold m2TransportedAllOrbitMoment
 890  rw [sum_six_orbits]
 891  rw [m2TransportedOrbitMoment_t11_cross, m2TransportedOrbitMoment_t12_cross,
 892    m2TransportedOrbitMoment_t21_cross, m2TransportedOrbitMoment_t13_cross,
 893    m2TransportedOrbitMoment_t31_cross, m2TransportedOrbitMoment_t22_cross]
 894  norm_num
 895
 896/-- Distinct-hinge `1/r_τ` on cross / symbolDir equals frozen EH `-1/4`
 897(`0 + (-4)/4 + (-1)/4 + (3/2)/6 + (3/2)/6 + 2/4`), matching plus. -/
 898theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_symbolDir :
 899    m2TransportedAllOrbitMomentDistinctHinge axisTTCross symbolDir =
 900      (-1 / 4 : ℝ) := by
 901  unfold m2TransportedAllOrbitMomentDistinctHinge
 902  rw [sum_six_orbits]
 903  simp only [orbitStarSize]
 904  rw [m2TransportedOrbitMoment_t11_cross, m2TransportedOrbitMoment_t12_cross,
 905    m2TransportedOrbitMoment_t21_cross, m2TransportedOrbitMoment_t13_cross,
 906    m2TransportedOrbitMoment_t31_cross, m2TransportedOrbitMoment_t22_cross]
 907  norm_num
 908
 909/-- Formerly OPEN; now inhabited by the cross distinct-hinge certificate. -/
 910def M2DistinctHingeAxisTTCrossSymbolDirEvalOpen : Prop :=
 911  m2TransportedAllOrbitMomentDistinctHinge axisTTCross symbolDir =
 912    (-1 / 4 : ℝ)
 913
 914theorem M2DistinctHingeAxisTTCrossSymbolDirEvalOpen_holds :
 915    M2DistinctHingeAxisTTCrossSymbolDirEvalOpen :=
 916  m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_symbolDir
 917
 918theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTCrossNormalized_symbolDir :
 919    m2TransportedAllOrbitMomentDistinctHinge
 920        ((Real.sqrt 2)⁻¹ • axisTTCross) symbolDir =
 921      (-1 / 8 : ℝ) := by
 922  rw [m2TransportedAllOrbitMomentDistinctHinge_smul,
 923    m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_symbolDir,
 924    inv_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
 925  norm_num
 926
 927/-- Plus/cross agreement on the Frobenius-normalized distinct-hinge face. -/
 928theorem m2TransportedDistinctHinge_plus_cross_normalized_agree_symbolDir :
 929    m2TransportedAllOrbitMomentDistinctHinge
 930        ((Real.sqrt 2)⁻¹ • axisTTPlus) symbolDir =
 931      m2TransportedAllOrbitMomentDistinctHinge
 932        ((Real.sqrt 2)⁻¹ • axisTTCross) symbolDir := by
 933  rw [m2TransportedAllOrbitMomentDistinctHinge_axisTTPlusNormalized_symbolDir,
 934    m2TransportedAllOrbitMomentDistinctHinge_axisTTCrossNormalized_symbolDir]
 935
 936/-! ## §11. Axis-aligned ray `e0Dir = (1,0,0,0)`
 937
 938Integer phase scaffolding for the lattice axis.  Distinct-hinge moments
 939(THEOREM below): plus `0`, cross `-1/8`.  Continuum EH needs every
 940nonzero mode; this axis anisotropy is recorded as
 941`Regge4DContinuumIsotropyBlockedOnAxisMode` (OPEN, status false).
 942Geometric cause (MEASURED reading): TT support of plus/cross lives in
 943the bit-2/3 plane (`classCoeff` = `D₂−D₃` / `2 D₂ D₃`), while
 944`phaseScaleDir e0Dir` only sees coordinate 0, so the transported
 945cover does not mix the TT plane into the axis phase the way
 946`symbolDir = (1,1,0,0)` does.
 947-/
 948
 949def e0Dir : Fin 4 → ℝ
 950  | 0 => 1
 951  | _ => 0
 952
 953/-- Integer double-phase along `e0Dir`. -/
 954def phase2NatE0 (s : Fin 24) (t : Fin 10) (d : Fin 15) : ℕ :=
 955  2 * (if Nat.testBit (triangleVertexMasks s t).1 0 then 1 else 0) +
 956    (if classBit d 0 then 1 else 0)
 957
 958theorem phaseScaleDir_e0Dir (s : Fin 24) (t : Fin 10) (d : Fin 15) :
 959    phaseScaleDir e0Dir (hingeBase s t) d = (phase2NatE0 s t d : ℝ) / 2 := by
 960  unfold phaseScaleDir phase2NatE0 hingeBase maskCoord classDisp e0Dir
 961  simp only [Fin.sum_univ_four]
 962  by_cases h0 : Nat.testBit (triangleVertexMasks s t).1 0
 963  · by_cases d0 : classBit d 0 <;> simp [h0, d0] <;> ring
 964  · by_cases d0 : classBit d 0 <;> simp [h0, d0] <;> ring
 965
 966theorem e0Dir_normSq :
 967    (∑ i : Fin 4, e0Dir i * e0Dir i) = (1 : ℝ) := by
 968  simp [e0Dir, Fin.sum_univ_four]
 969
 970def slotKppOrbitE0 (sign : Fin 15 → ℤ) (cz : Fin 15 → ℤ)
 971    (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) : ℤ :=
 972  ∑ d0 : Fin 15,
 973    sign d0 * cz (permClass (orbitCoveringPerm ty s t) d0) *
 974      ((phase2NatE0 s t (permClass (orbitCoveringPerm ty s t) d0) : ℕ) : ℤ) ^ 2
 975
 976def m2OrbitCertZ12E0 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 977  if isOrbit .t12 s t then -slotAZ12 cz s t * slotKppOrbitE0 kernel12Sign cz .t12 s t
 978  else 0
 979
 980def m2OrbitCertZ21E0 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 981  if isOrbit .t21 s t then -slotAZ21 cz s t * slotKppOrbitE0 kernel12Sign cz .t21 s t
 982  else 0
 983
 984def m2OrbitCertZ13E0 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 985  if isOrbit .t13 s t then -slotAZ13 cz s t * slotKppOrbitE0 kernel13Sign cz .t13 s t
 986  else 0
 987
 988def m2OrbitCertZ31E0 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 989  if isOrbit .t31 s t then -slotAZ31 cz s t * slotKppOrbitE0 kernel13Sign cz .t31 s t
 990  else 0
 991
 992def m2OrbitCertZ22E0 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 993  if isOrbit .t22 s t then -slotAZ22 cz s t * slotKppOrbitE0 kernel22Sign cz .t22 s t
 994  else 0
 995
 996def slotKppZE0 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 997  ∑ d0 : Fin 15,
 998    kernel11Sign d0 * cz (permClass (slotTransportPerm s t) d0) *
 999      ((phase2NatE0 s t (permClass (slotTransportPerm s t) d0) : ℕ) : ℤ) ^ 2
1000
1001def m2SlotCertZE0 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
1002  if isT11 s t then -slotA0Z4 cz s t * slotKppZE0 cz s t else 0
1003
1004private lemma ker_push_sqrt2_half_e0 (cz : Fin 15 → ℤ) (p : Fin 24)
1005    (H : Mat4) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
1006    (s : Fin 24) (t : Fin 10) :
1007    (∑ d0 : Fin 15,
1008        ReggeHinge4DStarKernel12.fullStarClassKernel d0 *
1009          classCoeff H (permClass p d0) *
1010            (phaseScaleDir e0Dir (hingeBase s t) (permClass p d0)) ^ 2) =
1011      Real.sqrt 2 *
1012        (∑ d0 : Fin 15,
1013            kernel12Sign d0 * cz (permClass p d0) *
1014              ((phase2NatE0 s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 8 := by
1015  simp_rw [kernel12_eq_sign, hH, phaseScaleDir_e0Dir]
1016  calc
1017    (∑ d0 : Fin 15,
1018        ((kernel12Sign d0 : ℝ) * (Real.sqrt 2 / 2)) *
1019          (cz (permClass p d0) : ℝ) *
1020            (((phase2NatE0 s t (permClass p d0) : ℕ) : ℝ) / 2) ^ 2) =
1021        Real.sqrt 2 / 8 *
1022          ∑ d0 : Fin 15,
1023            (kernel12Sign d0 : ℝ) * (cz (permClass p d0) : ℝ) *
1024              ((phase2NatE0 s t (permClass p d0) : ℕ) : ℝ) ^ 2 := by
1025      refine Eq.trans ?_ (Finset.mul_sum _ _ _).symm
1026      refine Finset.sum_congr rfl fun d0 _ => by ring
1027    _ = Real.sqrt 2 *
1028          (∑ d0 : Fin 15,
1029              kernel12Sign d0 * cz (permClass p d0) *
1030                ((phase2NatE0 s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 8 := by
1031      rw [Int.cast_sum]
1032      push_cast; ring
1033
1034private lemma ker_push_sqrt3_e0 (cz : Fin 15 → ℤ) (p : Fin 24)
1035    (H : Mat4) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
1036    (s : Fin 24) (t : Fin 10) :
1037    (∑ d0 : Fin 15,
1038        ReggeHinge4DStarKernel13.fullStarClassKernel d0 *
1039          classCoeff H (permClass p d0) *
1040            (phaseScaleDir e0Dir (hingeBase s t) (permClass p d0)) ^ 2) =
1041      Real.sqrt 3 *
1042        (∑ d0 : Fin 15,
1043            kernel13Sign d0 * cz (permClass p d0) *
1044              ((phase2NatE0 s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 4 := by
1045  simp_rw [kernel13_eq_sign, hH, phaseScaleDir_e0Dir]
1046  calc
1047    (∑ d0 : Fin 15,
1048        ((kernel13Sign d0 : ℝ) * Real.sqrt 3) *
1049          (cz (permClass p d0) : ℝ) *
1050            (((phase2NatE0 s t (permClass p d0) : ℕ) : ℝ) / 2) ^ 2) =
1051        Real.sqrt 3 / 4 *
1052          ∑ d0 : Fin 15,
1053            (kernel13Sign d0 : ℝ) * (cz (permClass p d0) : ℝ) *
1054              ((phase2NatE0 s t (permClass p d0) : ℕ) : ℝ) ^ 2 := by
1055      refine Eq.trans ?_ (Finset.mul_sum _ _ _).symm
1056      refine Finset.sum_congr rfl fun d0 _ => by ring
1057    _ = Real.sqrt 3 *
1058          (∑ d0 : Fin 15,
1059              kernel13Sign d0 * cz (permClass p d0) *
1060                ((phase2NatE0 s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 4 := by
1061      rw [Int.cast_sum]
1062      push_cast; ring
1063
1064theorem m2TransportedOrbitSlotCoeff_t12_eq_cert_e0 (H : Mat4) (cz : Fin 15 → ℤ)
1065    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
1066    m2TransportedOrbitSlotCoeff .t12 H e0Dir s t =
1067      (m2OrbitCertZ12E0 cz s t : ℝ) / 64 := by
1068  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
1069    m2OrbitCertZ12E0
1070  by_cases ht : isOrbit .t12 s t
1071  · simp only [ht, ite_true]
1072    set p := orbitCoveringPerm .t12 s t with hp
1073    have hA :
1074        (∑ d : Fin 15, slotOrbitAreaCov .t12 s t d * classCoeff H d) =
1075          Real.sqrt 2 * (slotAZ12 cz s t : ℝ) / 8 := by
1076      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
1077      rw [sum_mul_pushforward, ← hp]
1078      simpa [slotAZ12, hp] using
1079        area_push_sqrt2 area12Z cz p H hH areaCov12 areaCov12_eq_z
1080    have hK :
1081        (∑ d : Fin 15,
1082            slotOrbitDeficitKer .t12 s t d * classCoeff H d *
1083              (phaseScaleDir e0Dir (hingeBase s t) d) ^ 2) =
1084          Real.sqrt 2 * (slotKppOrbitE0 kernel12Sign cz .t12 s t : ℝ) / 8 := by
1085      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel]
1086      rw [sum_mul_pushforward_weighted, ← hp]
1087      simpa [slotKppOrbitE0, hp] using ker_push_sqrt2_half_e0 cz p H hH s t
1088    rw [hA, hK]
1089    exact radical2_slot_arith (slotAZ12 cz s t)
1090      (slotKppOrbitE0 kernel12Sign cz .t12 s t)
1091  · simp [ht]
1092
1093theorem m2TransportedOrbitSlotCoeff_t21_eq_cert_e0 (H : Mat4) (cz : Fin 15 → ℤ)
1094    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
1095    m2TransportedOrbitSlotCoeff .t21 H e0Dir s t =
1096      (m2OrbitCertZ21E0 cz s t : ℝ) / 64 := by
1097  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
1098    m2OrbitCertZ21E0
1099  by_cases ht : isOrbit .t21 s t
1100  · simp only [ht, ite_true]
1101    set p := orbitCoveringPerm .t21 s t with hp
1102    have hA :
1103        (∑ d : Fin 15, slotOrbitAreaCov .t21 s t d * classCoeff H d) =
1104          Real.sqrt 2 * (slotAZ21 cz s t : ℝ) / 8 := by
1105      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
1106      rw [sum_mul_pushforward, ← hp]
1107      simpa [slotAZ21, hp] using
1108        area_push_sqrt2 area21Z cz p H hH areaCov21 areaCov21_eq_z
1109    have hK :
1110        (∑ d : Fin 15,
1111            slotOrbitDeficitKer .t21 s t d * classCoeff H d *
1112              (phaseScaleDir e0Dir (hingeBase s t) d) ^ 2) =
1113          Real.sqrt 2 * (slotKppOrbitE0 kernel12Sign cz .t21 s t : ℝ) / 8 := by
1114      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel,
1115        kernel21]
1116      rw [sum_mul_pushforward_weighted, ← hp]
1117      simpa [slotKppOrbitE0, hp] using ker_push_sqrt2_half_e0 cz p H hH s t
1118    rw [hA, hK]
1119    exact radical2_slot_arith (slotAZ21 cz s t)
1120      (slotKppOrbitE0 kernel12Sign cz .t21 s t)
1121  · simp [ht]
1122
1123theorem m2TransportedOrbitSlotCoeff_t13_eq_cert_e0 (H : Mat4) (cz : Fin 15 → ℤ)
1124    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
1125    m2TransportedOrbitSlotCoeff .t13 H e0Dir s t =
1126      (m2OrbitCertZ13E0 cz s t : ℝ) / 32 := by
1127  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
1128    m2OrbitCertZ13E0
1129  by_cases ht : isOrbit .t13 s t
1130  · simp only [ht, ite_true]
1131    set p := orbitCoveringPerm .t13 s t with hp
1132    have hA :
1133        (∑ d : Fin 15, slotOrbitAreaCov .t13 s t d * classCoeff H d) =
1134          Real.sqrt 3 * (slotAZ13 cz s t : ℝ) / 12 := by
1135      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
1136      rw [sum_mul_pushforward, ← hp]
1137      simpa [slotAZ13, hp] using
1138        area_push_sqrt3 area13Z cz p H hH areaCov13 areaCov13_eq_z
1139    have hK :
1140        (∑ d : Fin 15,
1141            slotOrbitDeficitKer .t13 s t d * classCoeff H d *
1142              (phaseScaleDir e0Dir (hingeBase s t) d) ^ 2) =
1143          Real.sqrt 3 * (slotKppOrbitE0 kernel13Sign cz .t13 s t : ℝ) / 4 := by
1144      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel]
1145      rw [sum_mul_pushforward_weighted, ← hp]
1146      simpa [slotKppOrbitE0, hp] using ker_push_sqrt3_e0 cz p H hH s t
1147    rw [hA, hK]
1148    exact radical3_slot_arith (slotAZ13 cz s t)
1149      (slotKppOrbitE0 kernel13Sign cz .t13 s t)
1150  · simp [ht]
1151
1152theorem m2TransportedOrbitSlotCoeff_t31_eq_cert_e0 (H : Mat4) (cz : Fin 15 → ℤ)
1153    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
1154    m2TransportedOrbitSlotCoeff .t31 H e0Dir s t =
1155      (m2OrbitCertZ31E0 cz s t : ℝ) / 32 := by
1156  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
1157    m2OrbitCertZ31E0
1158  by_cases ht : isOrbit .t31 s t
1159  · simp only [ht, ite_true]
1160    set p := orbitCoveringPerm .t31 s t with hp
1161    have hA :
1162        (∑ d : Fin 15, slotOrbitAreaCov .t31 s t d * classCoeff H d) =
1163          Real.sqrt 3 * (slotAZ31 cz s t : ℝ) / 12 := by
1164      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
1165      rw [sum_mul_pushforward, ← hp]
1166      simpa [slotAZ31, hp] using
1167        area_push_sqrt3 area31Z cz p H hH areaCov31 areaCov31_eq_z
1168    have hK :
1169        (∑ d : Fin 15,
1170            slotOrbitDeficitKer .t31 s t d * classCoeff H d *
1171              (phaseScaleDir e0Dir (hingeBase s t) d) ^ 2) =
1172          Real.sqrt 3 * (slotKppOrbitE0 kernel13Sign cz .t31 s t : ℝ) / 4 := by
1173      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel,
1174        kernel31]
1175      rw [sum_mul_pushforward_weighted, ← hp]
1176      simpa [slotKppOrbitE0, hp] using ker_push_sqrt3_e0 cz p H hH s t
1177    rw [hA, hK]
1178    exact radical3_slot_arith (slotAZ31 cz s t)
1179      (slotKppOrbitE0 kernel13Sign cz .t31 s t)
1180  · simp [ht]
1181
1182theorem m2TransportedOrbitSlotCoeff_t22_eq_cert_e0 (H : Mat4) (cz : Fin 15 → ℤ)
1183    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
1184    m2TransportedOrbitSlotCoeff .t22 H e0Dir s t =
1185      (m2OrbitCertZ22E0 cz s t : ℝ) / 32 := by
1186  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
1187    m2OrbitCertZ22E0
1188  by_cases ht : isOrbit .t22 s t
1189  · simp only [ht, ite_true]
1190    set p := orbitCoveringPerm .t22 s t with hp
1191    have hA :
1192        (∑ d : Fin 15, slotOrbitAreaCov .t22 s t d * classCoeff H d) =
1193          (slotAZ22 cz s t : ℝ) / 4 := by
1194      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
1195      rw [sum_mul_pushforward, ← hp]
1196      unfold slotAZ22
1197      simp_rw [areaCov22_eq_z, hH]
1198      calc
1199        (∑ d0 : Fin 15,
1200            (area22Z d0 : ℝ) / 4 * (cz (permClass p d0) : ℝ)) =
1201            (∑ d0 : Fin 15, (area22Z d0 : ℝ) * (cz (permClass p d0) : ℝ)) /
1202              4 := by
1203          rw [Finset.sum_div]
1204          refine Finset.sum_congr rfl fun d0 _ => by ring
1205        _ = (∑ d0 : Fin 15, area22Z d0 * cz (permClass p d0) : ℤ) / 4 := by
1206          rw [Int.cast_sum]; push_cast; rfl
1207    have hK :
1208        (∑ d : Fin 15,
1209            slotOrbitDeficitKer .t22 s t d * classCoeff H d *
1210              (phaseScaleDir e0Dir (hingeBase s t) d) ^ 2) =
1211          (slotKppOrbitE0 kernel22Sign cz .t22 s t : ℝ) / 4 := by
1212      simp only [slotOrbitDeficitKer, transportedOrbitDeficit, orbitSeedKernel]
1213      rw [sum_mul_pushforward_weighted, ← hp]
1214      unfold slotKppOrbitE0
1215      simp_rw [kernel22_eq_sign, hH, phaseScaleDir_e0Dir]
1216      calc
1217        (∑ d0 : Fin 15,
1218            (kernel22Sign d0 : ℝ) * (cz (permClass p d0) : ℝ) *
1219              (((phase2NatE0 s t (permClass p d0) : ℕ) : ℝ) / 2) ^ 2) =
1220            (∑ d0 : Fin 15,
1221                (kernel22Sign d0 : ℝ) * (cz (permClass p d0) : ℝ) *
1222                  ((phase2NatE0 s t (permClass p d0) : ℕ) : ℝ) ^ 2) / 4 := by
1223          rw [Finset.sum_div]
1224          refine Finset.sum_congr rfl fun d0 _ => by ring
1225        _ = (∑ d0 : Fin 15,
1226                kernel22Sign d0 * cz (permClass p d0) *
1227                  ((phase2NatE0 s t (permClass p d0) : ℕ) : ℤ) ^ 2 : ℤ) / 4 := by
1228          rw [Int.cast_sum]; push_cast; rfl
1229    rw [hA, hK]
1230    push_cast; ring
1231  · simp [ht]
1232
1233theorem m2TransportedOrbitSlotCoeff_t11_eq_cert_e0 (H : Mat4) (cz : Fin 15 → ℤ)
1234    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
1235    m2TransportedOrbitSlotCoeff .t11 H e0Dir s t =
1236      (m2SlotCertZE0 cz s t : ℝ) / 32 := by
1237  unfold m2TransportedOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
1238    m2SlotCertZE0
1239  by_cases h : isOrbit .t11 s t
1240  · have ht : isT11 s t := (isOrbit_t11_iff_isT11 s t).mp h
1241    simp only [h, ht, ite_true]
1242    have hA :
1243        (∑ d : Fin 15, slotOrbitAreaCov .t11 s t d * classCoeff H d) =
1244          (slotA0Z4 cz s t : ℝ) / 4 := by
1245      simp only [slotOrbitAreaCov_t11 s t ht]
1246      unfold slotA0Z4
1247      have hcast : ∀ d : Fin 15,
1248          slotAreaCov s t d = ((slotAreaCovZ4 s t d : ℤ) : ℝ) / 4 := by
1249        intro d
1250        unfold slotAreaCov slotAreaCovZ4
1251        split_ifs <;> norm_num
1252      rw [Int.cast_sum, Finset.sum_div]
1253      refine Finset.sum_congr rfl fun d _ => ?_
1254      rw [hcast, hH]; push_cast; ring
1255    have hK :
1256        (∑ d : Fin 15,
1257            slotOrbitDeficitKer .t11 s t d * classCoeff H d *
1258              (phaseScaleDir e0Dir (hingeBase s t) d) ^ 2) =
1259          (slotKppZE0 cz s t : ℝ) / 4 := by
1260      simp only [slotOrbitDeficitKer_t11]
1261      have hre :
1262          (∑ d : Fin 15,
1263              slotDeficitKer s t d * classCoeff H d *
1264                (phaseScaleDir e0Dir (hingeBase s t) d) ^ 2) =
1265            ∑ d0 : Fin 15,
1266              ReggeHinge4DStarKernel.fullStarClassKernel d0 *
1267                classCoeff H (permClass (slotTransportPerm s t) d0) *
1268                  (phaseScaleDir e0Dir (hingeBase s t)
1269                    (permClass (slotTransportPerm s t) d0)) ^ 2 := by
1270        unfold slotDeficitKer transportedDeficit
1271        simp_rw [Finset.sum_mul]
1272        rw [Finset.sum_comm]
1273        refine Finset.sum_congr rfl fun d0 _ => ?_
1274        classical
1275        rw [Finset.sum_eq_single (permClass (slotTransportPerm s t) d0)]
1276        · simp
1277        · intro d _ hd
1278          have : permClass (slotTransportPerm s t) d0 ≠ d := by
1279            intro heq; exact hd heq.symm
1280          simp [this]
1281        · intro huniv; exact (huniv (Finset.mem_univ _)).elim
1282      rw [hre]
1283      unfold slotKppZE0
1284      simp_rw [kernel11_eq_sign, hH, phaseScaleDir_e0Dir]
1285      rw [Int.cast_sum, Finset.sum_div]
1286      refine Finset.sum_congr rfl fun d0 _ => ?_
1287      push_cast; ring
1288    rw [hA, hK]; push_cast; ring
1289  · have ht : ¬ isT11 s t := fun ht =>
1290      h ((isOrbit_t11_iff_isT11 s t).mpr ht)
1291    simp [h, ht]
1292
1293/-! ### Integer sums on `e0Dir` (probe-confirmed targets) -/
1294
1295set_option maxRecDepth 12000 in
1296set_option maxHeartbeats 8000000 in
1297theorem sum_m2SlotCertZE0_plus :
1298    (∑ s : Fin 24, ∑ t : Fin 10, m2SlotCertZE0 axisTTPlusCoeffZ s t) =
1299      (0 : ℤ) := by
1300  decide
1301
1302set_option maxRecDepth 12000 in
1303set_option maxHeartbeats 8000000 in
1304theorem sum_m2OrbitCertZ12E0_plus :
1305    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ12E0 axisTTPlusCoeffZ s t) =
1306      (0 : ℤ) := by
1307  decide
1308
1309set_option maxRecDepth 12000 in
1310set_option maxHeartbeats 8000000 in
1311theorem sum_m2OrbitCertZ21E0_plus :
1312    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ21E0 axisTTPlusCoeffZ s t) =
1313      (0 : ℤ) := by
1314  decide
1315
1316set_option maxRecDepth 12000 in
1317set_option maxHeartbeats 8000000 in
1318theorem sum_m2OrbitCertZ13E0_plus :
1319    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ13E0 axisTTPlusCoeffZ s t) =
1320      (0 : ℤ) := by
1321  decide
1322
1323set_option maxRecDepth 12000 in
1324set_option maxHeartbeats 8000000 in
1325theorem sum_m2OrbitCertZ31E0_plus :
1326    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ31E0 axisTTPlusCoeffZ s t) =
1327      (0 : ℤ) := by
1328  decide
1329
1330set_option maxRecDepth 12000 in
1331set_option maxHeartbeats 8000000 in
1332theorem sum_m2OrbitCertZ22E0_plus :
1333    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ22E0 axisTTPlusCoeffZ s t) =
1334      (0 : ℤ) := by
1335  decide
1336
1337set_option maxRecDepth 12000 in
1338set_option maxHeartbeats 8000000 in
1339theorem sum_m2SlotCertZE0_cross :
1340    (∑ s : Fin 24, ∑ t : Fin 10, m2SlotCertZE0 axisTTCrossCoeffZ s t) =
1341      (0 : ℤ) := by
1342  decide
1343
1344set_option maxRecDepth 12000 in
1345set_option maxHeartbeats 8000000 in
1346theorem sum_m2OrbitCertZ12E0_cross :
1347    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ12E0 axisTTCrossCoeffZ s t) =
1348      (-96 : ℤ) := by
1349  decide
1350
1351set_option maxRecDepth 12000 in
1352set_option maxHeartbeats 8000000 in
1353theorem sum_m2OrbitCertZ21E0_cross :
1354    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ21E0 axisTTCrossCoeffZ s t) =
1355      (0 : ℤ) := by
1356  decide
1357
1358set_option maxRecDepth 12000 in
1359set_option maxHeartbeats 8000000 in
1360theorem sum_m2OrbitCertZ13E0_cross :
1361    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ13E0 axisTTCrossCoeffZ s t) =
1362      (24 : ℤ) := by
1363  decide
1364
1365set_option maxRecDepth 12000 in
1366set_option maxHeartbeats 8000000 in
1367theorem sum_m2OrbitCertZ31E0_cross :
1368    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ31E0 axisTTCrossCoeffZ s t) =
1369      (24 : ℤ) := by
1370  decide
1371
1372set_option maxRecDepth 12000 in
1373set_option maxHeartbeats 8000000 in
1374theorem sum_m2OrbitCertZ22E0_cross :
1375    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ22E0 axisTTCrossCoeffZ s t) =
1376      (0 : ℤ) := by
1377  decide
1378
1379/-! ### Real moments on `e0Dir` -/
1380
1381theorem m2TransportedOrbitMoment_t11_plus_e0 :
1382    m2TransportedOrbitMoment .t11 axisTTPlus e0Dir = (0 : ℝ) := by
1383  unfold m2TransportedOrbitMoment
1384  simp_rw [m2TransportedOrbitSlotCoeff_t11_eq_cert_e0 axisTTPlus axisTTPlusCoeffZ
1385    classCoeff_axisTTPlus_int]
1386  have hsum :
1387      (∑ s : Fin 24, ∑ t : Fin 10,
1388          (m2SlotCertZE0 axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
1389    simpa [Int.cast_sum] using
1390      congrArg (fun n : ℤ => (n : ℝ)) sum_m2SlotCertZE0_plus
1391  rw [sum_div_const_st, hsum]; norm_num
1392
1393theorem m2TransportedOrbitMoment_t12_plus_e0 :
1394    m2TransportedOrbitMoment .t12 axisTTPlus e0Dir = (0 : ℝ) := by
1395  unfold m2TransportedOrbitMoment
1396  simp_rw [m2TransportedOrbitSlotCoeff_t12_eq_cert_e0 axisTTPlus axisTTPlusCoeffZ
1397    classCoeff_axisTTPlus_int]
1398  have hsum :
1399      (∑ s : Fin 24, ∑ t : Fin 10,
1400          (m2OrbitCertZ12E0 axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
1401    simpa [Int.cast_sum] using
1402      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ12E0_plus
1403  rw [sum_div_const_st, hsum]; norm_num
1404
1405theorem m2TransportedOrbitMoment_t21_plus_e0 :
1406    m2TransportedOrbitMoment .t21 axisTTPlus e0Dir = (0 : ℝ) := by
1407  unfold m2TransportedOrbitMoment
1408  simp_rw [m2TransportedOrbitSlotCoeff_t21_eq_cert_e0 axisTTPlus axisTTPlusCoeffZ
1409    classCoeff_axisTTPlus_int]
1410  have hsum :
1411      (∑ s : Fin 24, ∑ t : Fin 10,
1412          (m2OrbitCertZ21E0 axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
1413    simpa [Int.cast_sum] using
1414      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ21E0_plus
1415  rw [sum_div_const_st, hsum]; norm_num
1416
1417theorem m2TransportedOrbitMoment_t13_plus_e0 :
1418    m2TransportedOrbitMoment .t13 axisTTPlus e0Dir = (0 : ℝ) := by
1419  unfold m2TransportedOrbitMoment
1420  simp_rw [m2TransportedOrbitSlotCoeff_t13_eq_cert_e0 axisTTPlus axisTTPlusCoeffZ
1421    classCoeff_axisTTPlus_int]
1422  have hsum :
1423      (∑ s : Fin 24, ∑ t : Fin 10,
1424          (m2OrbitCertZ13E0 axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
1425    simpa [Int.cast_sum] using
1426      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ13E0_plus
1427  rw [sum_div_const_st, hsum]; norm_num
1428
1429theorem m2TransportedOrbitMoment_t31_plus_e0 :
1430    m2TransportedOrbitMoment .t31 axisTTPlus e0Dir = (0 : ℝ) := by
1431  unfold m2TransportedOrbitMoment
1432  simp_rw [m2TransportedOrbitSlotCoeff_t31_eq_cert_e0 axisTTPlus axisTTPlusCoeffZ
1433    classCoeff_axisTTPlus_int]
1434  have hsum :
1435      (∑ s : Fin 24, ∑ t : Fin 10,
1436          (m2OrbitCertZ31E0 axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
1437    simpa [Int.cast_sum] using
1438      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ31E0_plus
1439  rw [sum_div_const_st, hsum]; norm_num
1440
1441theorem m2TransportedOrbitMoment_t22_plus_e0 :
1442    m2TransportedOrbitMoment .t22 axisTTPlus e0Dir = (0 : ℝ) := by
1443  unfold m2TransportedOrbitMoment
1444  simp_rw [m2TransportedOrbitSlotCoeff_t22_eq_cert_e0 axisTTPlus axisTTPlusCoeffZ
1445    classCoeff_axisTTPlus_int]
1446  have hsum :
1447      (∑ s : Fin 24, ∑ t : Fin 10,
1448          (m2OrbitCertZ22E0 axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
1449    simpa [Int.cast_sum] using
1450      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ22E0_plus
1451  rw [sum_div_const_st, hsum]; norm_num
1452
1453theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_e0Dir :
1454    m2TransportedAllOrbitMomentDistinctHinge axisTTPlus e0Dir = (0 : ℝ) := by
1455  unfold m2TransportedAllOrbitMomentDistinctHinge
1456  rw [sum_six_orbits]
1457  simp only [orbitStarSize]
1458  rw [m2TransportedOrbitMoment_t11_plus_e0, m2TransportedOrbitMoment_t12_plus_e0,
1459    m2TransportedOrbitMoment_t21_plus_e0, m2TransportedOrbitMoment_t13_plus_e0,
1460    m2TransportedOrbitMoment_t31_plus_e0, m2TransportedOrbitMoment_t22_plus_e0]
1461  norm_num
1462
1463theorem m2TransportedOrbitMoment_t11_cross_e0 :
1464    m2TransportedOrbitMoment .t11 axisTTCross e0Dir = (0 : ℝ) := by
1465  unfold m2TransportedOrbitMoment
1466  simp_rw [m2TransportedOrbitSlotCoeff_t11_eq_cert_e0 axisTTCross axisTTCrossCoeffZ
1467    classCoeff_axisTTCross_int]
1468  have hsum :
1469      (∑ s : Fin 24, ∑ t : Fin 10,
1470          (m2SlotCertZE0 axisTTCrossCoeffZ s t : ℝ)) = (0 : ℝ) := by
1471    simpa [Int.cast_sum] using
1472      congrArg (fun n : ℤ => (n : ℝ)) sum_m2SlotCertZE0_cross
1473  rw [sum_div_const_st, hsum]; norm_num
1474
1475theorem m2TransportedOrbitMoment_t12_cross_e0 :
1476    m2TransportedOrbitMoment .t12 axisTTCross e0Dir = (-3 / 2 : ℝ) := by
1477  unfold m2TransportedOrbitMoment
1478  simp_rw [m2TransportedOrbitSlotCoeff_t12_eq_cert_e0 axisTTCross axisTTCrossCoeffZ
1479    classCoeff_axisTTCross_int]
1480  have hsum :
1481      (∑ s : Fin 24, ∑ t : Fin 10,
1482          (m2OrbitCertZ12E0 axisTTCrossCoeffZ s t : ℝ)) = (-96 : ℝ) := by
1483    simpa [Int.cast_sum] using
1484      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ12E0_cross
1485  rw [sum_div_const_st, hsum]; norm_num
1486
1487theorem m2TransportedOrbitMoment_t21_cross_e0 :
1488    m2TransportedOrbitMoment .t21 axisTTCross e0Dir = (0 : ℝ) := by
1489  unfold m2TransportedOrbitMoment
1490  simp_rw [m2TransportedOrbitSlotCoeff_t21_eq_cert_e0 axisTTCross axisTTCrossCoeffZ
1491    classCoeff_axisTTCross_int]
1492  have hsum :
1493      (∑ s : Fin 24, ∑ t : Fin 10,
1494          (m2OrbitCertZ21E0 axisTTCrossCoeffZ s t : ℝ)) = (0 : ℝ) := by
1495    simpa [Int.cast_sum] using
1496      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ21E0_cross
1497  rw [sum_div_const_st, hsum]; norm_num
1498
1499theorem m2TransportedOrbitMoment_t13_cross_e0 :
1500    m2TransportedOrbitMoment .t13 axisTTCross e0Dir = (3 / 4 : ℝ) := by
1501  unfold m2TransportedOrbitMoment
1502  simp_rw [m2TransportedOrbitSlotCoeff_t13_eq_cert_e0 axisTTCross axisTTCrossCoeffZ
1503    classCoeff_axisTTCross_int]
1504  have hsum :
1505      (∑ s : Fin 24, ∑ t : Fin 10,
1506          (m2OrbitCertZ13E0 axisTTCrossCoeffZ s t : ℝ)) = (24 : ℝ) := by
1507    simpa [Int.cast_sum] using
1508      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ13E0_cross
1509  rw [sum_div_const_st, hsum]; norm_num
1510
1511theorem m2TransportedOrbitMoment_t31_cross_e0 :
1512    m2TransportedOrbitMoment .t31 axisTTCross e0Dir = (3 / 4 : ℝ) := by
1513  unfold m2TransportedOrbitMoment
1514  simp_rw [m2TransportedOrbitSlotCoeff_t31_eq_cert_e0 axisTTCross axisTTCrossCoeffZ
1515    classCoeff_axisTTCross_int]
1516  have hsum :
1517      (∑ s : Fin 24, ∑ t : Fin 10,
1518          (m2OrbitCertZ31E0 axisTTCrossCoeffZ s t : ℝ)) = (24 : ℝ) := by
1519    simpa [Int.cast_sum] using
1520      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ31E0_cross
1521  rw [sum_div_const_st, hsum]; norm_num
1522
1523theorem m2TransportedOrbitMoment_t22_cross_e0 :
1524    m2TransportedOrbitMoment .t22 axisTTCross e0Dir = (0 : ℝ) := by
1525  unfold m2TransportedOrbitMoment
1526  simp_rw [m2TransportedOrbitSlotCoeff_t22_eq_cert_e0 axisTTCross axisTTCrossCoeffZ
1527    classCoeff_axisTTCross_int]
1528  have hsum :
1529      (∑ s : Fin 24, ∑ t : Fin 10,
1530          (m2OrbitCertZ22E0 axisTTCrossCoeffZ s t : ℝ)) = (0 : ℝ) := by
1531    simpa [Int.cast_sum] using
1532      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ22E0_cross
1533  rw [sum_div_const_st, hsum]; norm_num
1534
1535/-- Distinct-hinge on cross / e0Dir: `(-3/2)/4 + (3/4)/6 + (3/4)/6 = -1/8`. -/
1536theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_e0Dir :
1537    m2TransportedAllOrbitMomentDistinctHinge axisTTCross e0Dir =
1538      (-1 / 8 : ℝ) := by
1539  unfold m2TransportedAllOrbitMomentDistinctHinge
1540  rw [sum_six_orbits]
1541  simp only [orbitStarSize]
1542  rw [m2TransportedOrbitMoment_t11_cross_e0, m2TransportedOrbitMoment_t12_cross_e0,
1543    m2TransportedOrbitMoment_t21_cross_e0, m2TransportedOrbitMoment_t13_cross_e0,
1544    m2TransportedOrbitMoment_t31_cross_e0, m2TransportedOrbitMoment_t22_cross_e0]
1545  norm_num
1546
1547theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTPlusNormalized_e0Dir :
1548    m2TransportedAllOrbitMomentDistinctHinge
1549        ((Real.sqrt 2)⁻¹ • axisTTPlus) e0Dir = (0 : ℝ) := by
1550  rw [m2TransportedAllOrbitMomentDistinctHinge_smul,
1551    m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_e0Dir]
1552  norm_num
1553
1554theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTCrossNormalized_e0Dir :
1555    m2TransportedAllOrbitMomentDistinctHinge
1556        ((Real.sqrt 2)⁻¹ • axisTTCross) e0Dir =
1557      (-1 / 16 : ℝ) := by
1558  rw [m2TransportedAllOrbitMomentDistinctHinge_smul,
1559    m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_e0Dir,
1560    inv_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
1561  norm_num
1562
1563/-- **OPEN (status false)**: continuum TT isotropy is blocked on the bare
1564lattice-axis mode `e0Dir`, where plus vanishes and cross gives `-1/8`
1565(normalized `-1/16`).  Not hidden: EH Tendsto needs every nonzero mode. -/
1566def Regge4DContinuumIsotropyBlockedOnAxisMode : Prop :=
1567  m2TransportedAllOrbitMomentDistinctHinge axisTTPlus e0Dir =
1568    m2TransportedAllOrbitMomentDistinctHinge axisTTCross e0Dir ∧
1569      m2TransportedAllOrbitMomentDistinctHinge
1570          ((Real.sqrt 2)⁻¹ • axisTTPlus) e0Dir =
1571        (-1 / 16 : ℝ)
1572
1573theorem Regge4DContinuumIsotropyBlockedOnAxisMode_status_false :
1574    ¬ Regge4DContinuumIsotropyBlockedOnAxisMode := by
1575  unfold Regge4DContinuumIsotropyBlockedOnAxisMode
1576  intro h
1577  have hplus := m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_e0Dir
1578  have hcross := m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_e0Dir
1579  have hne : (0 : ℝ) ≠ (-1 / 8 : ℝ) := by norm_num
1580  exact hne (hplus.symm.trans (h.1.trans hcross))
1581
1582theorem axis_mode_plus_cross_disagree_e0Dir :
1583    m2TransportedAllOrbitMomentDistinctHinge axisTTPlus e0Dir ≠
1584      m2TransportedAllOrbitMomentDistinctHinge axisTTCross e0Dir := by
1585  rw [m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_e0Dir,
1586    m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_e0Dir]
1587  norm_num
1588
1589/-! ## §12. Full cosine two-jet `A0*K2 + A2*K0` vs truncated `A0*K2`
1590
1591Integer unphased ker dots vanish for TT plus/cross on every slot
1592(`slotOrbitKerDot_axisTTPlus` / `slotOrbitKerDot_axisTTCross`, via
1593`slotOrbitKerDotZ_*` decide certificates), so the `A2*K0` summand is
1594identically zero and full jet equals the truncated `A0*K2` certificates
1595on every direction.  Consequently e0Dir anisotropy (plus `0`, cross
1596`-1/8`) and plus vanishing are **not** repaired by restoring `A2*K0`.
1597Probe receipts: `scripts/probe_m2_full_twojet_e0.py` and
1598`state/qg_full_theory/probe_fulljet_distinct_hinge_20260721.json`
1599(MEASURED off-axis faces; THEOREM on the banked axisTTPlus/Cross rays).
1600-/
1601
1602/-- Integer unphased transported ker · `cz` (radical factored out). -/
1603def slotOrbitKerDotZ (sign : Fin 15 → ℤ) (cz : Fin 15 → ℤ)
1604    (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) : ℤ :=
1605  ∑ d0 : Fin 15,
1606    sign d0 * cz (permClass (orbitCoveringPerm ty s t) d0)
1607
1608def slotOrbitKerDotZ_of (ty : HingeOrbitType) (cz : Fin 15 → ℤ)
1609    (s : Fin 24) (t : Fin 10) : ℤ :=
1610  match ty with
1611  | .t11 => slotOrbitKerDotZ kernel11Sign cz .t11 s t
1612  | .t12 => slotOrbitKerDotZ kernel12Sign cz .t12 s t
1613  | .t21 => slotOrbitKerDotZ kernel12Sign cz .t21 s t
1614  | .t13 => slotOrbitKerDotZ kernel13Sign cz .t13 s t
1615  | .t31 => slotOrbitKerDotZ kernel13Sign cz .t31 s t
1616  | .t22 => slotOrbitKerDotZ kernel22Sign cz .t22 s t
1617
1618set_option maxRecDepth 8000 in
1619set_option maxHeartbeats 800000 in
1620theorem slotOrbitKerDotZ_axisTTPlus :
1621    ∀ ty : HingeOrbitType, ∀ s : Fin 24, ∀ t : Fin 10,
1622      slotOrbitKerDotZ_of ty axisTTPlusCoeffZ s t = 0 := by
1623  decide
1624
1625set_option maxRecDepth 8000 in
1626set_option maxHeartbeats 800000 in
1627theorem slotOrbitKerDotZ_axisTTCross :
1628    ∀ ty : HingeOrbitType, ∀ s : Fin 24, ∀ t : Fin 10,
1629      slotOrbitKerDotZ_of ty axisTTCrossCoeffZ s t = 0 := by
1630  decide
1631
1632private lemma slotOrbitKerDot_reindex (ty : HingeOrbitType) (H : Mat4)
1633    (s : Fin 24) (t : Fin 10) :
1634    slotOrbitKerDot ty H s t =
1635      ∑ d0 : Fin 15,
1636        orbitSeedKernel ty d0 *
1637          classCoeff H (permClass (orbitCoveringPerm ty s t) d0) := by
1638  unfold slotOrbitKerDot slotOrbitDeficitKer transportedOrbitDeficit
1639  exact sum_mul_pushforward (orbitSeedKernel ty) (classCoeff H)
1640    (orbitCoveringPerm ty s t)
1641
1642/-- `orbitSeedKernel = sign * α` (matching `kernel*_eq_sign` order). -/
1643private lemma slotOrbitKerDot_eq_z_mul (ty : HingeOrbitType) (H : Mat4)
1644    (cz : Fin 15 → ℤ) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
1645    (s : Fin 24) (t : Fin 10) (α : ℝ) (sign : Fin 15 → ℤ)
1646    (hker : ∀ d0, orbitSeedKernel ty d0 = (sign d0 : ℝ) * α) :
1647    slotOrbitKerDot ty H s t =
1648      α * (slotOrbitKerDotZ sign cz ty s t : ℝ) := by
1649  rw [slotOrbitKerDot_reindex]
1650  simp_rw [hker, hH]
1651  have hterm : ∀ d0 : Fin 15,
1652      (sign d0 : ℝ) * α * (cz (permClass (orbitCoveringPerm ty s t) d0) : ℝ) =
1653        α * ((sign d0 : ℝ) *
1654          (cz (permClass (orbitCoveringPerm ty s t) d0) : ℝ)) := by
1655    intro d0; ring
1656  simp_rw [hterm, ← Finset.mul_sum]
1657  unfold slotOrbitKerDotZ
1658  congr 1
1659  rw [Int.cast_sum]
1660  push_cast
1661  rfl
1662
1663private lemma slotOrbitKerDot_of_z0 (ty : HingeOrbitType) (H : Mat4)
1664    (cz : Fin 15 → ℤ) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
1665    (s : Fin 24) (t : Fin 10) (α : ℝ) (sign : Fin 15 → ℤ)
1666    (hker : ∀ d0, orbitSeedKernel ty d0 = (sign d0 : ℝ) * α)
1667    (hz : slotOrbitKerDotZ sign cz ty s t = 0) :
1668    slotOrbitKerDot ty H s t = 0 := by
1669  rw [slotOrbitKerDot_eq_z_mul ty H cz hH s t α sign hker, hz]
1670  simp
1671
1672theorem slotOrbitKerDot_axisTTPlus (ty : HingeOrbitType) (s : Fin 24)
1673    (t : Fin 10) : slotOrbitKerDot ty axisTTPlus s t = 0 := by
1674  have hz := slotOrbitKerDotZ_axisTTPlus ty s t
1675  cases ty with
1676  | t11 =>
1677      exact slotOrbitKerDot_of_z0 .t11 axisTTPlus axisTTPlusCoeffZ
1678        classCoeff_axisTTPlus_int s t 1 kernel11Sign
1679        (fun d0 => by simpa using kernel11_eq_sign d0)
1680        (by simpa [slotOrbitKerDotZ_of] using hz)
1681  | t12 =>
1682      exact slotOrbitKerDot_of_z0 .t12 axisTTPlus axisTTPlusCoeffZ
1683        classCoeff_axisTTPlus_int s t (Real.sqrt 2 / 2) kernel12Sign
1684        (fun d0 => by simpa [orbitSeedKernel] using kernel12_eq_sign d0)
1685        (by simpa [slotOrbitKerDotZ_of] using hz)
1686  | t21 =>
1687      exact slotOrbitKerDot_of_z0 .t21 axisTTPlus axisTTPlusCoeffZ
1688        classCoeff_axisTTPlus_int s t (Real.sqrt 2 / 2) kernel12Sign
1689        (fun d0 => by simpa [orbitSeedKernel, kernel21] using kernel12_eq_sign d0)
1690        (by simpa [slotOrbitKerDotZ_of] using hz)
1691  | t13 =>
1692      exact slotOrbitKerDot_of_z0 .t13 axisTTPlus axisTTPlusCoeffZ
1693        classCoeff_axisTTPlus_int s t (Real.sqrt 3) kernel13Sign
1694        (fun d0 => by simpa [orbitSeedKernel] using kernel13_eq_sign d0)
1695        (by simpa [slotOrbitKerDotZ_of] using hz)
1696  | t31 =>
1697      exact slotOrbitKerDot_of_z0 .t31 axisTTPlus axisTTPlusCoeffZ
1698        classCoeff_axisTTPlus_int s t (Real.sqrt 3) kernel13Sign
1699        (fun d0 => by simpa [orbitSeedKernel, kernel31] using kernel13_eq_sign d0)
1700        (by simpa [slotOrbitKerDotZ_of] using hz)
1701  | t22 =>
1702      exact slotOrbitKerDot_of_z0 .t22 axisTTPlus axisTTPlusCoeffZ
1703        classCoeff_axisTTPlus_int s t 1 kernel22Sign
1704        (fun d0 => by simpa using kernel22_eq_sign d0)
1705        (by simpa [slotOrbitKerDotZ_of] using hz)
1706
1707theorem slotOrbitKerDot_axisTTCross (ty : HingeOrbitType) (s : Fin 24)
1708    (t : Fin 10) : slotOrbitKerDot ty axisTTCross s t = 0 := by
1709  have hz := slotOrbitKerDotZ_axisTTCross ty s t
1710  cases ty with
1711  | t11 =>
1712      exact slotOrbitKerDot_of_z0 .t11 axisTTCross axisTTCrossCoeffZ
1713        classCoeff_axisTTCross_int s t 1 kernel11Sign
1714        (fun d0 => by simpa using kernel11_eq_sign d0)
1715        (by simpa [slotOrbitKerDotZ_of] using hz)
1716  | t12 =>
1717      exact slotOrbitKerDot_of_z0 .t12 axisTTCross axisTTCrossCoeffZ
1718        classCoeff_axisTTCross_int s t (Real.sqrt 2 / 2) kernel12Sign
1719        (fun d0 => by simpa [orbitSeedKernel] using kernel12_eq_sign d0)
1720        (by simpa [slotOrbitKerDotZ_of] using hz)
1721  | t21 =>
1722      exact slotOrbitKerDot_of_z0 .t21 axisTTCross axisTTCrossCoeffZ
1723        classCoeff_axisTTCross_int s t (Real.sqrt 2 / 2) kernel12Sign
1724        (fun d0 => by simpa [orbitSeedKernel, kernel21] using kernel12_eq_sign d0)
1725        (by simpa [slotOrbitKerDotZ_of] using hz)
1726  | t13 =>
1727      exact slotOrbitKerDot_of_z0 .t13 axisTTCross axisTTCrossCoeffZ
1728        classCoeff_axisTTCross_int s t (Real.sqrt 3) kernel13Sign
1729        (fun d0 => by simpa [orbitSeedKernel] using kernel13_eq_sign d0)
1730        (by simpa [slotOrbitKerDotZ_of] using hz)
1731  | t31 =>
1732      exact slotOrbitKerDot_of_z0 .t31 axisTTCross axisTTCrossCoeffZ
1733        classCoeff_axisTTCross_int s t (Real.sqrt 3) kernel13Sign
1734        (fun d0 => by simpa [orbitSeedKernel, kernel31] using kernel13_eq_sign d0)
1735        (by simpa [slotOrbitKerDotZ_of] using hz)
1736  | t22 =>
1737      exact slotOrbitKerDot_of_z0 .t22 axisTTCross axisTTCrossCoeffZ
1738        classCoeff_axisTTCross_int s t 1 kernel22Sign
1739        (fun d0 => by simpa using kernel22_eq_sign d0)
1740        (by simpa [slotOrbitKerDotZ_of] using hz)
1741
1742theorem m2TransportedOrbitSlotCoeffFull_eq_trunc_axisTTPlus
1743    (ty : HingeOrbitType) (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
1744    m2TransportedOrbitSlotCoeffFull ty axisTTPlus dir s t =
1745      m2TransportedOrbitSlotCoeff ty axisTTPlus dir s t :=
1746  m2TransportedOrbitSlotCoeffFull_eq_trunc_of_ker0 ty axisTTPlus dir s t
1747    (slotOrbitKerDot_axisTTPlus ty s t)
1748
1749theorem m2TransportedOrbitSlotCoeffFull_eq_trunc_axisTTCross
1750    (ty : HingeOrbitType) (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
1751    m2TransportedOrbitSlotCoeffFull ty axisTTCross dir s t =
1752      m2TransportedOrbitSlotCoeff ty axisTTCross dir s t :=
1753  m2TransportedOrbitSlotCoeffFull_eq_trunc_of_ker0 ty axisTTCross dir s t
1754    (slotOrbitKerDot_axisTTCross ty s t)
1755
1756theorem m2TransportedAllOrbitMomentDistinctHingeFull_eq_trunc_axisTTPlus
1757    (dir : Fin 4 → ℝ) :
1758    m2TransportedAllOrbitMomentDistinctHingeFull axisTTPlus dir =
1759      m2TransportedAllOrbitMomentDistinctHinge axisTTPlus dir := by
1760  unfold m2TransportedAllOrbitMomentDistinctHingeFull
1761    m2TransportedAllOrbitMomentDistinctHinge m2TransportedOrbitMomentFull
1762    m2TransportedOrbitMoment
1763  refine Finset.sum_congr rfl fun ty _ => ?_
1764  congr 1
1765  refine Finset.sum_congr rfl fun s _ =>
1766    Finset.sum_congr rfl fun t _ =>
1767      m2TransportedOrbitSlotCoeffFull_eq_trunc_axisTTPlus ty dir s t
1768
1769theorem m2TransportedAllOrbitMomentDistinctHingeFull_eq_trunc_axisTTCross
1770    (dir : Fin 4 → ℝ) :
1771    m2TransportedAllOrbitMomentDistinctHingeFull axisTTCross dir =
1772      m2TransportedAllOrbitMomentDistinctHinge axisTTCross dir := by
1773  unfold m2TransportedAllOrbitMomentDistinctHingeFull
1774    m2TransportedAllOrbitMomentDistinctHinge m2TransportedOrbitMomentFull
1775    m2TransportedOrbitMoment
1776  refine Finset.sum_congr rfl fun ty _ => ?_
1777  congr 1
1778  refine Finset.sum_congr rfl fun s _ =>
1779    Finset.sum_congr rfl fun t _ =>
1780      m2TransportedOrbitSlotCoeffFull_eq_trunc_axisTTCross ty dir s t
1781
1782/-- Full two-jet distinct-hinge values on e0Dir: plus `0`, cross `-1/8`
1783(same as truncated; anisotropy persists). -/
1784theorem m2TransportedAllOrbitMomentDistinctHingeFull_axisTTPlus_e0Dir :
1785    m2TransportedAllOrbitMomentDistinctHingeFull axisTTPlus e0Dir =
1786      (0 : ℝ) := by
1787  rw [m2TransportedAllOrbitMomentDistinctHingeFull_eq_trunc_axisTTPlus,
1788    m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_e0Dir]
1789
1790theorem m2TransportedAllOrbitMomentDistinctHingeFull_axisTTCross_e0Dir :
1791    m2TransportedAllOrbitMomentDistinctHingeFull axisTTCross e0Dir =
1792      (-1 / 8 : ℝ) := by
1793  rw [m2TransportedAllOrbitMomentDistinctHingeFull_eq_trunc_axisTTCross,
1794    m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_e0Dir]
1795
1796theorem m2TransportedAllOrbitMomentDistinctHingeFull_axisTTPlus_symbolDir :
1797    m2TransportedAllOrbitMomentDistinctHingeFull axisTTPlus symbolDir =
1798      (-1 / 4 : ℝ) := by
1799  rw [m2TransportedAllOrbitMomentDistinctHingeFull_eq_trunc_axisTTPlus,
1800    m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir]
1801
1802theorem m2TransportedAllOrbitMomentDistinctHingeFull_axisTTCross_symbolDir :
1803    m2TransportedAllOrbitMomentDistinctHingeFull axisTTCross symbolDir =
1804      (-1 / 4 : ℝ) := by
1805  rw [m2TransportedAllOrbitMomentDistinctHingeFull_eq_trunc_axisTTCross,
1806    m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_symbolDir]
1807
1808/-- Full jet does **not** restore e0Dir plus/cross isotropy. -/
1809theorem full_twojet_does_not_repair_e0_anisotropy :
1810    m2TransportedAllOrbitMomentDistinctHingeFull axisTTPlus e0Dir ≠
1811      m2TransportedAllOrbitMomentDistinctHingeFull axisTTCross e0Dir := by
1812  rw [m2TransportedAllOrbitMomentDistinctHingeFull_axisTTPlus_e0Dir,
1813    m2TransportedAllOrbitMomentDistinctHingeFull_axisTTCross_e0Dir]
1814  norm_num
1815
1816/-- Normalized continuum face under full jet on e0: plus `0`, cross `-1/16`
1817(not EH `-1/4`). -/
1818theorem continuumFace_fullTwoJet_normalizedCross_e0Dir :
1819    m2TransportedAllOrbitMomentDistinctHingeFull
1820          ((Real.sqrt 2)⁻¹ • axisTTCross) e0Dir /
1821        (∑ i : Fin 4, e0Dir i * e0Dir i) =
1822      (-1 / 16 : ℝ) := by
1823  rw [m2TransportedAllOrbitMomentDistinctHingeFull_smul,
1824    m2TransportedAllOrbitMomentDistinctHingeFull_axisTTCross_e0Dir,
1825    e0Dir_normSq, inv_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
1826  norm_num
1827
1828/-- Named restoration claim: full two-jet makes `axisTTPlus` on `e0Dir`
1829leave zero.  Status false (plus stays `0` because `A2*K0` vanishes). -/
1830def Regge4DFullTwoJetRestoresE0PlusVanishing : Prop :=
1831  m2TransportedAllOrbitMomentDistinctHingeFull axisTTPlus e0Dir ≠ (0 : ℝ)
1832
1833theorem Regge4DFullTwoJetRestoresE0PlusVanishing_status_false :
1834    ¬ Regge4DFullTwoJetRestoresE0PlusVanishing := by
1835  intro h
1836  exact h m2TransportedAllOrbitMomentDistinctHingeFull_axisTTPlus_e0Dir
1837
1838/-- Named restoration claim: full two-jet restores e0Dir plus/cross
1839isotropy.  Status false. -/
1840def Regge4DFullTwoJetRestoresE0Isotropy : Prop :=
1841  m2TransportedAllOrbitMomentDistinctHingeFull axisTTPlus e0Dir =
1842    m2TransportedAllOrbitMomentDistinctHingeFull axisTTCross e0Dir
1843
1844theorem Regge4DFullTwoJetRestoresE0Isotropy_status_false :
1845    ¬ Regge4DFullTwoJetRestoresE0Isotropy :=
1846  full_twojet_does_not_repair_e0_anisotropy
1847
1848structure ReggeBlochFullTwoJetM2Eval4DStatus where
1849  k0VanishesOnTTPlusCross : Bool
1850  fullEqualsTruncOnTT : Bool
1851  e0AnisotropyPersists : Bool
1852  e0PlusVanishingPersists : Bool
1853  gapActionRecovery : Bool
1854
1855def reggeBlochFullTwoJetM2Eval4DStatus :
1856    ReggeBlochFullTwoJetM2Eval4DStatus where
1857  k0VanishesOnTTPlusCross := true
1858  fullEqualsTruncOnTT := true
1859  e0AnisotropyPersists := true
1860  e0PlusVanishingPersists := true
1861  gapActionRecovery := false
1862
1863theorem reggeBlochFullTwoJetM2Eval4DStatus_flags :
1864    reggeBlochFullTwoJetM2Eval4DStatus.k0VanishesOnTTPlusCross = true ∧
1865      reggeBlochFullTwoJetM2Eval4DStatus.fullEqualsTruncOnTT = true ∧
1866        reggeBlochFullTwoJetM2Eval4DStatus.e0AnisotropyPersists = true ∧
1867          reggeBlochFullTwoJetM2Eval4DStatus.e0PlusVanishingPersists =
1868            true ∧
1869            reggeBlochFullTwoJetM2Eval4DStatus.gapActionRecovery =
1870              false := by
1871  decide
1872
1873theorem full_twojet_does_not_flip_gap_action_recovery :
1874    reggeBlochFullTwoJetM2Eval4DStatus.gapActionRecovery = false :=
1875  rfl
1876
1877end
1878
1879end ReggeBlochTransportedAllOrbitM2Eval4D
1880end Analysis
1881end Gravity
1882end IndisputableMonolith
1883