IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
   3import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12
   4import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel13
   5import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22
   6import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
   7import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
   8
   9/-!
  10# Regge 4D flat Hessian assembly (zero-momentum true weights)
  11
  12QG full-theory campaign: assemble the committed per-orbit star deficit
  13kernels with Heron area gradients into the flat second-variation class
  14quadratic of the 4D Regge action, replacing the provisional weight-1
  15aggregate of `ReggeEdgeStencil4D.finiteTTQuadratic`.
  16
  17## Tier tags (binding)
  18
  19* THEOREM: every named theorem below (kernel-checked; no `sorry`, no
  20  `admit`, no new axioms, no `native_decide`, no `: True` shells).
  21* Scope: **zero-momentum** (constant edge-class perturbation) per-cell
  22  Hessian only.  Finite-momentum Bloch phase folding across hinge
  23  translates is **OPEN**.
  24* This does **not** prove `S_RS_converges_EH_4d`.
  25* This does **not** flip `gap_action_recovery`.
  26* This does **not** reverse-engineer weights from Einstein–Hilbert: all
  27  orbit counts, area gradients, and deficit kernels come from the
  28  committed geometry modules imported above.
  29
  30## What is proved (deliverable A)
  31
  321. **Area gradients.** For each of the four committed flat triangle
  33   representatives `(a,b,c) ∈ {(1,1,2),(1,2,3),(1,3,4),(2,2,4)}`, the
  34   Heron form `A² = (2ab+2bc+2ca−a²−b²−c²)/16` yields explicit
  35   `HasDerivAt` theorems for `∂A/∂a`, `∂A/∂b`, `∂A/∂c` at flat, with
  36   closed values recorded below.
  372. **Complement transport (identity on edge classes).** Vertex
  38   complement `m ↦ m ⊕ 15` preserves difference masks
  39   (`(u⊕15)⊕(v⊕15) = u⊕v`), so edge-class indices are invariant.
  40   Therefore the type-`(2,1)` (resp. `(3,1)`) star class kernel equals
  41   the committed type-`(1,2)` (resp. `(1,3)`) kernel on `Fin 15`.
  423. **Zero-momentum true-weight Hessian.** Orbit-count-weighted sum of
  43   `(dA · c)(dδ · c)` over the six `S₄` types, with counts
  44   `72/48/48/24/24/24`.
  454. **Polarization / bilinearity** of the associated symmetric bilinear
  46   form.
  475. **Evaluations** on `axisTTPlus`, `decoyGauge`, and `decoyTrace`:
  48   all three equal `0`.  True weights **kill pure gauge** at zero
  49   momentum (provisional weight-1 gave `32` on the same decoy).
  506. **Homothety** direction evaluates to `0`.
  51
  52Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  53-/
  54
  55namespace IndisputableMonolith
  56namespace Gravity
  57namespace Analysis
  58namespace ReggeFlat4DHessianAssembly
  59
  60open BigOperators
  61open ReggeEdgeStencil4D
  62open ReggeHinge4DOrbitClassification
  63open EdgeTTDecomposition4D
  64
  65noncomputable section
  66
  67/-! ## §1. Heron area and coordinate derivatives -/
  68
  69def heronSq (a b c : ℝ) : ℝ :=
  70  (2 * a * b + 2 * b * c + 2 * c * a - a ^ 2 - b ^ 2 - c ^ 2) / 16
  71
  72def hingeArea (a b c : ℝ) : ℝ := Real.sqrt (heronSq a b c)
  73
  74def areaGradA (a b c : ℝ) : ℝ :=
  75  (b + c - a) / (16 * hingeArea a b c)
  76
  77def areaGradB (a b c : ℝ) : ℝ :=
  78  (a + c - b) / (16 * hingeArea a b c)
  79
  80def areaGradC (a b c : ℝ) : ℝ :=
  81  (a + b - c) / (16 * hingeArea a b c)
  82
  83private lemma hasDerivAt_quad_sub_sq (p q t0 : ℝ) :
  84    HasDerivAt (fun t : ℝ => p * t - t ^ 2 + q) (p - 2 * t0) t0 := by
  85  have hpow : HasDerivAt (fun t : ℝ => t ^ 2) (2 * t0) t0 := by
  86    simpa using hasDerivAt_pow 2 t0
  87  have hlin := ((hasDerivAt_id t0).const_mul p).sub hpow
  88  convert hlin.add_const q using 1
  89  ring
  90
  91theorem hasDerivAt_heronSq_a (a0 b c : ℝ) :
  92    HasDerivAt (fun t : ℝ => heronSq t b c) ((b + c - a0) / 8) a0 := by
  93  have hfun :
  94      (fun t : ℝ => heronSq t b c) =
  95        fun t : ℝ =>
  96          ((2 * b + 2 * c) * t - t ^ 2 + (2 * b * c - b ^ 2 - c ^ 2)) / 16 := by
  97    funext t; unfold heronSq; ring
  98  rw [hfun]
  99  have h :=
 100    (hasDerivAt_quad_sub_sq (2 * b + 2 * c) (2 * b * c - b ^ 2 - c ^ 2) a0).div_const
 101      (16 : ℝ)
 102  convert h using 1
 103  ring
 104
 105theorem hasDerivAt_heronSq_b (a b0 c : ℝ) :
 106    HasDerivAt (fun t : ℝ => heronSq a t c) ((a + c - b0) / 8) b0 := by
 107  have hfun :
 108      (fun t : ℝ => heronSq a t c) =
 109        fun t : ℝ =>
 110          ((2 * a + 2 * c) * t - t ^ 2 + (2 * a * c - a ^ 2 - c ^ 2)) / 16 := by
 111    funext t; unfold heronSq; ring
 112  rw [hfun]
 113  have h :=
 114    (hasDerivAt_quad_sub_sq (2 * a + 2 * c) (2 * a * c - a ^ 2 - c ^ 2) b0).div_const
 115      (16 : ℝ)
 116  convert h using 1
 117  ring
 118
 119theorem hasDerivAt_heronSq_c (a b c0 : ℝ) :
 120    HasDerivAt (fun t : ℝ => heronSq a b t) ((a + b - c0) / 8) c0 := by
 121  have hfun :
 122      (fun t : ℝ => heronSq a b t) =
 123        fun t : ℝ =>
 124          ((2 * a + 2 * b) * t - t ^ 2 + (2 * a * b - a ^ 2 - b ^ 2)) / 16 := by
 125    funext t; unfold heronSq; ring
 126  rw [hfun]
 127  have h :=
 128    (hasDerivAt_quad_sub_sq (2 * a + 2 * b) (2 * a * b - a ^ 2 - b ^ 2) c0).div_const
 129      (16 : ℝ)
 130  convert h using 1
 131  ring
 132
 133private lemma hasDerivAt_sqrt_heron_coord
 134    {F : ℝ → ℝ} {t0 F' : ℝ}
 135    (hF : HasDerivAt F F' t0) (hpos : 0 < F t0) :
 136    HasDerivAt (fun t : ℝ => Real.sqrt (F t))
 137      (F' / (2 * Real.sqrt (F t0))) t0 := by
 138  have hsqrt := (Real.hasDerivAt_sqrt (ne_of_gt hpos)).comp t0 hF
 139  convert hsqrt using 1
 140  ring
 141
 142theorem hasDerivAt_hingeArea_a (a0 b c : ℝ) (hpos : 0 < heronSq a0 b c) :
 143    HasDerivAt (fun t : ℝ => hingeArea t b c) (areaGradA a0 b c) a0 := by
 144  have h :=
 145    hasDerivAt_sqrt_heron_coord (hasDerivAt_heronSq_a a0 b c) hpos
 146  -- Goal derivative equality: areaGradA = heronSq'_a / (2 √heronSq)
 147  change HasDerivAt (fun t : ℝ => Real.sqrt (heronSq t b c))
 148      ((b + c - a0) / (16 * Real.sqrt (heronSq a0 b c))) a0
 149  convert h using 1
 150  ring
 151
 152theorem hasDerivAt_hingeArea_b (a b0 c : ℝ) (hpos : 0 < heronSq a b0 c) :
 153    HasDerivAt (fun t : ℝ => hingeArea a t c) (areaGradB a b0 c) b0 := by
 154  have h :=
 155    hasDerivAt_sqrt_heron_coord (hasDerivAt_heronSq_b a b0 c) hpos
 156  change HasDerivAt (fun t : ℝ => Real.sqrt (heronSq a t c))
 157      ((a + c - b0) / (16 * Real.sqrt (heronSq a b0 c))) b0
 158  convert h using 1
 159  ring
 160
 161theorem hasDerivAt_hingeArea_c (a b c0 : ℝ) (hpos : 0 < heronSq a b c0) :
 162    HasDerivAt (fun t : ℝ => hingeArea a b t) (areaGradC a b c0) c0 := by
 163  have h :=
 164    hasDerivAt_sqrt_heron_coord (hasDerivAt_heronSq_c a b c0) hpos
 165  change HasDerivAt (fun t : ℝ => Real.sqrt (heronSq a b t))
 166      ((a + b - c0) / (16 * Real.sqrt (heronSq a b c0))) c0
 167  convert h using 1
 168  ring
 169
 170/-! ## §2. Flat values on committed representatives -/
 171
 172theorem heronSq_t11 : heronSq 1 1 2 = 1 / 4 := by unfold heronSq; norm_num
 173theorem heronSq_t12 : heronSq 1 2 3 = 1 / 2 := by unfold heronSq; norm_num
 174theorem heronSq_t13 : heronSq 1 3 4 = 3 / 4 := by unfold heronSq; norm_num
 175theorem heronSq_t22 : heronSq 2 2 4 = 1 := by unfold heronSq; norm_num
 176
 177theorem hingeArea_t11 : hingeArea 1 1 2 = 1 / 2 := by
 178  unfold hingeArea
 179  rw [heronSq_t11, show (1 / 4 : ℝ) = ((1 : ℝ) / 2) ^ 2 by norm_num]
 180  exact Real.sqrt_sq (by norm_num)
 181
 182theorem hingeArea_t12 : hingeArea 1 2 3 = Real.sqrt 2 / 2 := by
 183  unfold hingeArea
 184  have h : (1 / 2 : ℝ) = (Real.sqrt 2 / 2) ^ 2 := by
 185    rw [div_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]; norm_num
 186  rw [heronSq_t12, h]
 187  exact Real.sqrt_sq (by positivity)
 188
 189theorem hingeArea_t13 : hingeArea 1 3 4 = Real.sqrt 3 / 2 := by
 190  unfold hingeArea
 191  have h : (3 / 4 : ℝ) = (Real.sqrt 3 / 2) ^ 2 := by
 192    rw [div_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]; norm_num
 193  rw [heronSq_t13, h]
 194  exact Real.sqrt_sq (by positivity)
 195
 196theorem hingeArea_t22 : hingeArea 2 2 4 = 1 := by
 197  unfold hingeArea; rw [heronSq_t22, Real.sqrt_one]
 198
 199theorem areaGradA_t11 : areaGradA 1 1 2 = 1 / 4 := by
 200  unfold areaGradA; rw [hingeArea_t11]; norm_num
 201theorem areaGradB_t11 : areaGradB 1 1 2 = 1 / 4 := by
 202  unfold areaGradB; rw [hingeArea_t11]; norm_num
 203theorem areaGradC_t11 : areaGradC 1 1 2 = 0 := by
 204  unfold areaGradC; rw [hingeArea_t11]; norm_num
 205
 206theorem areaGradA_t12 : areaGradA 1 2 3 = Real.sqrt 2 / 4 := by
 207  unfold areaGradA; rw [hingeArea_t12]
 208  have hs2 : Real.sqrt 2 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
 209  field_simp [hs2]
 210  rw [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
 211  norm_num
 212
 213theorem areaGradB_t12 : areaGradB 1 2 3 = Real.sqrt 2 / 8 := by
 214  unfold areaGradB; rw [hingeArea_t12]
 215  have hs2 : Real.sqrt 2 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
 216  field_simp [hs2]
 217  rw [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
 218  norm_num
 219
 220theorem areaGradC_t12 : areaGradC 1 2 3 = 0 := by
 221  unfold areaGradC; rw [hingeArea_t12]; ring
 222
 223theorem areaGradA_t13 : areaGradA 1 3 4 = Real.sqrt 3 / 4 := by
 224  unfold areaGradA; rw [hingeArea_t13]
 225  have hs3 : Real.sqrt 3 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
 226  field_simp [hs3]
 227  rw [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]
 228  norm_num
 229
 230theorem areaGradB_t13 : areaGradB 1 3 4 = Real.sqrt 3 / 12 := by
 231  unfold areaGradB; rw [hingeArea_t13]
 232  have hs3 : Real.sqrt 3 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
 233  field_simp [hs3]
 234  rw [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)]
 235  norm_num
 236
 237theorem areaGradC_t13 : areaGradC 1 3 4 = 0 := by
 238  unfold areaGradC; rw [hingeArea_t13]; ring
 239
 240theorem areaGradA_t22 : areaGradA 2 2 4 = 1 / 4 := by
 241  unfold areaGradA; rw [hingeArea_t22]; norm_num
 242theorem areaGradB_t22 : areaGradB 2 2 4 = 1 / 4 := by
 243  unfold areaGradB; rw [hingeArea_t22]; norm_num
 244theorem areaGradC_t22 : areaGradC 2 2 4 = 0 := by
 245  unfold areaGradC; rw [hingeArea_t22]; norm_num
 246
 247theorem hasDerivAt_area_t11_a :
 248    HasDerivAt (fun t : ℝ => hingeArea t 1 2) (1 / 4) 1 := by
 249  simpa [areaGradA_t11] using
 250    hasDerivAt_hingeArea_a 1 1 2 (by rw [heronSq_t11]; norm_num)
 251theorem hasDerivAt_area_t11_b :
 252    HasDerivAt (fun t : ℝ => hingeArea 1 t 2) (1 / 4) 1 := by
 253  simpa [areaGradB_t11] using
 254    hasDerivAt_hingeArea_b 1 1 2 (by rw [heronSq_t11]; norm_num)
 255theorem hasDerivAt_area_t11_c :
 256    HasDerivAt (fun t : ℝ => hingeArea 1 1 t) 0 2 := by
 257  simpa [areaGradC_t11] using
 258    hasDerivAt_hingeArea_c 1 1 2 (by rw [heronSq_t11]; norm_num)
 259
 260theorem hasDerivAt_area_t12_a :
 261    HasDerivAt (fun t : ℝ => hingeArea t 2 3) (Real.sqrt 2 / 4) 1 := by
 262  simpa [areaGradA_t12] using
 263    hasDerivAt_hingeArea_a 1 2 3 (by rw [heronSq_t12]; norm_num)
 264theorem hasDerivAt_area_t12_b :
 265    HasDerivAt (fun t : ℝ => hingeArea 1 t 3) (Real.sqrt 2 / 8) 2 := by
 266  simpa [areaGradB_t12] using
 267    hasDerivAt_hingeArea_b 1 2 3 (by rw [heronSq_t12]; norm_num)
 268theorem hasDerivAt_area_t12_c :
 269    HasDerivAt (fun t : ℝ => hingeArea 1 2 t) 0 3 := by
 270  simpa [areaGradC_t12] using
 271    hasDerivAt_hingeArea_c 1 2 3 (by rw [heronSq_t12]; norm_num)
 272
 273theorem hasDerivAt_area_t13_a :
 274    HasDerivAt (fun t : ℝ => hingeArea t 3 4) (Real.sqrt 3 / 4) 1 := by
 275  simpa [areaGradA_t13] using
 276    hasDerivAt_hingeArea_a 1 3 4 (by rw [heronSq_t13]; norm_num)
 277theorem hasDerivAt_area_t13_b :
 278    HasDerivAt (fun t : ℝ => hingeArea 1 t 4) (Real.sqrt 3 / 12) 3 := by
 279  simpa [areaGradB_t13] using
 280    hasDerivAt_hingeArea_b 1 3 4 (by rw [heronSq_t13]; norm_num)
 281theorem hasDerivAt_area_t13_c :
 282    HasDerivAt (fun t : ℝ => hingeArea 1 3 t) 0 4 := by
 283  simpa [areaGradC_t13] using
 284    hasDerivAt_hingeArea_c 1 3 4 (by rw [heronSq_t13]; norm_num)
 285
 286theorem hasDerivAt_area_t22_a :
 287    HasDerivAt (fun t : ℝ => hingeArea t 2 4) (1 / 4) 2 := by
 288  simpa [areaGradA_t22] using
 289    hasDerivAt_hingeArea_a 2 2 4 (by rw [heronSq_t22]; norm_num)
 290theorem hasDerivAt_area_t22_b :
 291    HasDerivAt (fun t : ℝ => hingeArea 2 t 4) (1 / 4) 2 := by
 292  simpa [areaGradB_t22] using
 293    hasDerivAt_hingeArea_b 2 2 4 (by rw [heronSq_t22]; norm_num)
 294theorem hasDerivAt_area_t22_c :
 295    HasDerivAt (fun t : ℝ => hingeArea 2 2 t) 0 4 := by
 296  simpa [areaGradC_t22] using
 297    hasDerivAt_hingeArea_c 2 2 4 (by rw [heronSq_t22]; norm_num)
 298
 299/-! ## §3. Complement transport (identity on edge classes) -/
 300
 301def complementMask (m : ℕ) : ℕ := Nat.xor m 15
 302
 303theorem complement_preserves_edge_mask (u v : ℕ) :
 304    Nat.xor (complementMask u) (complementMask v) = Nat.xor u v := by
 305  unfold complementMask
 306  -- (u ^^^ 15) ^^^ (v ^^^ 15) = u ^^^ v
 307  change (u ^^^ (15 : ℕ)) ^^^ (v ^^^ (15 : ℕ)) = u ^^^ v
 308  rw [Nat.xor_assoc u 15 (v ^^^ 15)]
 309  -- u ^^^ (15 ^^^ (v ^^^ 15))
 310  rw [Nat.xor_comm v 15]
 311  -- u ^^^ (15 ^^^ (15 ^^^ v))
 312  rw [← Nat.xor_assoc 15 15 v, Nat.xor_self 15, Nat.zero_xor]
 313
 314/-- Type `(2,1)` kernel = committed `(1,2)` kernel (identity transport). -/
 315def kernel21 : Fin 15 → ℝ :=
 316  ReggeHinge4DStarKernel12.fullStarClassKernel
 317
 318/-- Type `(3,1)` kernel = committed `(1,3)` kernel (identity transport). -/
 319def kernel31 : Fin 15 → ℝ :=
 320  ReggeHinge4DStarKernel13.fullStarClassKernel
 321
 322theorem kernel21_eq_kernel12 (d : Fin 15) :
 323    kernel21 d = ReggeHinge4DStarKernel12.fullStarClassKernel d := rfl
 324
 325theorem kernel31_eq_kernel13 (d : Fin 15) :
 326    kernel31 d = ReggeHinge4DStarKernel13.fullStarClassKernel d := rfl
 327
 328theorem complement_swaps_type_reexport (s : Fin 24) (t : Fin 10) :
 329    ∃ s' : Fin 24, ∃ t' : Fin 10,
 330      hingeTypePop s' t' =
 331        ((hingeTypePop s t).2, (hingeTypePop s t).1) :=
 332  complement_swaps_type s t
 333
 334/-! ## §4. Area covectors on the 15 classes -/
 335
 336def areaCov11 : Fin 15 → ℝ
 337  | ⟨0, _⟩ => 1 / 4
 338  | ⟨1, _⟩ => 1 / 4
 339  | ⟨2, _⟩ => 0
 340  | _ => 0
 341
 342def areaCov12 : Fin 15 → ℝ
 343  | ⟨0, _⟩ => Real.sqrt 2 / 4
 344  | ⟨5, _⟩ => Real.sqrt 2 / 8
 345  | ⟨6, _⟩ => 0
 346  | _ => 0
 347
 348def areaCov21 : Fin 15 → ℝ
 349  | ⟨2, _⟩ => Real.sqrt 2 / 8
 350  | ⟨3, _⟩ => Real.sqrt 2 / 4
 351  | ⟨6, _⟩ => 0
 352  | _ => 0
 353
 354def areaCov13 : Fin 15 → ℝ
 355  | ⟨0, _⟩ => Real.sqrt 3 / 4
 356  | ⟨13, _⟩ => Real.sqrt 3 / 12
 357  | ⟨14, _⟩ => 0
 358  | _ => 0
 359
 360def areaCov31 : Fin 15 → ℝ
 361  | ⟨6, _⟩ => Real.sqrt 3 / 12
 362  | ⟨7, _⟩ => Real.sqrt 3 / 4
 363  | ⟨14, _⟩ => 0
 364  | _ => 0
 365
 366def areaCov22 : Fin 15 → ℝ
 367  | ⟨2, _⟩ => 1 / 4
 368  | ⟨11, _⟩ => 1 / 4
 369  | ⟨14, _⟩ => 0
 370  | _ => 0
 371
 372theorem areaCov11_eq_grads :
 373    areaCov11 0 = areaGradA 1 1 2 ∧
 374      areaCov11 1 = areaGradB 1 1 2 ∧
 375        areaCov11 2 = areaGradC 1 1 2 := by
 376  simp [areaCov11, areaGradA_t11, areaGradB_t11, areaGradC_t11]
 377
 378theorem areaCov12_eq_grads :
 379    areaCov12 0 = areaGradA 1 2 3 ∧
 380      areaCov12 5 = areaGradB 1 2 3 ∧
 381        areaCov12 6 = areaGradC 1 2 3 := by
 382  simp [areaCov12, areaGradA_t12, areaGradB_t12, areaGradC_t12]
 383
 384theorem areaCov22_eq_grads :
 385    areaCov22 2 = areaGradA 2 2 4 ∧
 386      areaCov22 11 = areaGradB 2 2 4 ∧
 387        areaCov22 14 = areaGradC 2 2 4 := by
 388  simp [areaCov22, areaGradA_t22, areaGradB_t22, areaGradC_t22]
 389
 390/-! ## §5. Zero-momentum true-weight Hessian -/
 391
 392def orbitDeficitKernel : HingeOrbitType → Fin 15 → ℝ
 393  | .t11 => ReggeHinge4DStarKernel.fullStarClassKernel
 394  | .t12 => ReggeHinge4DStarKernel12.fullStarClassKernel
 395  | .t21 => kernel21
 396  | .t13 => ReggeHinge4DStarKernel13.fullStarClassKernel
 397  | .t31 => kernel31
 398  | .t22 => ReggeHinge4DStarKernel22.fullStarClassKernel
 399
 400def orbitAreaCov : HingeOrbitType → Fin 15 → ℝ
 401  | .t11 => areaCov11
 402  | .t12 => areaCov12
 403  | .t21 => areaCov21
 404  | .t13 => areaCov13
 405  | .t31 => areaCov31
 406  | .t22 => areaCov22
 407
 408def orbitCellCount : HingeOrbitType → ℕ
 409  | .t11 => 72
 410  | .t12 => 48
 411  | .t21 => 48
 412  | .t13 => 24
 413  | .t31 => 24
 414  | .t22 => 24
 415
 416theorem orbitCellCount_eq_classification (ty : HingeOrbitType) :
 417    orbitCellCount ty = cellTriangleCount ty.toPop := by
 418  cases ty <;> rfl
 419
 420/-- Dot of two class covectors. -/
 421def coeffDot (v w : Fin 15 → ℝ) : ℝ :=
 422  ∑ d : Fin 15, v d * w d
 423
 424def classDot (v : Fin 15 → ℝ) (H : Mat4) : ℝ :=
 425  coeffDot v (classCoeff H)
 426
 427def orbitZeroMomQuadratic (ty : HingeOrbitType) (H : Mat4) : ℝ :=
 428  (orbitCellCount ty : ℝ) *
 429    classDot (orbitAreaCov ty) H * classDot (orbitDeficitKernel ty) H
 430
 431def orbitZeroMomBilinear (ty : HingeOrbitType) (A B : Mat4) : ℝ :=
 432  (orbitCellCount ty : ℝ) / 2 *
 433    (classDot (orbitAreaCov ty) A * classDot (orbitDeficitKernel ty) B +
 434      classDot (orbitAreaCov ty) B * classDot (orbitDeficitKernel ty) A)
 435
 436def trueWeightZeroMomQuadratic (H : Mat4) : ℝ :=
 437  ∑ ty : HingeOrbitType, orbitZeroMomQuadratic ty H
 438
 439def trueWeightZeroMomBilinear (A B : Mat4) : ℝ :=
 440  ∑ ty : HingeOrbitType, orbitZeroMomBilinear ty A B
 441
 442theorem classDot_add (v : Fin 15 → ℝ) (A B : Mat4) :
 443    classDot v (A + B) = classDot v A + classDot v B := by
 444  unfold classDot coeffDot
 445  simp_rw [classCoeff_add, mul_add, Finset.sum_add_distrib]
 446
 447theorem classDot_smul (v : Fin 15 → ℝ) (c : ℝ) (A : Mat4) :
 448    classDot v (c • A) = c * classDot v A := by
 449  unfold classDot coeffDot
 450  simp_rw [classCoeff_smul]
 451  refine Eq.trans ?_ (Finset.mul_sum _ _ c).symm
 452  refine Finset.sum_congr rfl fun d _ => by ring
 453
 454theorem orbitZeroMomQuadratic_eq_bilinear (ty : HingeOrbitType) (H : Mat4) :
 455    orbitZeroMomQuadratic ty H = orbitZeroMomBilinear ty H H := by
 456  unfold orbitZeroMomQuadratic orbitZeroMomBilinear; ring
 457
 458theorem trueWeightZeroMomQuadratic_eq_bilinear (H : Mat4) :
 459    trueWeightZeroMomQuadratic H = trueWeightZeroMomBilinear H H := by
 460  unfold trueWeightZeroMomQuadratic trueWeightZeroMomBilinear
 461  exact Finset.sum_congr rfl fun ty _ => orbitZeroMomQuadratic_eq_bilinear ty H
 462
 463theorem trueWeightZeroMomBilinear_symm (A B : Mat4) :
 464    trueWeightZeroMomBilinear A B = trueWeightZeroMomBilinear B A := by
 465  unfold trueWeightZeroMomBilinear orbitZeroMomBilinear
 466  exact Finset.sum_congr rfl fun ty _ => by ring
 467
 468theorem trueWeightZeroMomBilinear_add_left (A₁ A₂ B : Mat4) :
 469    trueWeightZeroMomBilinear (A₁ + A₂) B =
 470      trueWeightZeroMomBilinear A₁ B + trueWeightZeroMomBilinear A₂ B := by
 471  unfold trueWeightZeroMomBilinear orbitZeroMomBilinear
 472  simp_rw [classDot_add]
 473  rw [← Finset.sum_add_distrib]
 474  exact Finset.sum_congr rfl fun ty _ => by ring
 475
 476theorem trueWeightZeroMomBilinear_smul_left (c : ℝ) (A B : Mat4) :
 477    trueWeightZeroMomBilinear (c • A) B = c * trueWeightZeroMomBilinear A B := by
 478  unfold trueWeightZeroMomBilinear orbitZeroMomBilinear
 479  simp_rw [classDot_smul]
 480  rw [Finset.mul_sum]
 481  exact Finset.sum_congr rfl fun ty _ => by ring
 482
 483theorem trueWeightZeroMomQuadratic_add (A B : Mat4) :
 484    trueWeightZeroMomQuadratic (A + B) =
 485      trueWeightZeroMomQuadratic A + trueWeightZeroMomQuadratic B +
 486        2 * trueWeightZeroMomBilinear A B := by
 487  -- Expand via bilinearity of classDot and algebra on each orbit summand.
 488  unfold trueWeightZeroMomQuadratic
 489  have hty : ∀ ty : HingeOrbitType,
 490      orbitZeroMomQuadratic ty (A + B) =
 491        orbitZeroMomQuadratic ty A + orbitZeroMomQuadratic ty B +
 492          2 * orbitZeroMomBilinear ty A B := by
 493    intro ty
 494    unfold orbitZeroMomQuadratic orbitZeroMomBilinear
 495    simp_rw [classDot_add]
 496    ring
 497  simp_rw [hty]
 498  rw [Finset.sum_add_distrib, Finset.sum_add_distrib, ← Finset.mul_sum]
 499  rfl
 500
 501/-! ## §6. Deficit kernels annihilate named class vectors
 502
 503Integer sign tables + `decide` on `ℤ`-sums; cast back to `ℝ`.
 504-/
 505
 506def axisTTPlusCoeffZ (d : Fin 15) : ℤ :=
 507  (if classBit d 2 then (1 : ℤ) else 0) - if classBit d 3 then 1 else 0
 508
 509theorem classCoeff_axisTTPlus_int (d : Fin 15) :
 510    classCoeff axisTTPlus d = (axisTTPlusCoeffZ d : ℝ) := by
 511  rw [classCoeff_axisTTPlus]
 512  unfold axisTTPlusCoeffZ
 513  cases classBit d 2 <;> cases classBit d 3 <;> norm_num
 514
 515/-- Integer class coefficients for `axisTTCross`: `2` when bits 2 and 3 are set. -/
 516def axisTTCrossCoeffZ (d : Fin 15) : ℤ :=
 517  2 * (if classBit d 2 && classBit d 3 then (1 : ℤ) else 0)
 518
 519theorem classCoeff_axisTTCross_int (d : Fin 15) :
 520    classCoeff axisTTCross d = (axisTTCrossCoeffZ d : ℝ) := by
 521  rw [classCoeff_axisTTCross]
 522  unfold axisTTCrossCoeffZ
 523  cases classBit d 2 <;> cases classBit d 3 <;> norm_num
 524
 525def gaugeBit0 (d : Fin 15) : ℕ := if classBit d 0 then 1 else 0
 526
 527theorem classCoeff_decoyGauge_bit (d : Fin 15) :
 528    classCoeff decoyGauge d = (2 : ℝ) * (gaugeBit0 d : ℝ) := by
 529  unfold decoyGauge gaugeBit0
 530  rw [classCoeff_gaugePart_axis]
 531  cases classBit d 0 <;> norm_num
 532
 533def kernel11Sign (d : Fin 15) : ℤ :=
 534  match d with
 535  | ⟨2, _⟩ => -1 | ⟨3, _⟩ => -1 | ⟨6, _⟩ => 1 | ⟨7, _⟩ => -1
 536  | ⟨10, _⟩ => 1 | ⟨11, _⟩ => 1 | ⟨14, _⟩ => -1
 537  | _ => 0
 538
 539theorem kernel11_eq_sign (d : Fin 15) :
 540    ReggeHinge4DStarKernel.fullStarClassKernel d = (kernel11Sign d : ℝ) := by
 541  fin_cases d <;> simp [ReggeHinge4DStarKernel.fullStarClassKernel, kernel11Sign]
 542
 543def kernel12Sign (d : Fin 15) : ℤ :=
 544  match d with
 545  | ⟨0, _⟩ => -1 | ⟨1, _⟩ => 1 | ⟨2, _⟩ => 1 | ⟨3, _⟩ => 1 | ⟨4, _⟩ => 1
 546  | ⟨5, _⟩ => -1 | ⟨6, _⟩ => -1 | ⟨7, _⟩ => 1 | ⟨8, _⟩ => 1 | ⟨9, _⟩ => -1
 547  | ⟨10, _⟩ => -1 | ⟨11, _⟩ => -1 | ⟨12, _⟩ => -1 | ⟨13, _⟩ => 1 | ⟨14, _⟩ => 1
 548
 549theorem kernel12_eq_sign (d : Fin 15) :
 550    ReggeHinge4DStarKernel12.fullStarClassKernel d =
 551      (kernel12Sign d : ℝ) * (Real.sqrt 2 / 2) := by
 552  fin_cases d <;>
 553    simp [ReggeHinge4DStarKernel12.fullStarClassKernel, kernel12Sign] <;> ring
 554
 555def kernel13Sign (d : Fin 15) : ℤ :=
 556  match d with
 557  | ⟨1, _⟩ => -1 | ⟨3, _⟩ => -1 | ⟨5, _⟩ => 1 | ⟨7, _⟩ => -1
 558  | ⟨9, _⟩ => 1 | ⟨11, _⟩ => 1 | ⟨13, _⟩ => -1
 559  | _ => 0
 560
 561theorem kernel13_eq_sign (d : Fin 15) :
 562    ReggeHinge4DStarKernel13.fullStarClassKernel d =
 563      (kernel13Sign d : ℝ) * Real.sqrt 3 := by
 564  fin_cases d <;>
 565    simp [ReggeHinge4DStarKernel13.fullStarClassKernel, kernel13Sign]
 566
 567def kernel22Sign (d : Fin 15) : ℤ :=
 568  match d with
 569  | ⟨0, _⟩ => 1 | ⟨1, _⟩ => 1 | ⟨2, _⟩ => -1 | ⟨3, _⟩ => 1 | ⟨4, _⟩ => -1
 570  | ⟨5, _⟩ => -1 | ⟨6, _⟩ => 1 | ⟨7, _⟩ => 1 | ⟨8, _⟩ => -1 | ⟨9, _⟩ => -1
 571  | ⟨10, _⟩ => 1 | ⟨11, _⟩ => -1 | ⟨12, _⟩ => 1 | ⟨13, _⟩ => 1 | ⟨14, _⟩ => -1
 572
 573theorem kernel22_eq_sign (d : Fin 15) :
 574    ReggeHinge4DStarKernel22.fullStarClassKernel d = (kernel22Sign d : ℝ) := by
 575  fin_cases d <;> simp [ReggeHinge4DStarKernel22.fullStarClassKernel, kernel22Sign]
 576
 577def signDotAxis (sign : Fin 15 → ℤ) : ℤ :=
 578  ∑ d : Fin 15, sign d * axisTTPlusCoeffZ d
 579
 580def signDotGauge (sign : Fin 15 → ℤ) : ℤ :=
 581  ∑ d : Fin 15, sign d * (2 * (gaugeBit0 d : ℤ))
 582
 583theorem signDotAxis_kernel11 : signDotAxis kernel11Sign = 0 := by
 584  unfold signDotAxis kernel11Sign axisTTPlusCoeffZ classBit maskOf; decide
 585theorem signDotAxis_kernel12 : signDotAxis kernel12Sign = 0 := by
 586  unfold signDotAxis kernel12Sign axisTTPlusCoeffZ classBit maskOf; decide
 587theorem signDotAxis_kernel13 : signDotAxis kernel13Sign = 0 := by
 588  unfold signDotAxis kernel13Sign axisTTPlusCoeffZ classBit maskOf; decide
 589theorem signDotAxis_kernel22 : signDotAxis kernel22Sign = 0 := by
 590  unfold signDotAxis kernel22Sign axisTTPlusCoeffZ classBit maskOf; decide
 591
 592theorem signDotGauge_kernel11 : signDotGauge kernel11Sign = 0 := by
 593  unfold signDotGauge kernel11Sign gaugeBit0 classBit maskOf; decide
 594theorem signDotGauge_kernel12 : signDotGauge kernel12Sign = 0 := by
 595  unfold signDotGauge kernel12Sign gaugeBit0 classBit maskOf; decide
 596theorem signDotGauge_kernel13 : signDotGauge kernel13Sign = 0 := by
 597  unfold signDotGauge kernel13Sign gaugeBit0 classBit maskOf; decide
 598theorem signDotGauge_kernel22 : signDotGauge kernel22Sign = 0 := by
 599  unfold signDotGauge kernel22Sign gaugeBit0 classBit maskOf; decide
 600
 601private lemma sum_sign_axis (sign : Fin 15 → ℤ) :
 602    (∑ d : Fin 15, (sign d : ℝ) * (axisTTPlusCoeffZ d : ℝ)) =
 603      (signDotAxis sign : ℝ) := by
 604  unfold signDotAxis; simp [Int.cast_sum, Int.cast_mul]
 605
 606private lemma sum_sign_gauge (sign : Fin 15 → ℤ) :
 607    (∑ d : Fin 15, (sign d : ℝ) * ((2 : ℝ) * (gaugeBit0 d : ℝ))) =
 608      (signDotGauge sign : ℝ) := by
 609  unfold signDotGauge
 610  have h : ∀ d,
 611      (sign d : ℝ) * ((2 : ℝ) * (gaugeBit0 d : ℝ)) =
 612        ((sign d * (2 * (gaugeBit0 d : ℤ)) : ℤ) : ℝ) := by
 613    intro d; push_cast; ring
 614  simp_rw [h, ← Int.cast_sum]
 615
 616theorem deficitKernel11_dot_axisTTPlus :
 617    classDot ReggeHinge4DStarKernel.fullStarClassKernel axisTTPlus = 0 := by
 618  unfold classDot coeffDot
 619  simp_rw [kernel11_eq_sign, classCoeff_axisTTPlus_int, sum_sign_axis,
 620    signDotAxis_kernel11]
 621  norm_num
 622
 623theorem deficitKernel22_dot_axisTTPlus :
 624    classDot ReggeHinge4DStarKernel22.fullStarClassKernel axisTTPlus = 0 := by
 625  unfold classDot coeffDot
 626  simp_rw [kernel22_eq_sign, classCoeff_axisTTPlus_int, sum_sign_axis,
 627    signDotAxis_kernel22]
 628  norm_num
 629
 630theorem deficitKernel12_dot_axisTTPlus :
 631    classDot ReggeHinge4DStarKernel12.fullStarClassKernel axisTTPlus = 0 := by
 632  unfold classDot coeffDot
 633  have h :
 634      (∑ d : Fin 15,
 635          ReggeHinge4DStarKernel12.fullStarClassKernel d *
 636            classCoeff axisTTPlus d) =
 637        (Real.sqrt 2 / 2) *
 638          ∑ d : Fin 15, (kernel12Sign d : ℝ) * (axisTTPlusCoeffZ d : ℝ) := by
 639    simp_rw [kernel12_eq_sign, classCoeff_axisTTPlus_int, Finset.mul_sum]
 640    exact Finset.sum_congr rfl fun d _ => by ring
 641  rw [h, sum_sign_axis, signDotAxis_kernel12]
 642  norm_num
 643
 644theorem deficitKernel13_dot_axisTTPlus :
 645    classDot ReggeHinge4DStarKernel13.fullStarClassKernel axisTTPlus = 0 := by
 646  unfold classDot coeffDot
 647  have h :
 648      (∑ d : Fin 15,
 649          ReggeHinge4DStarKernel13.fullStarClassKernel d *
 650            classCoeff axisTTPlus d) =
 651        Real.sqrt 3 *
 652          ∑ d : Fin 15, (kernel13Sign d : ℝ) * (axisTTPlusCoeffZ d : ℝ) := by
 653    simp_rw [kernel13_eq_sign, classCoeff_axisTTPlus_int, Finset.mul_sum]
 654    exact Finset.sum_congr rfl fun d _ => by ring
 655  rw [h, sum_sign_axis, signDotAxis_kernel13]
 656  norm_num
 657
 658theorem deficitKernel11_dot_decoyGauge :
 659    classDot ReggeHinge4DStarKernel.fullStarClassKernel decoyGauge = 0 := by
 660  unfold classDot coeffDot
 661  simp_rw [kernel11_eq_sign, classCoeff_decoyGauge_bit, sum_sign_gauge,
 662    signDotGauge_kernel11]
 663  norm_num
 664
 665theorem deficitKernel22_dot_decoyGauge :
 666    classDot ReggeHinge4DStarKernel22.fullStarClassKernel decoyGauge = 0 := by
 667  unfold classDot coeffDot
 668  simp_rw [kernel22_eq_sign, classCoeff_decoyGauge_bit, sum_sign_gauge,
 669    signDotGauge_kernel22]
 670  norm_num
 671
 672theorem deficitKernel12_dot_decoyGauge :
 673    classDot ReggeHinge4DStarKernel12.fullStarClassKernel decoyGauge = 0 := by
 674  unfold classDot coeffDot
 675  have h :
 676      (∑ d : Fin 15,
 677          ReggeHinge4DStarKernel12.fullStarClassKernel d *
 678            classCoeff decoyGauge d) =
 679        (Real.sqrt 2 / 2) *
 680          ∑ d : Fin 15,
 681            (kernel12Sign d : ℝ) * ((2 : ℝ) * (gaugeBit0 d : ℝ)) := by
 682    simp_rw [kernel12_eq_sign, classCoeff_decoyGauge_bit, Finset.mul_sum]
 683    exact Finset.sum_congr rfl fun d _ => by ring
 684  rw [h, sum_sign_gauge, signDotGauge_kernel12]
 685  norm_num
 686
 687theorem deficitKernel13_dot_decoyGauge :
 688    classDot ReggeHinge4DStarKernel13.fullStarClassKernel decoyGauge = 0 := by
 689  unfold classDot coeffDot
 690  have h :
 691      (∑ d : Fin 15,
 692          ReggeHinge4DStarKernel13.fullStarClassKernel d *
 693            classCoeff decoyGauge d) =
 694        Real.sqrt 3 *
 695          ∑ d : Fin 15,
 696            (kernel13Sign d : ℝ) * ((2 : ℝ) * (gaugeBit0 d : ℝ)) := by
 697    simp_rw [kernel13_eq_sign, classCoeff_decoyGauge_bit, Finset.mul_sum]
 698    exact Finset.sum_congr rfl fun d _ => by ring
 699  rw [h, sum_sign_gauge, signDotGauge_kernel13]
 700  norm_num
 701
 702theorem deficitKernel11_dot_decoyTrace :
 703    classDot ReggeHinge4DStarKernel.fullStarClassKernel decoyTrace = 0 := by
 704  -- classCoeff decoyTrace = classWeightNat; use committed homothety stationarity
 705  have hv : classCoeff decoyTrace = fun d => (classWeightNat d : ℝ) := by
 706    funext d; rw [classCoeff_decoyTrace, classDispSq_eq_weight]
 707  unfold classDot coeffDot
 708  -- ∑ K * w = ∑ w * K = fullStarDirectional w
 709  have h :
 710      (∑ d : Fin 15,
 711          ReggeHinge4DStarKernel.fullStarClassKernel d *
 712            classCoeff decoyTrace d) =
 713        ReggeHinge4DStarKernel.fullStarDirectional
 714          (fun d => (classWeightNat d : ℝ)) := by
 715    rw [hv]
 716    exact Finset.sum_congr rfl fun d _ => mul_comm _ _
 717  rw [h]
 718  exact ReggeHinge4DStarKernel.fullStar_homothety_stationary
 719
 720theorem deficitKernel12_dot_decoyTrace :
 721    classDot ReggeHinge4DStarKernel12.fullStarClassKernel decoyTrace = 0 := by
 722  have hv : classCoeff decoyTrace = fun d => (classWeightNat d : ℝ) := by
 723    funext d; rw [classCoeff_decoyTrace, classDispSq_eq_weight]
 724  unfold classDot coeffDot
 725  have h :
 726      (∑ d : Fin 15,
 727          ReggeHinge4DStarKernel12.fullStarClassKernel d *
 728            classCoeff decoyTrace d) =
 729        ReggeHinge4DStarKernel12.fullStarDirectional
 730          (fun d => (classWeightNat d : ℝ)) := by
 731    rw [hv]
 732    exact Finset.sum_congr rfl fun d _ => mul_comm _ _
 733  rw [h]
 734  exact ReggeHinge4DStarKernel12.fullStar_homothety_stationary
 735
 736theorem deficitKernel13_dot_decoyTrace :
 737    classDot ReggeHinge4DStarKernel13.fullStarClassKernel decoyTrace = 0 := by
 738  have hv : classCoeff decoyTrace = fun d => (classWeightNat d : ℝ) := by
 739    funext d; rw [classCoeff_decoyTrace, classDispSq_eq_weight]
 740  unfold classDot coeffDot
 741  have h :
 742      (∑ d : Fin 15,
 743          ReggeHinge4DStarKernel13.fullStarClassKernel d *
 744            classCoeff decoyTrace d) =
 745        ReggeHinge4DStarKernel13.fullStarDirectional
 746          (fun d => (classWeightNat d : ℝ)) := by
 747    rw [hv]
 748    exact Finset.sum_congr rfl fun d _ => mul_comm _ _
 749  rw [h]
 750  exact ReggeHinge4DStarKernel13.fullStar_homothety_stationary
 751
 752theorem deficitKernel22_dot_decoyTrace :
 753    classDot ReggeHinge4DStarKernel22.fullStarClassKernel decoyTrace = 0 := by
 754  have hv : classCoeff decoyTrace = fun d => (classWeightNat d : ℝ) := by
 755    funext d; rw [classCoeff_decoyTrace, classDispSq_eq_weight]
 756  unfold classDot coeffDot
 757  have h :
 758      (∑ d : Fin 15,
 759          ReggeHinge4DStarKernel22.fullStarClassKernel d *
 760            classCoeff decoyTrace d) =
 761        ReggeHinge4DStarKernel22.fullStarDirectional
 762          (fun d => (classWeightNat d : ℝ)) := by
 763    rw [hv]
 764    exact Finset.sum_congr rfl fun d _ => mul_comm _ _
 765  rw [h]
 766  exact ReggeHinge4DStarKernel22.fullStar_homothety_stationary
 767
 768theorem deficitKernel11_dot_homothety :
 769    classDot ReggeHinge4DStarKernel.fullStarClassKernel decoyTrace = 0 :=
 770  deficitKernel11_dot_decoyTrace
 771theorem deficitKernel12_dot_homothety :
 772    classDot ReggeHinge4DStarKernel12.fullStarClassKernel decoyTrace = 0 :=
 773  deficitKernel12_dot_decoyTrace
 774theorem deficitKernel13_dot_homothety :
 775    classDot ReggeHinge4DStarKernel13.fullStarClassKernel decoyTrace = 0 :=
 776  deficitKernel13_dot_decoyTrace
 777theorem deficitKernel22_dot_homothety :
 778    classDot ReggeHinge4DStarKernel22.fullStarClassKernel decoyTrace = 0 :=
 779  deficitKernel22_dot_decoyTrace
 780
 781theorem orbitDeficit_dot_axisTTPlus (ty : HingeOrbitType) :
 782    classDot (orbitDeficitKernel ty) axisTTPlus = 0 := by
 783  cases ty with
 784  | t11 => exact deficitKernel11_dot_axisTTPlus
 785  | t12 => exact deficitKernel12_dot_axisTTPlus
 786  | t21 => simpa [orbitDeficitKernel, kernel21] using
 787      deficitKernel12_dot_axisTTPlus
 788  | t13 => exact deficitKernel13_dot_axisTTPlus
 789  | t31 => simpa [orbitDeficitKernel, kernel31] using
 790      deficitKernel13_dot_axisTTPlus
 791  | t22 => exact deficitKernel22_dot_axisTTPlus
 792
 793theorem orbitDeficit_dot_decoyGauge (ty : HingeOrbitType) :
 794    classDot (orbitDeficitKernel ty) decoyGauge = 0 := by
 795  cases ty with
 796  | t11 => exact deficitKernel11_dot_decoyGauge
 797  | t12 => exact deficitKernel12_dot_decoyGauge
 798  | t21 => simpa [orbitDeficitKernel, kernel21] using
 799      deficitKernel12_dot_decoyGauge
 800  | t13 => exact deficitKernel13_dot_decoyGauge
 801  | t31 => simpa [orbitDeficitKernel, kernel31] using
 802      deficitKernel13_dot_decoyGauge
 803  | t22 => exact deficitKernel22_dot_decoyGauge
 804
 805theorem orbitDeficit_dot_decoyTrace (ty : HingeOrbitType) :
 806    classDot (orbitDeficitKernel ty) decoyTrace = 0 := by
 807  cases ty with
 808  | t11 => exact deficitKernel11_dot_decoyTrace
 809  | t12 => exact deficitKernel12_dot_decoyTrace
 810  | t21 => simpa [orbitDeficitKernel, kernel21] using
 811      deficitKernel12_dot_decoyTrace
 812  | t13 => exact deficitKernel13_dot_decoyTrace
 813  | t31 => simpa [orbitDeficitKernel, kernel31] using
 814      deficitKernel13_dot_decoyTrace
 815  | t22 => exact deficitKernel22_dot_decoyTrace
 816
 817/-! ## §7. Named evaluations -/
 818
 819private lemma orbitQuadratic_of_deficit_zero (ty : HingeOrbitType) (H : Mat4)
 820    (h : classDot (orbitDeficitKernel ty) H = 0) :
 821    orbitZeroMomQuadratic ty H = 0 := by
 822  unfold orbitZeroMomQuadratic; rw [h, mul_zero]
 823
 824theorem trueWeightZeroMomQuadratic_axisTTPlus :
 825    trueWeightZeroMomQuadratic axisTTPlus = 0 := by
 826  unfold trueWeightZeroMomQuadratic
 827  exact Finset.sum_eq_zero fun ty _ =>
 828    orbitQuadratic_of_deficit_zero ty _ (orbitDeficit_dot_axisTTPlus ty)
 829
 830theorem trueWeightZeroMomQuadratic_decoyGauge :
 831    trueWeightZeroMomQuadratic decoyGauge = 0 := by
 832  unfold trueWeightZeroMomQuadratic
 833  exact Finset.sum_eq_zero fun ty _ =>
 834    orbitQuadratic_of_deficit_zero ty _ (orbitDeficit_dot_decoyGauge ty)
 835
 836theorem trueWeightZeroMomQuadratic_decoyTrace :
 837    trueWeightZeroMomQuadratic decoyTrace = 0 := by
 838  unfold trueWeightZeroMomQuadratic
 839  exact Finset.sum_eq_zero fun ty _ =>
 840    orbitQuadratic_of_deficit_zero ty _ (orbitDeficit_dot_decoyTrace ty)
 841
 842def homothetyClassCoeff : Mat4 := decoyTrace
 843
 844theorem trueWeightZeroMomQuadratic_homothety :
 845    trueWeightZeroMomQuadratic homothetyClassCoeff = 0 := by
 846  unfold homothetyClassCoeff
 847  exact trueWeightZeroMomQuadratic_decoyTrace
 848
 849theorem trueWeight_kills_gauge_at_zero_momentum :
 850    trueWeightZeroMomQuadratic decoyGauge = 0 ∧
 851      finiteTTQuadratic decoyGauge = 32 :=
 852  ⟨trueWeightZeroMomQuadratic_decoyGauge, finiteTTQuadratic_decoyGauge⟩
 853
 854/-! ## §8. Status -/
 855
 856structure Flat4DHessianAssemblyStatus where
 857  areaGradientsClosed : Bool
 858  complementTransportClosed : Bool
 859  zeroMomentumHessianClosed : Bool
 860  finiteMomentumBlochOpen : Bool
 861  convergesEH4d : Bool
 862  gapActionRecovery : Bool
 863
 864def flat4DHessianAssemblyStatus : Flat4DHessianAssemblyStatus where
 865  areaGradientsClosed := true
 866  complementTransportClosed := true
 867  zeroMomentumHessianClosed := true
 868  finiteMomentumBlochOpen := true
 869  convergesEH4d := false
 870  gapActionRecovery := false
 871
 872theorem flat4DHessianAssemblyStatus_flags :
 873    flat4DHessianAssemblyStatus.areaGradientsClosed = true ∧
 874      flat4DHessianAssemblyStatus.complementTransportClosed = true ∧
 875        flat4DHessianAssemblyStatus.zeroMomentumHessianClosed = true ∧
 876          flat4DHessianAssemblyStatus.finiteMomentumBlochOpen = true ∧
 877            flat4DHessianAssemblyStatus.convergesEH4d = false ∧
 878              flat4DHessianAssemblyStatus.gapActionRecovery = false := by
 879  decide
 880
 881end
 882
 883end ReggeFlat4DHessianAssembly
 884end Analysis
 885end Gravity
 886end IndisputableMonolith
 887