IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOriginsM2Eval4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOrigins4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
   5import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   6/-!
   7# Edge-origin m² evaluation certificates (fold repair)
   8
   9Closes the distinct-hinge edge-origin moment on TT / `symbolDir`:
  10
  11  `m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir = -1/4`
  12  `m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir = -1/4`
  13
  14Orbit slices on plus (edge mode): t11=-3, t12=t21=t31=t22=0, t13=3/2
  15so `-3/6 + (3/2)/6 = -1/4`.
  16
  17Also kills the pure-gauge counterexample `gaugePart (1,1,0,0) e₂` and
  18`decoyGauge` on `symbolDir`.
  19
  20Integer certificates: radical-cancelled `decide` on `Fin 24 × Fin 10`.
  21Python oracle: `scripts/qg/regge_4d_fold_position_resolved_20260721.py` (mode=edge).
  22
  23Does **not** flip `gap_action_recovery`. Forbidden: base0, covering-perm chase.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Gravity
  28namespace Analysis
  29namespace ReggeBlochStarEdgeOriginsM2Eval4D
  30
  31open BigOperators
  32open ReggeEdgeStencil4D
  33open ReggeHinge4DOrbitClassification
  34open ReggeBlochFold4D
  35open ReggeBlochM2Symbol4D
  36open ReggeBlochOrbitTransport4D
  37open ReggeBlochTransportedAllOrbit4D
  38open ReggeBlochAllOrbitSymbol4D (isOrbit phaseScaleDir)
  39open ReggeBlochStarEdgeOrigins4D
  40open ReggeBlochTransportedAllOrbitM2Eval4D
  41open ReggeFlat4DHessianAssembly
  42open EdgeTTDecomposition4D (axisTTPlus axisTTCross gaugePart)
  43
  44abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
  45abbrev Wave4 := Fin 4 → ℝ
  46
  47noncomputable section
  48
  49/-! ## §1. Integer seed edge contributions -/
  50
  51structure SeedEdgeContribZ where
  52  cls : Fin 15
  53  weightZ : ℤ
  54  originZ : Fin 4 → ℤ
  55
  56def toReal12 (c : SeedEdgeContribZ) : SeedEdgeContrib where
  57  cls := c.cls
  58  weight := (c.weightZ : ℝ) * Real.sqrt 2 / 4
  59  origin := fun i => (c.originZ i : ℝ)
  60
  61def toReal13 (c : SeedEdgeContribZ) : SeedEdgeContrib where
  62  cls := c.cls
  63  weight := (c.weightZ : ℝ) * Real.sqrt 3 / 12
  64  origin := fun i => (c.originZ i : ℝ)
  65
  66def toReal22 (c : SeedEdgeContribZ) : SeedEdgeContrib where
  67  cls := c.cls
  68  weight := (c.weightZ : ℝ) / 4
  69  origin := fun i => (c.originZ i : ℝ)
  70
  71def seedEdgeContribsZ_t12 : List SeedEdgeContribZ :=
  72  [
  73
  74    ⟨(5 : Fin 15), (-1 : ℤ), ![1, 0, 0, 0]⟩,
  75    ⟨(13 : Fin 15), (1 : ℤ), ![1, 0, 0, 0]⟩,
  76    ⟨(3 : Fin 15), (2 : ℤ), ![1, 1, 0, 0]⟩,
  77    ⟨(7 : Fin 15), (1 : ℤ), ![1, 1, 1, 0]⟩,
  78    ⟨(11 : Fin 15), (-2 : ℤ), ![1, 1, 0, 0]⟩,
  79    ⟨(5 : Fin 15), (-1 : ℤ), ![1, 0, 0, 0]⟩,
  80    ⟨(13 : Fin 15), (1 : ℤ), ![1, 0, 0, 0]⟩,
  81    ⟨(1 : Fin 15), (2 : ℤ), ![1, 0, 1, 0]⟩,
  82    ⟨(7 : Fin 15), (1 : ℤ), ![1, 1, 1, 0]⟩,
  83    ⟨(9 : Fin 15), (-2 : ℤ), ![1, 0, 1, 0]⟩,
  84    ⟨(0 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
  85    ⟨(6 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
  86    ⟨(2 : Fin 15), (2 : ℤ), ![0, 0, 0, 0]⟩,
  87    ⟨(8 : Fin 15), (1 : ℤ), ![0, 0, 0, -1]⟩,
  88    ⟨(14 : Fin 15), (1 : ℤ), ![0, 0, 0, -1]⟩,
  89    ⟨(10 : Fin 15), (-2 : ℤ), ![0, 0, 0, -1]⟩,
  90    ⟨(0 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
  91    ⟨(6 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
  92    ⟨(4 : Fin 15), (2 : ℤ), ![0, 0, 0, 0]⟩,
  93    ⟨(8 : Fin 15), (1 : ℤ), ![0, 0, 0, -1]⟩,
  94    ⟨(14 : Fin 15), (1 : ℤ), ![0, 0, 0, -1]⟩,
  95    ⟨(12 : Fin 15), (-2 : ℤ), ![0, 0, 0, -1]⟩
  96
  97  ]
  98
  99def seedEdgeContribsZ_t13 : List SeedEdgeContribZ :=
 100  [
 101
 102    ⟨(13 : Fin 15), (-2 : ℤ), ![1, 0, 0, 0]⟩,
 103    ⟨(5 : Fin 15), (3 : ℤ), ![1, 0, 0, 0]⟩,
 104    ⟨(11 : Fin 15), (3 : ℤ), ![1, 1, 0, 0]⟩,
 105    ⟨(3 : Fin 15), (-6 : ℤ), ![1, 1, 0, 0]⟩,
 106    ⟨(13 : Fin 15), (-2 : ℤ), ![1, 0, 0, 0]⟩,
 107    ⟨(9 : Fin 15), (3 : ℤ), ![1, 0, 0, 0]⟩,
 108    ⟨(11 : Fin 15), (3 : ℤ), ![1, 1, 0, 0]⟩,
 109    ⟨(7 : Fin 15), (-6 : ℤ), ![1, 1, 0, 0]⟩,
 110    ⟨(13 : Fin 15), (-2 : ℤ), ![1, 0, 0, 0]⟩,
 111    ⟨(5 : Fin 15), (3 : ℤ), ![1, 0, 0, 0]⟩,
 112    ⟨(9 : Fin 15), (3 : ℤ), ![1, 0, 1, 0]⟩,
 113    ⟨(1 : Fin 15), (-6 : ℤ), ![1, 0, 1, 0]⟩,
 114    ⟨(13 : Fin 15), (-2 : ℤ), ![1, 0, 0, 0]⟩,
 115    ⟨(11 : Fin 15), (3 : ℤ), ![1, 0, 0, 0]⟩,
 116    ⟨(9 : Fin 15), (3 : ℤ), ![1, 0, 1, 0]⟩,
 117    ⟨(7 : Fin 15), (-6 : ℤ), ![1, 0, 1, 0]⟩,
 118    ⟨(13 : Fin 15), (-2 : ℤ), ![1, 0, 0, 0]⟩,
 119    ⟨(9 : Fin 15), (3 : ℤ), ![1, 0, 0, 0]⟩,
 120    ⟨(5 : Fin 15), (3 : ℤ), ![1, 0, 0, 1]⟩,
 121    ⟨(1 : Fin 15), (-6 : ℤ), ![1, 0, 0, 1]⟩,
 122    ⟨(13 : Fin 15), (-2 : ℤ), ![1, 0, 0, 0]⟩,
 123    ⟨(11 : Fin 15), (3 : ℤ), ![1, 0, 0, 0]⟩,
 124    ⟨(5 : Fin 15), (3 : ℤ), ![1, 0, 0, 1]⟩,
 125    ⟨(3 : Fin 15), (-6 : ℤ), ![1, 0, 0, 1]⟩
 126
 127  ]
 128
 129def seedEdgeContribsZ_t22 : List SeedEdgeContribZ :=
 130  [
 131
 132    ⟨(2 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
 133    ⟨(14 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
 134    ⟨(6 : Fin 15), (2 : ℤ), ![0, 0, 0, 0]⟩,
 135    ⟨(11 : Fin 15), (-1 : ℤ), ![1, 1, 0, 0]⟩,
 136    ⟨(1 : Fin 15), (2 : ℤ), ![1, 0, 0, 0]⟩,
 137    ⟨(3 : Fin 15), (2 : ℤ), ![1, 1, 0, 0]⟩,
 138    ⟨(13 : Fin 15), (2 : ℤ), ![1, 0, 0, 0]⟩,
 139    ⟨(5 : Fin 15), (-4 : ℤ), ![1, 0, 0, 0]⟩,
 140    ⟨(2 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
 141    ⟨(14 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
 142    ⟨(10 : Fin 15), (2 : ℤ), ![0, 0, 0, 0]⟩,
 143    ⟨(11 : Fin 15), (-1 : ℤ), ![1, 1, 0, 0]⟩,
 144    ⟨(1 : Fin 15), (2 : ℤ), ![1, 0, 0, 0]⟩,
 145    ⟨(7 : Fin 15), (2 : ℤ), ![1, 1, 0, 0]⟩,
 146    ⟨(13 : Fin 15), (2 : ℤ), ![1, 0, 0, 0]⟩,
 147    ⟨(9 : Fin 15), (-4 : ℤ), ![1, 0, 0, 0]⟩,
 148    ⟨(2 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
 149    ⟨(14 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
 150    ⟨(6 : Fin 15), (2 : ℤ), ![0, 0, 0, 0]⟩,
 151    ⟨(11 : Fin 15), (-1 : ℤ), ![1, 1, 0, 0]⟩,
 152    ⟨(0 : Fin 15), (2 : ℤ), ![0, 1, 0, 0]⟩,
 153    ⟨(3 : Fin 15), (2 : ℤ), ![1, 1, 0, 0]⟩,
 154    ⟨(12 : Fin 15), (2 : ℤ), ![0, 1, 0, 0]⟩,
 155    ⟨(4 : Fin 15), (-4 : ℤ), ![0, 1, 0, 0]⟩,
 156    ⟨(2 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
 157    ⟨(14 : Fin 15), (-1 : ℤ), ![0, 0, 0, 0]⟩,
 158    ⟨(10 : Fin 15), (2 : ℤ), ![0, 0, 0, 0]⟩,
 159    ⟨(11 : Fin 15), (-1 : ℤ), ![1, 1, 0, 0]⟩,
 160    ⟨(0 : Fin 15), (2 : ℤ), ![0, 1, 0, 0]⟩,
 161    ⟨(7 : Fin 15), (2 : ℤ), ![1, 1, 0, 0]⟩,
 162    ⟨(12 : Fin 15), (2 : ℤ), ![0, 1, 0, 0]⟩,
 163    ⟨(8 : Fin 15), (-4 : ℤ), ![0, 1, 0, 0]⟩
 164
 165  ]
 166
 167def seedEdgeContribsZ_t21 : List SeedEdgeContribZ := seedEdgeContribsZ_t12
 168def seedEdgeContribsZ_t31 : List SeedEdgeContribZ := seedEdgeContribsZ_t13
 169
 170theorem seedEdgeContribsZ_t12_length : seedEdgeContribsZ_t12.length = 22 := rfl
 171theorem seedEdgeContribsZ_t13_length : seedEdgeContribsZ_t13.length = 24 := rfl
 172theorem seedEdgeContribsZ_t22_length : seedEdgeContribsZ_t22.length = 32 := rfl
 173
 174/-! ## §2. Integer phase at edge origins (symbolDir) -/
 175
 176def hingeBaseZ (s : Fin 24) (t : Fin 10) (i : Fin 4) : ℤ :=
 177  if Nat.testBit (triangleVertexMasks s t).1 i.val then (1 : ℤ) else 0
 178
 179def transportOriginZ (p : Fin 24) (off : Fin 4 → ℤ) (i : Fin 4) : ℤ :=
 180  ∑ j : Fin 4, if coordPermOf p j = i then off j else 0
 181
 182/-- `2 * phaseScale (base + transportOrigin off) d` for `symbolDir`. -/
 183def phase2EdgeSymbolZ (s : Fin 24) (t : Fin 10) (p : Fin 24)
 184    (off : Fin 4 → ℤ) (d : Fin 15) : ℤ :=
 185  2 * (hingeBaseZ s t 0 + transportOriginZ p off 0 +
 186        hingeBaseZ s t 1 + transportOriginZ p off 1) +
 187    (if classBit d 0 then (1 : ℤ) else 0) +
 188      (if classBit d 1 then (1 : ℤ) else 0)
 189
 190/-! ## §3. Per-orbit edge Kpp certificates -/
 191
 192def edgePhase2Z (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) (p : Fin 24)
 193    (c : SeedEdgeContribZ) : ℤ :=
 194  c.weightZ * cz (permClass p c.cls) *
 195    (phase2EdgeSymbolZ s t p c.originZ (permClass p c.cls)) ^ 2
 196
 197def slotKppEdge (seeds : List SeedEdgeContribZ) (cz : Fin 15 → ℤ)
 198    (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) : ℤ :=
 199  let p := orbitCoveringPerm ty s t
 200  (seeds.map (edgePhase2Z cz s t p)).sum
 201
 202def m2OrbitCertZ12Edge (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 203  if isOrbit .t12 s t then
 204    -slotAZ12 cz s t * slotKppEdge seedEdgeContribsZ_t12 cz .t12 s t
 205  else 0
 206
 207def m2OrbitCertZ21Edge (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 208  if isOrbit .t21 s t then
 209    -slotAZ21 cz s t * slotKppEdge seedEdgeContribsZ_t21 cz .t21 s t
 210  else 0
 211
 212def m2OrbitCertZ13Edge (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 213  if isOrbit .t13 s t then
 214    -slotAZ13 cz s t * slotKppEdge seedEdgeContribsZ_t13 cz .t13 s t
 215  else 0
 216
 217def m2OrbitCertZ31Edge (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 218  if isOrbit .t31 s t then
 219    -slotAZ31 cz s t * slotKppEdge seedEdgeContribsZ_t31 cz .t31 s t
 220  else 0
 221
 222def m2OrbitCertZ22Edge (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 223  if isOrbit .t22 s t then
 224    -slotAZ22 cz s t * slotKppEdge seedEdgeContribsZ_t22 cz .t22 s t
 225  else 0
 226
 227/-! ## §4. Pure-gauge counterexample coefficients -/
 228
 229/-- `gaugePart m v` for `m=(1,1,0,0)`, `v=e₂`: `2 (D₀+D₁) D₂`. -/
 230def gaugeM1100E2CoeffZ (d : Fin 15) : ℤ :=
 231  2 * ((if classBit d 0 then (1 : ℤ) else 0) +
 232        (if classBit d 1 then (1 : ℤ) else 0)) *
 233    (if classBit d 2 then (1 : ℤ) else 0)
 234
 235def gaugeM1100E2 : Mat4 :=
 236  gaugePart (![(1 : ℝ), (1 : ℝ), (0 : ℝ), (0 : ℝ)])
 237    (![(0 : ℝ), (0 : ℝ), (1 : ℝ), (0 : ℝ)])
 238
 239theorem classCoeff_gaugeM1100E2_int (d : Fin 15) :
 240    classCoeff gaugeM1100E2 d = (gaugeM1100E2CoeffZ d : ℝ) := by
 241  unfold gaugeM1100E2 gaugeM1100E2CoeffZ
 242  rw [classCoeff_gaugePart]
 243  simp [classDisp, Fin.sum_univ_four]
 244
 245/-! ## §5. Seed table bridges (real ↔ integer) -/
 246
 247theorem seedEdgeContribs_t12_eq_Z :
 248    seedEdgeContribs_t12 = seedEdgeContribsZ_t12.map toReal12 := by
 249  unfold seedEdgeContribs_t12 seedEdgeContribsZ_t12 toReal12
 250  rfl
 251
 252theorem seedEdgeContribs_t21_eq_Z :
 253    seedEdgeContribs_t21 = seedEdgeContribsZ_t21.map toReal12 := by
 254  simpa [seedEdgeContribs_t21, seedEdgeContribsZ_t21] using seedEdgeContribs_t12_eq_Z
 255
 256theorem seedEdgeContribs_t13_eq_Z :
 257    seedEdgeContribs_t13 = seedEdgeContribsZ_t13.map toReal13 := by
 258  unfold seedEdgeContribs_t13 seedEdgeContribsZ_t13 toReal13
 259  rfl
 260
 261theorem seedEdgeContribs_t31_eq_Z :
 262    seedEdgeContribs_t31 = seedEdgeContribsZ_t31.map toReal13 := by
 263  simpa [seedEdgeContribs_t31, seedEdgeContribsZ_t31] using seedEdgeContribs_t13_eq_Z
 264
 265theorem seedEdgeContribs_t22_eq_Z :
 266    seedEdgeContribs_t22 = seedEdgeContribsZ_t22.map toReal22 := by
 267  unfold seedEdgeContribs_t22 seedEdgeContribsZ_t22 toReal22
 268  rfl
 269
 270/-! ## §6. Phase bridge -/
 271
 272private lemma transportOrigin_int (p : Fin 24) (off : Fin 4 → ℤ) (i : Fin 4) :
 273    transportOrigin p (fun j => (off j : ℝ)) i = (transportOriginZ p off i : ℝ) := by
 274  unfold transportOrigin transportOriginZ
 275  rw [Int.cast_sum]
 276  refine Finset.sum_congr rfl fun j _ => ?_
 277  split_ifs <;> simp
 278
 279private lemma hingeBase_int (s : Fin 24) (t : Fin 10) (i : Fin 4) :
 280    hingeBase s t i = (hingeBaseZ s t i : ℝ) := by
 281  unfold hingeBase hingeBaseZ maskCoord
 282  split_ifs <;> simp
 283
 284theorem phaseScale_edge_eq_phase2EdgeSymbolZ (s : Fin 24) (t : Fin 10)
 285    (p : Fin 24) (off : Fin 4 → ℤ) (d : Fin 15) :
 286    phaseScale
 287        (fun i => hingeBase s t i + transportOrigin p (fun j => (off j : ℝ)) i) d =
 288      (phase2EdgeSymbolZ s t p off d : ℝ) / 2 := by
 289  unfold phaseScale phase2EdgeSymbolZ symbolDir
 290  simp only [Fin.sum_univ_four]
 291  have h0 := hingeBase_int s t (0 : Fin 4)
 292  have h1 := hingeBase_int s t (1 : Fin 4)
 293  have h2 := hingeBase_int s t (2 : Fin 4)
 294  have h3 := hingeBase_int s t (3 : Fin 4)
 295  have t0 := transportOrigin_int p off (0 : Fin 4)
 296  have t1 := transportOrigin_int p off (1 : Fin 4)
 297  have t2 := transportOrigin_int p off (2 : Fin 4)
 298  have t3 := transportOrigin_int p off (3 : Fin 4)
 299  simp [h0, h1, h2, h3, t0, t1, t2, t3, classDisp]
 300  --  (x0+x1) + (D0+D1)/2 = (2(x0+x1)+D0+D1)/2
 301  cases classBit d 0 <;> cases classBit d 1 <;> push_cast <;> ring
 302
 303/-! ## §7. Radical slot arithmetic (edge Kpp) -/
 304
 305private lemma sqrt2_mul_self : Real.sqrt 2 * Real.sqrt 2 = (2 : ℝ) := by
 306  simpa [pow_two] using Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)
 307
 308private lemma sqrt3_mul_self : Real.sqrt 3 * Real.sqrt 3 = (3 : ℝ) := by
 309  simpa [pow_two] using Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)
 310
 311private lemma radical2_edge_slot_arith (AZ K : ℤ) :
 312    Real.sqrt 2 * (AZ : ℝ) / 8 *
 313        (-(1 / 2 : ℝ) * (Real.sqrt 2 * (K : ℝ) / 16)) =
 314      ((-AZ * K : ℤ) : ℝ) / 128 := by
 315  have hs := sqrt2_mul_self
 316  ring_nf
 317  rw [show (Real.sqrt 2) ^ 2 = (2 : ℝ) by simpa [pow_two] using hs]
 318  push_cast; ring
 319
 320private lemma radical3_edge_slot_arith (AZ K : ℤ) :
 321    Real.sqrt 3 * (AZ : ℝ) / 12 *
 322        (-(1 / 2 : ℝ) * (Real.sqrt 3 * (K : ℝ) / 48)) =
 323      ((-AZ * K : ℤ) : ℝ) / 384 := by
 324  have hs := sqrt3_mul_self
 325  ring_nf
 326  rw [show (Real.sqrt 3) ^ 2 = (3 : ℝ) by simpa [pow_two] using hs]
 327  push_cast; ring
 328
 329private lemma rational_edge_slot_arith (AZ K : ℤ) :
 330    (AZ : ℝ) / 4 * (-(1 / 2 : ℝ) * ((K : ℝ) / 16)) =
 331      ((-AZ * K : ℤ) : ℝ) / 128 := by
 332  push_cast; ring
 333
 334private lemma sum_div_const_st (c : ℝ) (f : Fin 24 → Fin 10 → ℝ) :
 335    (∑ s : Fin 24, ∑ t : Fin 10, f s t / c) =
 336      (∑ s : Fin 24, ∑ t : Fin 10, f s t) / c := by
 337  simp_rw [div_eq_mul_inv, ← Finset.sum_mul]
 338
 339/-! ## §8. Phase² sum = radical × integer Kpp -/
 340
 341private lemma edgeContribPhase2_toReal12 (H : Mat4) (cz : Fin 15 → ℤ)
 342    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10)
 343    (p : Fin 24) (c : SeedEdgeContribZ) :
 344    edgeContribPhase2 p (hingeBase s t) H symbolDir (toReal12 c) =
 345      Real.sqrt 2 * (edgePhase2Z cz s t p c : ℝ) / 16 := by
 346  unfold edgeContribPhase2 toReal12 edgePhase2Z
 347  rw [hH, phaseScaleDir_symbolDir, phaseScale_edge_eq_phase2EdgeSymbolZ]
 348  push_cast; ring
 349
 350private lemma edgeContribPhase2_toReal13 (H : Mat4) (cz : Fin 15 → ℤ)
 351    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10)
 352    (p : Fin 24) (c : SeedEdgeContribZ) :
 353    edgeContribPhase2 p (hingeBase s t) H symbolDir (toReal13 c) =
 354      Real.sqrt 3 * (edgePhase2Z cz s t p c : ℝ) / 48 := by
 355  unfold edgeContribPhase2 toReal13 edgePhase2Z
 356  rw [hH, phaseScaleDir_symbolDir, phaseScale_edge_eq_phase2EdgeSymbolZ]
 357  push_cast; ring
 358
 359private lemma edgeContribPhase2_toReal22 (H : Mat4) (cz : Fin 15 → ℤ)
 360    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10)
 361    (p : Fin 24) (c : SeedEdgeContribZ) :
 362    edgeContribPhase2 p (hingeBase s t) H symbolDir (toReal22 c) =
 363      (edgePhase2Z cz s t p c : ℝ) / 16 := by
 364  unfold edgeContribPhase2 toReal22 edgePhase2Z
 365  rw [hH, phaseScaleDir_symbolDir, phaseScale_edge_eq_phase2EdgeSymbolZ]
 366  push_cast; ring
 367
 368private lemma list_sum_map_sqrt2_div16 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10)
 369    (p : Fin 24) (seeds : List SeedEdgeContribZ) (H : Mat4)
 370    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) :
 371    (seeds.map (fun c => edgeContribPhase2 p (hingeBase s t) H symbolDir (toReal12 c))).sum =
 372      Real.sqrt 2 * ((seeds.map (edgePhase2Z cz s t p)).sum : ℤ) / 16 := by
 373  induction seeds with
 374  | nil => simp
 375  | cons c rest ih =>
 376    simp [List.map, List.sum_cons, edgeContribPhase2_toReal12 H cz hH s t p c, ih]
 377    push_cast; ring
 378
 379private lemma list_sum_map_sqrt3_div48 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10)
 380    (p : Fin 24) (seeds : List SeedEdgeContribZ) (H : Mat4)
 381    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) :
 382    (seeds.map (fun c => edgeContribPhase2 p (hingeBase s t) H symbolDir (toReal13 c))).sum =
 383      Real.sqrt 3 * ((seeds.map (edgePhase2Z cz s t p)).sum : ℤ) / 48 := by
 384  induction seeds with
 385  | nil => simp
 386  | cons c rest ih =>
 387    simp [List.map, List.sum_cons, edgeContribPhase2_toReal13 H cz hH s t p c, ih]
 388    push_cast; ring
 389
 390private lemma list_sum_map_div16 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10)
 391    (p : Fin 24) (seeds : List SeedEdgeContribZ) (H : Mat4)
 392    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) :
 393    (seeds.map (fun c => edgeContribPhase2 p (hingeBase s t) H symbolDir (toReal22 c))).sum =
 394      ((seeds.map (edgePhase2Z cz s t p)).sum : ℤ) / 16 := by
 395  induction seeds with
 396  | nil => simp
 397  | cons c rest ih =>
 398    simp [List.map, List.sum_cons, edgeContribPhase2_toReal22 H cz hH s t p c, ih]
 399    push_cast; ring
 400
 401theorem slotOrbitDeficitPhase2EdgeOrigins_t12_eq_Z (H : Mat4) (cz : Fin 15 → ℤ)
 402    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 403    slotOrbitDeficitPhase2EdgeOrigins .t12 H symbolDir s t =
 404      Real.sqrt 2 *
 405        (slotKppEdge seedEdgeContribsZ_t12 cz .t12 s t : ℝ) / 16 := by
 406  unfold slotOrbitDeficitPhase2EdgeOrigins
 407  simp only [seedEdgeContribs]
 408  rw [seedEdgeContribs_t12_eq_Z, List.map_map]
 409  unfold slotKppEdge
 410  simpa [Function.comp] using
 411    list_sum_map_sqrt2_div16 cz s t (orbitCoveringPerm .t12 s t)
 412      seedEdgeContribsZ_t12 H hH
 413
 414theorem slotOrbitDeficitPhase2EdgeOrigins_t21_eq_Z (H : Mat4) (cz : Fin 15 → ℤ)
 415    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 416    slotOrbitDeficitPhase2EdgeOrigins .t21 H symbolDir s t =
 417      Real.sqrt 2 *
 418        (slotKppEdge seedEdgeContribsZ_t21 cz .t21 s t : ℝ) / 16 := by
 419  unfold slotOrbitDeficitPhase2EdgeOrigins
 420  simp only [seedEdgeContribs]
 421  rw [seedEdgeContribs_t21_eq_Z, List.map_map]
 422  unfold slotKppEdge
 423  simpa [Function.comp] using
 424    list_sum_map_sqrt2_div16 cz s t (orbitCoveringPerm .t21 s t)
 425      seedEdgeContribsZ_t21 H hH
 426
 427theorem slotOrbitDeficitPhase2EdgeOrigins_t13_eq_Z (H : Mat4) (cz : Fin 15 → ℤ)
 428    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 429    slotOrbitDeficitPhase2EdgeOrigins .t13 H symbolDir s t =
 430      Real.sqrt 3 *
 431        (slotKppEdge seedEdgeContribsZ_t13 cz .t13 s t : ℝ) / 48 := by
 432  unfold slotOrbitDeficitPhase2EdgeOrigins
 433  simp only [seedEdgeContribs]
 434  rw [seedEdgeContribs_t13_eq_Z, List.map_map]
 435  unfold slotKppEdge
 436  simpa [Function.comp] using
 437    list_sum_map_sqrt3_div48 cz s t (orbitCoveringPerm .t13 s t)
 438      seedEdgeContribsZ_t13 H hH
 439
 440theorem slotOrbitDeficitPhase2EdgeOrigins_t31_eq_Z (H : Mat4) (cz : Fin 15 → ℤ)
 441    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 442    slotOrbitDeficitPhase2EdgeOrigins .t31 H symbolDir s t =
 443      Real.sqrt 3 *
 444        (slotKppEdge seedEdgeContribsZ_t31 cz .t31 s t : ℝ) / 48 := by
 445  unfold slotOrbitDeficitPhase2EdgeOrigins
 446  simp only [seedEdgeContribs]
 447  rw [seedEdgeContribs_t31_eq_Z, List.map_map]
 448  unfold slotKppEdge
 449  simpa [Function.comp] using
 450    list_sum_map_sqrt3_div48 cz s t (orbitCoveringPerm .t31 s t)
 451      seedEdgeContribsZ_t31 H hH
 452
 453theorem slotOrbitDeficitPhase2EdgeOrigins_t22_eq_Z (H : Mat4) (cz : Fin 15 → ℤ)
 454    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 455    slotOrbitDeficitPhase2EdgeOrigins .t22 H symbolDir s t =
 456      (slotKppEdge seedEdgeContribsZ_t22 cz .t22 s t : ℝ) / 16 := by
 457  unfold slotOrbitDeficitPhase2EdgeOrigins
 458  simp only [seedEdgeContribs]
 459  rw [seedEdgeContribs_t22_eq_Z, List.map_map]
 460  unfold slotKppEdge
 461  simpa [Function.comp] using
 462    list_sum_map_div16 cz s t (orbitCoveringPerm .t22 s t)
 463      seedEdgeContribsZ_t22 H hH
 464
 465/-! ## §9. Area push helpers (local copies; sibling lemmas are private) -/
 466
 467private lemma area_push_sqrt2 (areaZ : Fin 15 → ℤ) (cz : Fin 15 → ℤ)
 468    (p : Fin 24) (H : Mat4) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
 469    (area : Fin 15 → ℝ)
 470    (harea : ∀ d, area d = Real.sqrt 2 * (areaZ d : ℝ) / 8) :
 471    (∑ d0 : Fin 15, area d0 * classCoeff H (permClass p d0)) =
 472      Real.sqrt 2 *
 473        (∑ d0 : Fin 15, areaZ d0 * cz (permClass p d0) : ℤ) / 8 := by
 474  simp_rw [harea, hH]
 475  calc
 476    (∑ d0 : Fin 15,
 477        Real.sqrt 2 * (areaZ d0 : ℝ) / 8 * (cz (permClass p d0) : ℝ)) =
 478        Real.sqrt 2 / 8 *
 479          ∑ d0 : Fin 15,
 480            (areaZ d0 : ℝ) * (cz (permClass p d0) : ℝ) := by
 481      refine Eq.trans ?_ (Finset.mul_sum _ _ _).symm
 482      refine Finset.sum_congr rfl fun d0 _ => by ring
 483    _ = Real.sqrt 2 *
 484          (∑ d0 : Fin 15, areaZ d0 * cz (permClass p d0) : ℤ) / 8 := by
 485      rw [Int.cast_sum]
 486      push_cast; ring
 487
 488private lemma area_push_sqrt3 (areaZ : Fin 15 → ℤ) (cz : Fin 15 → ℤ)
 489    (p : Fin 24) (H : Mat4) (hH : ∀ d, classCoeff H d = (cz d : ℝ))
 490    (area : Fin 15 → ℝ)
 491    (harea : ∀ d, area d = Real.sqrt 3 * (areaZ d : ℝ) / 12) :
 492    (∑ d0 : Fin 15, area d0 * classCoeff H (permClass p d0)) =
 493      Real.sqrt 3 *
 494        (∑ d0 : Fin 15, areaZ d0 * cz (permClass p d0) : ℤ) / 12 := by
 495  simp_rw [harea, hH]
 496  calc
 497    (∑ d0 : Fin 15,
 498        Real.sqrt 3 * (areaZ d0 : ℝ) / 12 * (cz (permClass p d0) : ℝ)) =
 499        Real.sqrt 3 / 12 *
 500          ∑ d0 : Fin 15,
 501            (areaZ d0 : ℝ) * (cz (permClass p d0) : ℝ) := by
 502      refine Eq.trans ?_ (Finset.mul_sum _ _ _).symm
 503      refine Finset.sum_congr rfl fun d0 _ => by ring
 504    _ = Real.sqrt 3 *
 505          (∑ d0 : Fin 15, areaZ d0 * cz (permClass p d0) : ℤ) / 12 := by
 506      rw [Int.cast_sum]
 507      push_cast; ring
 508
 509/-! ## §10. Slot coefficient = certificate / denom -/
 510
 511theorem m2OrbitSlotCoeffEdgeOrigins_t12_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 512    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 513    m2OrbitSlotCoeffEdgeOrigins .t12 H symbolDir s t =
 514      (m2OrbitCertZ12Edge cz s t : ℝ) / 128 := by
 515  unfold m2OrbitSlotCoeffEdgeOrigins m2OrbitCertZ12Edge
 516  by_cases ht : isOrbit .t12 s t
 517  · simp only [ht, ite_true]
 518    set p := orbitCoveringPerm .t12 s t with hp
 519    have hA :
 520        (∑ d : Fin 15, slotOrbitAreaCov .t12 s t d * classCoeff H d) =
 521          Real.sqrt 2 * (slotAZ12 cz s t : ℝ) / 8 := by
 522      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 523      rw [sum_mul_pushforward, ← hp]
 524      simpa [slotAZ12, hp] using
 525        area_push_sqrt2 area12Z cz p H hH areaCov12 areaCov12_eq_z
 526    rw [hA, slotOrbitDeficitPhase2EdgeOrigins_t12_eq_Z H cz hH s t]
 527    exact radical2_edge_slot_arith (slotAZ12 cz s t)
 528      (slotKppEdge seedEdgeContribsZ_t12 cz .t12 s t)
 529  · simp [ht]
 530
 531theorem m2OrbitSlotCoeffEdgeOrigins_t21_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 532    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 533    m2OrbitSlotCoeffEdgeOrigins .t21 H symbolDir s t =
 534      (m2OrbitCertZ21Edge cz s t : ℝ) / 128 := by
 535  unfold m2OrbitSlotCoeffEdgeOrigins m2OrbitCertZ21Edge
 536  by_cases ht : isOrbit .t21 s t
 537  · simp only [ht, ite_true]
 538    set p := orbitCoveringPerm .t21 s t with hp
 539    have hA :
 540        (∑ d : Fin 15, slotOrbitAreaCov .t21 s t d * classCoeff H d) =
 541          Real.sqrt 2 * (slotAZ21 cz s t : ℝ) / 8 := by
 542      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 543      rw [sum_mul_pushforward, ← hp]
 544      simpa [slotAZ21, hp] using
 545        area_push_sqrt2 area21Z cz p H hH areaCov21 areaCov21_eq_z
 546    rw [hA, slotOrbitDeficitPhase2EdgeOrigins_t21_eq_Z H cz hH s t]
 547    exact radical2_edge_slot_arith (slotAZ21 cz s t)
 548      (slotKppEdge seedEdgeContribsZ_t21 cz .t21 s t)
 549  · simp [ht]
 550
 551theorem m2OrbitSlotCoeffEdgeOrigins_t13_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 552    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 553    m2OrbitSlotCoeffEdgeOrigins .t13 H symbolDir s t =
 554      (m2OrbitCertZ13Edge cz s t : ℝ) / 384 := by
 555  unfold m2OrbitSlotCoeffEdgeOrigins m2OrbitCertZ13Edge
 556  by_cases ht : isOrbit .t13 s t
 557  · simp only [ht, ite_true]
 558    set p := orbitCoveringPerm .t13 s t with hp
 559    have hA :
 560        (∑ d : Fin 15, slotOrbitAreaCov .t13 s t d * classCoeff H d) =
 561          Real.sqrt 3 * (slotAZ13 cz s t : ℝ) / 12 := by
 562      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 563      rw [sum_mul_pushforward, ← hp]
 564      simpa [slotAZ13, hp] using
 565        area_push_sqrt3 area13Z cz p H hH areaCov13 areaCov13_eq_z
 566    rw [hA, slotOrbitDeficitPhase2EdgeOrigins_t13_eq_Z H cz hH s t]
 567    exact radical3_edge_slot_arith (slotAZ13 cz s t)
 568      (slotKppEdge seedEdgeContribsZ_t13 cz .t13 s t)
 569  · simp [ht]
 570
 571theorem m2OrbitSlotCoeffEdgeOrigins_t31_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 572    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 573    m2OrbitSlotCoeffEdgeOrigins .t31 H symbolDir s t =
 574      (m2OrbitCertZ31Edge cz s t : ℝ) / 384 := by
 575  unfold m2OrbitSlotCoeffEdgeOrigins m2OrbitCertZ31Edge
 576  by_cases ht : isOrbit .t31 s t
 577  · simp only [ht, ite_true]
 578    set p := orbitCoveringPerm .t31 s t with hp
 579    have hA :
 580        (∑ d : Fin 15, slotOrbitAreaCov .t31 s t d * classCoeff H d) =
 581          Real.sqrt 3 * (slotAZ31 cz s t : ℝ) / 12 := by
 582      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 583      rw [sum_mul_pushforward, ← hp]
 584      simpa [slotAZ31, hp] using
 585        area_push_sqrt3 area31Z cz p H hH areaCov31 areaCov31_eq_z
 586    rw [hA, slotOrbitDeficitPhase2EdgeOrigins_t31_eq_Z H cz hH s t]
 587    exact radical3_edge_slot_arith (slotAZ31 cz s t)
 588      (slotKppEdge seedEdgeContribsZ_t31 cz .t31 s t)
 589  · simp [ht]
 590
 591theorem m2OrbitSlotCoeffEdgeOrigins_t22_eq_cert (H : Mat4) (cz : Fin 15 → ℤ)
 592    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 593    m2OrbitSlotCoeffEdgeOrigins .t22 H symbolDir s t =
 594      (m2OrbitCertZ22Edge cz s t : ℝ) / 128 := by
 595  unfold m2OrbitSlotCoeffEdgeOrigins m2OrbitCertZ22Edge
 596  by_cases ht : isOrbit .t22 s t
 597  · simp only [ht, ite_true]
 598    set p := orbitCoveringPerm .t22 s t with hp
 599    have hA :
 600        (∑ d : Fin 15, slotOrbitAreaCov .t22 s t d * classCoeff H d) =
 601          (slotAZ22 cz s t : ℝ) / 4 := by
 602      simp only [slotOrbitAreaCov, transportedOrbitArea, orbitAreaCov]
 603      rw [sum_mul_pushforward, ← hp]
 604      unfold slotAZ22
 605      simp_rw [areaCov22_eq_z, hH]
 606      calc
 607        (∑ d0 : Fin 15,
 608            (area22Z d0 : ℝ) / 4 * (cz (permClass p d0) : ℝ)) =
 609            (∑ d0 : Fin 15, (area22Z d0 : ℝ) * (cz (permClass p d0) : ℝ)) /
 610              4 := by
 611          rw [Finset.sum_div]
 612          refine Finset.sum_congr rfl fun d0 _ => by ring
 613        _ = (∑ d0 : Fin 15, area22Z d0 * cz (permClass p d0) : ℤ) / 4 := by
 614          rw [Int.cast_sum]; push_cast; rfl
 615    rw [hA, slotOrbitDeficitPhase2EdgeOrigins_t22_eq_Z H cz hH s t]
 616    exact rational_edge_slot_arith (slotAZ22 cz s t)
 617      (slotKppEdge seedEdgeContribsZ_t22 cz .t22 s t)
 618  · simp [ht]
 619
 620/-! ## §10. Decidable integer sums (axis plus) -/
 621
 622set_option maxRecDepth 20000 in
 623set_option maxHeartbeats 12000000 in
 624theorem sum_m2OrbitCertZ12Edge_axis :
 625    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ12Edge axisTTPlusCoeffZ s t) =
 626      (0 : ℤ) := by
 627  decide
 628
 629set_option maxRecDepth 20000 in
 630set_option maxHeartbeats 12000000 in
 631theorem sum_m2OrbitCertZ21Edge_axis :
 632    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ21Edge axisTTPlusCoeffZ s t) =
 633      (0 : ℤ) := by
 634  decide
 635
 636set_option maxRecDepth 20000 in
 637set_option maxHeartbeats 12000000 in
 638theorem sum_m2OrbitCertZ13Edge_axis :
 639    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ13Edge axisTTPlusCoeffZ s t) =
 640      (576 : ℤ) := by
 641  decide
 642
 643set_option maxRecDepth 20000 in
 644set_option maxHeartbeats 12000000 in
 645theorem sum_m2OrbitCertZ31Edge_axis :
 646    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ31Edge axisTTPlusCoeffZ s t) =
 647      (0 : ℤ) := by
 648  decide
 649
 650set_option maxRecDepth 20000 in
 651set_option maxHeartbeats 12000000 in
 652theorem sum_m2OrbitCertZ22Edge_axis :
 653    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ22Edge axisTTPlusCoeffZ s t) =
 654      (0 : ℤ) := by
 655  decide
 656
 657/-! ## §11. Decidable integer sums (axis cross) -/
 658
 659set_option maxRecDepth 20000 in
 660set_option maxHeartbeats 12000000 in
 661theorem sum_m2OrbitCertZ12Edge_cross :
 662    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ12Edge axisTTCrossCoeffZ s t) =
 663      (-256 : ℤ) := by
 664  decide
 665
 666set_option maxRecDepth 20000 in
 667set_option maxHeartbeats 12000000 in
 668theorem sum_m2OrbitCertZ21Edge_cross :
 669    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ21Edge axisTTCrossCoeffZ s t) =
 670      (128 : ℤ) := by
 671  decide
 672
 673set_option maxRecDepth 20000 in
 674set_option maxHeartbeats 12000000 in
 675theorem sum_m2OrbitCertZ13Edge_cross :
 676    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ13Edge axisTTCrossCoeffZ s t) =
 677      (-576 : ℤ) := by
 678  decide
 679
 680set_option maxRecDepth 20000 in
 681set_option maxHeartbeats 12000000 in
 682theorem sum_m2OrbitCertZ31Edge_cross :
 683    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ31Edge axisTTCrossCoeffZ s t) =
 684      (-576 : ℤ) := by
 685  decide
 686
 687set_option maxRecDepth 20000 in
 688set_option maxHeartbeats 12000000 in
 689theorem sum_m2OrbitCertZ22Edge_cross :
 690    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ22Edge axisTTCrossCoeffZ s t) =
 691      (256 : ℤ) := by
 692  decide
 693
 694/-! ## §12. Decidable integer sums (decoyGauge / counterexample) -/
 695
 696set_option maxRecDepth 20000 in
 697set_option maxHeartbeats 12000000 in
 698theorem sum_m2OrbitCertZ12Edge_gauge :
 699    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ12Edge decoyGaugeCoeffZ s t) =
 700      (0 : ℤ) := by
 701  decide
 702
 703set_option maxRecDepth 20000 in
 704set_option maxHeartbeats 12000000 in
 705theorem sum_m2OrbitCertZ21Edge_gauge :
 706    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ21Edge decoyGaugeCoeffZ s t) =
 707      (0 : ℤ) := by
 708  decide
 709
 710set_option maxRecDepth 20000 in
 711set_option maxHeartbeats 12000000 in
 712theorem sum_m2OrbitCertZ13Edge_gauge :
 713    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ13Edge decoyGaugeCoeffZ s t) =
 714      (0 : ℤ) := by
 715  decide
 716
 717set_option maxRecDepth 20000 in
 718set_option maxHeartbeats 12000000 in
 719theorem sum_m2OrbitCertZ31Edge_gauge :
 720    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ31Edge decoyGaugeCoeffZ s t) =
 721      (0 : ℤ) := by
 722  decide
 723
 724set_option maxRecDepth 20000 in
 725set_option maxHeartbeats 12000000 in
 726theorem sum_m2OrbitCertZ22Edge_gauge :
 727    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ22Edge decoyGaugeCoeffZ s t) =
 728      (0 : ℤ) := by
 729  decide
 730
 731set_option maxRecDepth 20000 in
 732set_option maxHeartbeats 12000000 in
 733theorem sum_m2OrbitCertZ12Edge_counterex :
 734    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ12Edge gaugeM1100E2CoeffZ s t) =
 735      (256 : ℤ) := by
 736  decide
 737
 738set_option maxRecDepth 20000 in
 739set_option maxHeartbeats 12000000 in
 740theorem sum_m2OrbitCertZ21Edge_counterex :
 741    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ21Edge gaugeM1100E2CoeffZ s t) =
 742      (0 : ℤ) := by
 743  decide
 744
 745set_option maxRecDepth 20000 in
 746set_option maxHeartbeats 12000000 in
 747theorem sum_m2OrbitCertZ13Edge_counterex :
 748    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ13Edge gaugeM1100E2CoeffZ s t) =
 749      (-1152 : ℤ) := by
 750  decide
 751
 752set_option maxRecDepth 20000 in
 753set_option maxHeartbeats 12000000 in
 754theorem sum_m2OrbitCertZ31Edge_counterex :
 755    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ31Edge gaugeM1100E2CoeffZ s t) =
 756      (0 : ℤ) := by
 757  decide
 758
 759set_option maxRecDepth 20000 in
 760set_option maxHeartbeats 12000000 in
 761theorem sum_m2OrbitCertZ22Edge_counterex :
 762    (∑ s : Fin 24, ∑ t : Fin 10, m2OrbitCertZ22Edge gaugeM1100E2CoeffZ s t) =
 763      (0 : ℤ) := by
 764  decide
 765
 766set_option maxRecDepth 20000 in
 767set_option maxHeartbeats 12000000 in
 768theorem sum_m2SlotCertZ_counterex :
 769    (∑ s : Fin 24, ∑ t : Fin 10, m2SlotCertZ gaugeM1100E2CoeffZ s t) =
 770      (0 : ℤ) := by
 771  decide
 772
 773/-! ## §13. Per-orbit moment evaluations (plus / symbolDir) -/
 774
 775theorem m2OrbitMomentEdgeOrigins_t12_axis :
 776    m2OrbitMomentEdgeOrigins .t12 axisTTPlus symbolDir = (0 : ℝ) := by
 777  unfold m2OrbitMomentEdgeOrigins
 778  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t12_eq_cert axisTTPlus axisTTPlusCoeffZ
 779    classCoeff_axisTTPlus_int]
 780  have hsum :
 781      (∑ s : Fin 24, ∑ t : Fin 10,
 782          (m2OrbitCertZ12Edge axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
 783    simpa [Int.cast_sum] using
 784      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ12Edge_axis
 785  rw [sum_div_const_st, hsum]; norm_num
 786
 787theorem m2OrbitMomentEdgeOrigins_t21_axis :
 788    m2OrbitMomentEdgeOrigins .t21 axisTTPlus symbolDir = (0 : ℝ) := by
 789  unfold m2OrbitMomentEdgeOrigins
 790  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t21_eq_cert axisTTPlus axisTTPlusCoeffZ
 791    classCoeff_axisTTPlus_int]
 792  have hsum :
 793      (∑ s : Fin 24, ∑ t : Fin 10,
 794          (m2OrbitCertZ21Edge axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
 795    simpa [Int.cast_sum] using
 796      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ21Edge_axis
 797  rw [sum_div_const_st, hsum]; norm_num
 798
 799theorem m2OrbitMomentEdgeOrigins_t13_axis :
 800    m2OrbitMomentEdgeOrigins .t13 axisTTPlus symbolDir = (3 / 2 : ℝ) := by
 801  unfold m2OrbitMomentEdgeOrigins
 802  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t13_eq_cert axisTTPlus axisTTPlusCoeffZ
 803    classCoeff_axisTTPlus_int]
 804  have hsum :
 805      (∑ s : Fin 24, ∑ t : Fin 10,
 806          (m2OrbitCertZ13Edge axisTTPlusCoeffZ s t : ℝ)) = (576 : ℝ) := by
 807    simpa [Int.cast_sum] using
 808      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ13Edge_axis
 809  rw [sum_div_const_st, hsum]; norm_num
 810
 811theorem m2OrbitMomentEdgeOrigins_t31_axis :
 812    m2OrbitMomentEdgeOrigins .t31 axisTTPlus symbolDir = (0 : ℝ) := by
 813  unfold m2OrbitMomentEdgeOrigins
 814  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t31_eq_cert axisTTPlus axisTTPlusCoeffZ
 815    classCoeff_axisTTPlus_int]
 816  have hsum :
 817      (∑ s : Fin 24, ∑ t : Fin 10,
 818          (m2OrbitCertZ31Edge axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
 819    simpa [Int.cast_sum] using
 820      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ31Edge_axis
 821  rw [sum_div_const_st, hsum]; norm_num
 822
 823theorem m2OrbitMomentEdgeOrigins_t22_axis :
 824    m2OrbitMomentEdgeOrigins .t22 axisTTPlus symbolDir = (0 : ℝ) := by
 825  unfold m2OrbitMomentEdgeOrigins
 826  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t22_eq_cert axisTTPlus axisTTPlusCoeffZ
 827    classCoeff_axisTTPlus_int]
 828  have hsum :
 829      (∑ s : Fin 24, ∑ t : Fin 10,
 830          (m2OrbitCertZ22Edge axisTTPlusCoeffZ s t : ℝ)) = (0 : ℝ) := by
 831    simpa [Int.cast_sum] using
 832      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ22Edge_axis
 833  rw [sum_div_const_st, hsum]; norm_num
 834
 835/-! ## §14. Distinct-hinge assembly (plus) -/
 836
 837theorem m2AllOrbitMomentDistinctHingeEdgeOrigins_axisTTPlus_symbolDir :
 838    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir =
 839      (-1 / 4 : ℝ) := by
 840  unfold m2AllOrbitMomentDistinctHingeEdgeOrigins
 841  simp only [orbitStarSize]
 842  rw [m2TransportedOrbitMoment_t11_axis, m2OrbitMomentEdgeOrigins_t12_axis,
 843    m2OrbitMomentEdgeOrigins_t21_axis, m2OrbitMomentEdgeOrigins_t13_axis,
 844    m2OrbitMomentEdgeOrigins_t31_axis, m2OrbitMomentEdgeOrigins_t22_axis]
 845  -- `-3/6 + 0 + 0 + (3/2)/6 = -1/4`
 846  norm_num
 847
 848/-! ## §15. Cross orbit slices + distinct-hinge -/
 849
 850theorem m2OrbitMomentEdgeOrigins_t12_cross :
 851    m2OrbitMomentEdgeOrigins .t12 axisTTCross symbolDir = (-2 : ℝ) := by
 852  unfold m2OrbitMomentEdgeOrigins
 853  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t12_eq_cert axisTTCross axisTTCrossCoeffZ
 854    classCoeff_axisTTCross_int]
 855  have hsum :
 856      (∑ s : Fin 24, ∑ t : Fin 10,
 857          (m2OrbitCertZ12Edge axisTTCrossCoeffZ s t : ℝ)) = (-256 : ℝ) := by
 858    simpa [Int.cast_sum] using
 859      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ12Edge_cross
 860  rw [sum_div_const_st, hsum]; norm_num
 861
 862theorem m2OrbitMomentEdgeOrigins_t21_cross :
 863    m2OrbitMomentEdgeOrigins .t21 axisTTCross symbolDir = (1 : ℝ) := by
 864  unfold m2OrbitMomentEdgeOrigins
 865  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t21_eq_cert axisTTCross axisTTCrossCoeffZ
 866    classCoeff_axisTTCross_int]
 867  have hsum :
 868      (∑ s : Fin 24, ∑ t : Fin 10,
 869          (m2OrbitCertZ21Edge axisTTCrossCoeffZ s t : ℝ)) = (128 : ℝ) := by
 870    simpa [Int.cast_sum] using
 871      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ21Edge_cross
 872  rw [sum_div_const_st, hsum]; norm_num
 873
 874theorem m2OrbitMomentEdgeOrigins_t13_cross :
 875    m2OrbitMomentEdgeOrigins .t13 axisTTCross symbolDir = (-3 / 2 : ℝ) := by
 876  unfold m2OrbitMomentEdgeOrigins
 877  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t13_eq_cert axisTTCross axisTTCrossCoeffZ
 878    classCoeff_axisTTCross_int]
 879  have hsum :
 880      (∑ s : Fin 24, ∑ t : Fin 10,
 881          (m2OrbitCertZ13Edge axisTTCrossCoeffZ s t : ℝ)) = (-576 : ℝ) := by
 882    simpa [Int.cast_sum] using
 883      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ13Edge_cross
 884  rw [sum_div_const_st, hsum]; norm_num
 885
 886theorem m2OrbitMomentEdgeOrigins_t31_cross :
 887    m2OrbitMomentEdgeOrigins .t31 axisTTCross symbolDir = (-3 / 2 : ℝ) := by
 888  unfold m2OrbitMomentEdgeOrigins
 889  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t31_eq_cert axisTTCross axisTTCrossCoeffZ
 890    classCoeff_axisTTCross_int]
 891  have hsum :
 892      (∑ s : Fin 24, ∑ t : Fin 10,
 893          (m2OrbitCertZ31Edge axisTTCrossCoeffZ s t : ℝ)) = (-576 : ℝ) := by
 894    simpa [Int.cast_sum] using
 895      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ31Edge_cross
 896  rw [sum_div_const_st, hsum]; norm_num
 897
 898theorem m2OrbitMomentEdgeOrigins_t22_cross :
 899    m2OrbitMomentEdgeOrigins .t22 axisTTCross symbolDir = (2 : ℝ) := by
 900  unfold m2OrbitMomentEdgeOrigins
 901  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t22_eq_cert axisTTCross axisTTCrossCoeffZ
 902    classCoeff_axisTTCross_int]
 903  have hsum :
 904      (∑ s : Fin 24, ∑ t : Fin 10,
 905          (m2OrbitCertZ22Edge axisTTCrossCoeffZ s t : ℝ)) = (256 : ℝ) := by
 906    simpa [Int.cast_sum] using
 907      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ22Edge_cross
 908  rw [sum_div_const_st, hsum]; norm_num
 909
 910theorem m2AllOrbitMomentDistinctHingeEdgeOrigins_axisTTCross_symbolDir :
 911    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir =
 912      (-1 / 4 : ℝ) := by
 913  unfold m2AllOrbitMomentDistinctHingeEdgeOrigins
 914  simp only [orbitStarSize]
 915  rw [m2TransportedOrbitMoment_t11_cross, m2OrbitMomentEdgeOrigins_t12_cross,
 916    m2OrbitMomentEdgeOrigins_t21_cross, m2OrbitMomentEdgeOrigins_t13_cross,
 917    m2OrbitMomentEdgeOrigins_t31_cross, m2OrbitMomentEdgeOrigins_t22_cross]
 918  norm_num
 919
 920/-! ## §16. Gauge vanishing -/
 921
 922theorem m2OrbitMomentEdgeOrigins_t12_gauge :
 923    m2OrbitMomentEdgeOrigins .t12 decoyGauge symbolDir = (0 : ℝ) := by
 924  unfold m2OrbitMomentEdgeOrigins
 925  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t12_eq_cert decoyGauge decoyGaugeCoeffZ
 926    classCoeff_decoyGauge_int]
 927  have hsum :
 928      (∑ s : Fin 24, ∑ t : Fin 10,
 929          (m2OrbitCertZ12Edge decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 930    simpa [Int.cast_sum] using
 931      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ12Edge_gauge
 932  rw [sum_div_const_st, hsum]; norm_num
 933
 934theorem m2OrbitMomentEdgeOrigins_t21_gauge :
 935    m2OrbitMomentEdgeOrigins .t21 decoyGauge symbolDir = (0 : ℝ) := by
 936  unfold m2OrbitMomentEdgeOrigins
 937  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t21_eq_cert decoyGauge decoyGaugeCoeffZ
 938    classCoeff_decoyGauge_int]
 939  have hsum :
 940      (∑ s : Fin 24, ∑ t : Fin 10,
 941          (m2OrbitCertZ21Edge decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 942    simpa [Int.cast_sum] using
 943      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ21Edge_gauge
 944  rw [sum_div_const_st, hsum]; norm_num
 945
 946theorem m2OrbitMomentEdgeOrigins_t13_gauge :
 947    m2OrbitMomentEdgeOrigins .t13 decoyGauge symbolDir = (0 : ℝ) := by
 948  unfold m2OrbitMomentEdgeOrigins
 949  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t13_eq_cert decoyGauge decoyGaugeCoeffZ
 950    classCoeff_decoyGauge_int]
 951  have hsum :
 952      (∑ s : Fin 24, ∑ t : Fin 10,
 953          (m2OrbitCertZ13Edge decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 954    simpa [Int.cast_sum] using
 955      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ13Edge_gauge
 956  rw [sum_div_const_st, hsum]; norm_num
 957
 958theorem m2OrbitMomentEdgeOrigins_t31_gauge :
 959    m2OrbitMomentEdgeOrigins .t31 decoyGauge symbolDir = (0 : ℝ) := by
 960  unfold m2OrbitMomentEdgeOrigins
 961  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t31_eq_cert decoyGauge decoyGaugeCoeffZ
 962    classCoeff_decoyGauge_int]
 963  have hsum :
 964      (∑ s : Fin 24, ∑ t : Fin 10,
 965          (m2OrbitCertZ31Edge decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 966    simpa [Int.cast_sum] using
 967      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ31Edge_gauge
 968  rw [sum_div_const_st, hsum]; norm_num
 969
 970theorem m2OrbitMomentEdgeOrigins_t22_gauge :
 971    m2OrbitMomentEdgeOrigins .t22 decoyGauge symbolDir = (0 : ℝ) := by
 972  unfold m2OrbitMomentEdgeOrigins
 973  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t22_eq_cert decoyGauge decoyGaugeCoeffZ
 974    classCoeff_decoyGauge_int]
 975  have hsum :
 976      (∑ s : Fin 24, ∑ t : Fin 10,
 977          (m2OrbitCertZ22Edge decoyGaugeCoeffZ s t : ℝ)) = (0 : ℝ) := by
 978    simpa [Int.cast_sum] using
 979      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ22Edge_gauge
 980  rw [sum_div_const_st, hsum]; norm_num
 981
 982theorem m2AllOrbitMomentDistinctHingeEdgeOrigins_decoyGauge_symbolDir :
 983    m2AllOrbitMomentDistinctHingeEdgeOrigins decoyGauge symbolDir = (0 : ℝ) := by
 984  unfold m2AllOrbitMomentDistinctHingeEdgeOrigins
 985  simp only [orbitStarSize]
 986  rw [m2TransportedOrbitMoment_t11_gauge, m2OrbitMomentEdgeOrigins_t12_gauge,
 987    m2OrbitMomentEdgeOrigins_t21_gauge, m2OrbitMomentEdgeOrigins_t13_gauge,
 988    m2OrbitMomentEdgeOrigins_t31_gauge, m2OrbitMomentEdgeOrigins_t22_gauge]
 989  ring
 990
 991/-! ## §17. Counterexample m=(1,1,0,0), v=e₂ -/
 992
 993theorem m2Symbol_gaugeM1100E2 : m2Symbol gaugeM1100E2 = (0 : ℝ) := by
 994  unfold m2Symbol
 995  simp_rw [m2SlotCoeff_eq_cert gaugeM1100E2 gaugeM1100E2CoeffZ
 996    classCoeff_gaugeM1100E2_int]
 997  have hsum :
 998      (∑ s : Fin 24, ∑ t : Fin 10,
 999          (m2SlotCertZ gaugeM1100E2CoeffZ s t : ℝ)) = (0 : ℝ) := by
1000    simpa [Int.cast_sum] using
1001      congrArg (fun n : ℤ => (n : ℝ)) sum_m2SlotCertZ_counterex
1002  rw [sum_div_const_st, hsum]; norm_num
1003
1004theorem m2TransportedOrbitMoment_t11_counterex :
1005    m2TransportedOrbitMoment .t11 gaugeM1100E2 symbolDir = (0 : ℝ) := by
1006  rw [m2TransportedOrbitMoment_t11, m2Symbol_gaugeM1100E2]
1007
1008theorem m2OrbitMomentEdgeOrigins_t12_counterex :
1009    m2OrbitMomentEdgeOrigins .t12 gaugeM1100E2 symbolDir = (2 : ℝ) := by
1010  unfold m2OrbitMomentEdgeOrigins
1011  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t12_eq_cert gaugeM1100E2 gaugeM1100E2CoeffZ
1012    classCoeff_gaugeM1100E2_int]
1013  have hsum :
1014      (∑ s : Fin 24, ∑ t : Fin 10,
1015          (m2OrbitCertZ12Edge gaugeM1100E2CoeffZ s t : ℝ)) = (256 : ℝ) := by
1016    simpa [Int.cast_sum] using
1017      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ12Edge_counterex
1018  rw [sum_div_const_st, hsum]; norm_num
1019
1020theorem m2OrbitMomentEdgeOrigins_t21_counterex :
1021    m2OrbitMomentEdgeOrigins .t21 gaugeM1100E2 symbolDir = (0 : ℝ) := by
1022  unfold m2OrbitMomentEdgeOrigins
1023  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t21_eq_cert gaugeM1100E2 gaugeM1100E2CoeffZ
1024    classCoeff_gaugeM1100E2_int]
1025  have hsum :
1026      (∑ s : Fin 24, ∑ t : Fin 10,
1027          (m2OrbitCertZ21Edge gaugeM1100E2CoeffZ s t : ℝ)) = (0 : ℝ) := by
1028    simpa [Int.cast_sum] using
1029      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ21Edge_counterex
1030  rw [sum_div_const_st, hsum]; norm_num
1031
1032theorem m2OrbitMomentEdgeOrigins_t13_counterex :
1033    m2OrbitMomentEdgeOrigins .t13 gaugeM1100E2 symbolDir = (-3 : ℝ) := by
1034  unfold m2OrbitMomentEdgeOrigins
1035  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t13_eq_cert gaugeM1100E2 gaugeM1100E2CoeffZ
1036    classCoeff_gaugeM1100E2_int]
1037  have hsum :
1038      (∑ s : Fin 24, ∑ t : Fin 10,
1039          (m2OrbitCertZ13Edge gaugeM1100E2CoeffZ s t : ℝ)) = (-1152 : ℝ) := by
1040    simpa [Int.cast_sum] using
1041      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ13Edge_counterex
1042  rw [sum_div_const_st, hsum]; norm_num
1043
1044theorem m2OrbitMomentEdgeOrigins_t31_counterex :
1045    m2OrbitMomentEdgeOrigins .t31 gaugeM1100E2 symbolDir = (0 : ℝ) := by
1046  unfold m2OrbitMomentEdgeOrigins
1047  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t31_eq_cert gaugeM1100E2 gaugeM1100E2CoeffZ
1048    classCoeff_gaugeM1100E2_int]
1049  have hsum :
1050      (∑ s : Fin 24, ∑ t : Fin 10,
1051          (m2OrbitCertZ31Edge gaugeM1100E2CoeffZ s t : ℝ)) = (0 : ℝ) := by
1052    simpa [Int.cast_sum] using
1053      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ31Edge_counterex
1054  rw [sum_div_const_st, hsum]; norm_num
1055
1056theorem m2OrbitMomentEdgeOrigins_t22_counterex :
1057    m2OrbitMomentEdgeOrigins .t22 gaugeM1100E2 symbolDir = (0 : ℝ) := by
1058  unfold m2OrbitMomentEdgeOrigins
1059  simp_rw [m2OrbitSlotCoeffEdgeOrigins_t22_eq_cert gaugeM1100E2 gaugeM1100E2CoeffZ
1060    classCoeff_gaugeM1100E2_int]
1061  have hsum :
1062      (∑ s : Fin 24, ∑ t : Fin 10,
1063          (m2OrbitCertZ22Edge gaugeM1100E2CoeffZ s t : ℝ)) = (0 : ℝ) := by
1064    simpa [Int.cast_sum] using
1065      congrArg (fun n : ℤ => (n : ℝ)) sum_m2OrbitCertZ22Edge_counterex
1066  rw [sum_div_const_st, hsum]; norm_num
1067
1068theorem m2AllOrbitMomentDistinctHingeEdgeOrigins_gaugeM1100E2_symbolDir :
1069    m2AllOrbitMomentDistinctHingeEdgeOrigins gaugeM1100E2 symbolDir = (0 : ℝ) := by
1070  unfold m2AllOrbitMomentDistinctHingeEdgeOrigins
1071  simp only [orbitStarSize]
1072  rw [m2TransportedOrbitMoment_t11_counterex, m2OrbitMomentEdgeOrigins_t12_counterex,
1073    m2OrbitMomentEdgeOrigins_t21_counterex, m2OrbitMomentEdgeOrigins_t13_counterex,
1074    m2OrbitMomentEdgeOrigins_t31_counterex, m2OrbitMomentEdgeOrigins_t22_counterex]
1075  norm_num
1076
1077/-! ## §18. Status -/
1078
1079structure EdgeOriginsM2EvalStatus where
1080  plusSymbolDir : Bool
1081  crossSymbolDir : Bool
1082  decoyGaugeSymbolDir : Bool
1083  counterexM1100E2 : Bool
1084  gapActionRecovery : Bool
1085  base0Forbidden : Bool
1086
1087def edgeOriginsM2EvalStatus : EdgeOriginsM2EvalStatus where
1088  plusSymbolDir := true
1089  crossSymbolDir := true
1090  decoyGaugeSymbolDir := true
1091  counterexM1100E2 := true
1092  gapActionRecovery := false
1093  base0Forbidden := true
1094
1095theorem edgeOriginsM2EvalStatus_flags :
1096    edgeOriginsM2EvalStatus.plusSymbolDir = true ∧
1097      edgeOriginsM2EvalStatus.crossSymbolDir = true ∧
1098        edgeOriginsM2EvalStatus.decoyGaugeSymbolDir = true ∧
1099          edgeOriginsM2EvalStatus.counterexM1100E2 = true ∧
1100            edgeOriginsM2EvalStatus.gapActionRecovery = false ∧
1101              edgeOriginsM2EvalStatus.base0Forbidden = true := by
1102  decide
1103
1104/-- Closed targets (inhabited by the theorems above). -/
1105def M2EdgeOriginsPlusSymbolDirEval : Prop :=
1106  m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir = (-1 / 4 : ℝ)
1107
1108def M2EdgeOriginsCrossSymbolDirEval : Prop :=
1109  m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir = (-1 / 4 : ℝ)
1110
1111def M2EdgeOriginsDecoyGaugeEval : Prop :=
1112  m2AllOrbitMomentDistinctHingeEdgeOrigins decoyGauge symbolDir = (0 : ℝ)
1113
1114def M2EdgeOriginsCounterexM1100E2Eval : Prop :=
1115  m2AllOrbitMomentDistinctHingeEdgeOrigins gaugeM1100E2 symbolDir = (0 : ℝ)
1116
1117theorem M2EdgeOriginsPlusSymbolDirEval_holds : M2EdgeOriginsPlusSymbolDirEval :=
1118  m2AllOrbitMomentDistinctHingeEdgeOrigins_axisTTPlus_symbolDir
1119
1120theorem M2EdgeOriginsCrossSymbolDirEval_holds : M2EdgeOriginsCrossSymbolDirEval :=
1121  m2AllOrbitMomentDistinctHingeEdgeOrigins_axisTTCross_symbolDir
1122
1123theorem M2EdgeOriginsDecoyGaugeEval_holds : M2EdgeOriginsDecoyGaugeEval :=
1124  m2AllOrbitMomentDistinctHingeEdgeOrigins_decoyGauge_symbolDir
1125
1126theorem M2EdgeOriginsCounterexM1100E2Eval_holds :
1127    M2EdgeOriginsCounterexM1100E2Eval :=
1128  m2AllOrbitMomentDistinctHingeEdgeOrigins_gaugeM1100E2_symbolDir
1129
1130end
1131
1132end ReggeBlochStarEdgeOriginsM2Eval4D
1133end Analysis
1134end Gravity
1135end IndisputableMonolith
1136