IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   3import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
   4import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
   5import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel
   6import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
   7
   8/-!
   9# Regge 4D finite-momentum Bloch fold ((1,1) orbit)
  10
  11QG full-theory campaign: exact phase-decorated fold of the committed
  12true-weight flat Hessian for type-`(1,1)` triangle hinges in one Kuhn
  13cell, using the midpoint plane-wave convention of `ReggeEdgeStencil4D`.
  14
  15## Tier tags (binding)
  16
  17* THEOREM: every named theorem below (kernel-checked; no `sorry`, no
  18  `admit`, no new axioms, no `native_decide`, no `: True` shells).
  19* Scope: **(1,1) orbit only** (72 oriented slots per cell).
  20* This does **not** evaluate the `m²` Taylor coefficient against the
  21  Einstein–Hilbert / TT continuum symbol (next lane).
  22* This does **not** prove `S_RS_converges_EH_4d`.
  23* This does **not** flip `gap_action_recovery`.
  24
  25## What is proved
  26
  271. **Factorized phased fold** at `m = 0` equals committed
  28   `orbitZeroMomQuadratic .t11` (consistency gate
  29   `factorizedBlochFold11_zeroMomentum`).
  302. **Transported phased fold** `blochFold11` over all 72 slots with
  31   bilinearity and zero-momentum phase drop.
  323. **Structural vanishing:** difference masks `(1,2)` and `(2,1)` give
  33   identically zero `axisTTPlus` contributions for every wave vector
  34   (area supports miss axis-TT class loads).
  354. **Certificate algebra** at `m⋆ = (π/2, π/2, π/2, 0)`: the Nat-kind
  36   axis table sums to `-3` and the gauge table to `-4 + 4√2`.
  375. **Integer Bloch symbol** at `m⋆`: every midpoint phase is a natural
  38   multiple of `π/4` (`classMidpointPhase_waveStar`), so each slot term
  39   equals `(N₁ + N₂·√2)/8` with decidable integers
  40   (`transportedSlotTerm_waveStar_eval`).
  416. **Geometric ↔ certificate match, CLOSED:** on all 240 oriented slots
  42   the integer certificates match the Nat-kind tables (`slotN_axis_match`,
  43   `slotN_gauge_match` by `decide`), hence
  44   `transportedSlotTerm_axis_waveStar` / `transportedSlotTerm_gauge_waveStar`.
  457. **Closing values:** `blochFold11 axisTTPlus waveStar = -3` (nonzero:
  46   nonvacuity) and `blochFold11 decoyGauge waveStar = -4 + 4√2` (nonzero:
  47   discrete gauge invariance at finite momentum holds only up to the
  48   finite-difference identity).
  49
  50Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  51-/
  52
  53namespace IndisputableMonolith
  54namespace Gravity
  55namespace Analysis
  56namespace ReggeBlochFold4D
  57
  58open BigOperators
  59open ReggeEdgeStencil4D
  60open ReggeHinge4DOrbitClassification
  61open ReggeHinge4DFlatKernel
  62open ReggeFlat4DHessianAssembly
  63open EdgeTTDecomposition4D
  64
  65noncomputable section
  66
  67/-! ## §1. Phased class dots -/
  68
  69def maskCoord (mask : ℕ) : Fin 4 → ℝ :=
  70  fun i => if Nat.testBit mask i.val then (1 : ℝ) else 0
  71
  72def hingeBase (s : Fin 24) (t : Fin 10) : Fin 4 → ℝ :=
  73  maskCoord (triangleVertexMasks s t).1
  74
  75def phasedClassDot (v : Fin 15 → ℝ) (H : Mat4) (m x : Fin 4 → ℝ) : ℝ :=
  76  ∑ d : Fin 15, v d * planeWaveClassPert H m x d
  77
  78theorem phasedClassDot_add (v : Fin 15 → ℝ) (A B : Mat4)
  79    (m x : Fin 4 → ℝ) :
  80    phasedClassDot v (A + B) m x =
  81      phasedClassDot v A m x + phasedClassDot v B m x := by
  82  unfold phasedClassDot
  83  simp_rw [planeWaveClassPert_add, mul_add, Finset.sum_add_distrib]
  84
  85theorem phasedClassDot_smul (v : Fin 15 → ℝ) (c : ℝ) (A : Mat4)
  86    (m x : Fin 4 → ℝ) :
  87    phasedClassDot v (c • A) m x = c * phasedClassDot v A m x := by
  88  unfold phasedClassDot
  89  simp_rw [planeWaveClassPert_smul]
  90  refine Eq.trans ?_ (Finset.mul_sum _ _ c).symm
  91  exact Finset.sum_congr rfl fun d _ => by ring
  92
  93theorem phasedClassDot_zeroMomentum (v : Fin 15 → ℝ) (H : Mat4)
  94    (x : Fin 4 → ℝ) :
  95    phasedClassDot v H (fun _ => (0 : ℝ)) x = classDot v H := by
  96  unfold phasedClassDot classDot coeffDot planeWaveClassPert classMidpointPhase
  97  refine Finset.sum_congr rfl fun d _ => ?_
  98  simp [Real.cos_zero]
  99
 100/-! ## §2. Factorized fold and consistency gate -/
 101
 102def isT11 (s : Fin 24) (t : Fin 10) : Prop :=
 103  hingeOrbitType s t = .t11
 104
 105instance (s : Fin 24) (t : Fin 10) : Decidable (isT11 s t) :=
 106  inferInstanceAs (Decidable (hingeOrbitType s t = .t11))
 107
 108theorem isT11_iff_pop (s : Fin 24) (t : Fin 10) :
 109    isT11 s t ↔ hingeTypePop s t = (1, 1) := by
 110  constructor
 111  · intro h
 112    have hpop := hingeOrbitType_toPop s t
 113    simp only [isT11] at h
 114    rw [h, HingeOrbitType.toPop] at hpop
 115    exact hpop.symm
 116  · intro h
 117    simp [isT11, hingeOrbitType, h, popToOrbitType, Option.getD]
 118
 119def factorizedSlotTerm (H : Mat4) (m : Fin 4 → ℝ)
 120    (s : Fin 24) (t : Fin 10) : ℝ :=
 121  if isT11 s t then
 122    phasedClassDot areaCov11 H m (hingeBase s t) *
 123      phasedClassDot ReggeHinge4DStarKernel.fullStarClassKernel H m
 124        (hingeBase s t)
 125  else 0
 126
 127def factorizedBlochFold11 (H : Mat4) (m : Fin 4 → ℝ) : ℝ :=
 128  ∑ s : Fin 24, ∑ t : Fin 10, factorizedSlotTerm H m s t
 129
 130private lemma t11_count_nat :
 131    (∑ s : Fin 24, ∑ t : Fin 10, (if isT11 s t then (1 : ℕ) else 0)) =
 132      72 := by
 133  have h : (∑ s : Fin 24, ∑ t : Fin 10,
 134      (if hingeTypePop s t = (1, 1) then (1 : ℕ) else 0)) = 72 := by
 135    simpa [cellTriangleCount, triangleTypeNat] using cellTriangleCount_t11
 136  refine Eq.trans ?_ h
 137  refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ => ?_
 138  by_cases h' : isT11 s t
 139  · have hp : hingeTypePop s t = (1, 1) := (isT11_iff_pop s t).mp h'
 140    simp [h', hp]
 141  · have : hingeTypePop s t ≠ (1, 1) := fun happ =>
 142      h' ((isT11_iff_pop s t).mpr happ)
 143    simp [h', this]
 144
 145private lemma t11_count_real :
 146    (∑ s : Fin 24, ∑ t : Fin 10, (if isT11 s t then (1 : ℝ) else 0)) =
 147      (72 : ℝ) := by
 148  have := congrArg (fun n : ℕ => (n : ℝ)) t11_count_nat
 149  refine Eq.trans ?_ this
 150  simp_rw [Nat.cast_sum]
 151  refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ => ?_
 152  by_cases h : isT11 s t <;> simp [h]
 153
 154/-- Consistency gate: factorized fold at zero momentum recovers the
 155committed `(1,1)` orbit quadratic. -/
 156theorem factorizedBlochFold11_zeroMomentum (H : Mat4) :
 157    factorizedBlochFold11 H (fun _ => (0 : ℝ)) =
 158      orbitZeroMomQuadratic .t11 H := by
 159  unfold factorizedBlochFold11 orbitZeroMomQuadratic orbitCellCount
 160    orbitAreaCov orbitDeficitKernel
 161  have hterm : ∀ s t,
 162      factorizedSlotTerm H (fun _ => (0 : ℝ)) s t =
 163        (if isT11 s t then (1 : ℝ) else 0) *
 164          (classDot areaCov11 H *
 165            classDot ReggeHinge4DStarKernel.fullStarClassKernel H) := by
 166    intro s t
 167    unfold factorizedSlotTerm
 168    by_cases h : isT11 s t <;> simp [h, phasedClassDot_zeroMomentum]
 169  simp_rw [hterm]
 170  -- Pull the constant product out of the double sum.
 171  rw [show
 172      (∑ s : Fin 24, ∑ t : Fin 10,
 173          (if isT11 s t then (1 : ℝ) else 0) *
 174            (classDot areaCov11 H *
 175              classDot ReggeHinge4DStarKernel.fullStarClassKernel H)) =
 176        (∑ s : Fin 24, ∑ t : Fin 10, (if isT11 s t then (1 : ℝ) else 0)) *
 177          (classDot areaCov11 H *
 178            classDot ReggeHinge4DStarKernel.fullStarClassKernel H) by
 179    simp_rw [Finset.sum_mul]]
 180  rw [t11_count_real]
 181  ring
 182
 183/-! ## §3. Transported fold -/
 184
 185def transportPermOfDiff (a b : ℕ) : Fin 24 :=
 186  match a, b with
 187  | 1, 2 => 0
 188  | 1, 4 => 2
 189  | 1, 8 => 4
 190  | 2, 1 => 6
 191  | 2, 4 => 8
 192  | 2, 8 => 10
 193  | 4, 1 => 12
 194  | 4, 2 => 14
 195  | 4, 8 => 16
 196  | 8, 1 => 18
 197  | 8, 2 => 20
 198  | 8, 4 => 22
 199  | _, _ => 0
 200
 201def permClass (p : Fin 24) (d : Fin 15) : Fin 15 :=
 202  ⟨permMask (coordPermOf p) (maskOf d) - 1, by
 203    have : 0 < permMask (coordPermOf p) (maskOf d) ∧
 204        permMask (coordPermOf p) (maskOf d) ≤ 15 := by
 205      fin_cases p <;> fin_cases d <;> decide
 206    omega⟩
 207
 208def transportedDeficit (p : Fin 24) : Fin 15 → ℝ :=
 209  fun d =>
 210    ∑ d0 : Fin 15,
 211      if permClass p d0 = d then
 212        ReggeHinge4DStarKernel.fullStarClassKernel d0 else 0
 213
 214def slotTransportPerm (s : Fin 24) (t : Fin 10) : Fin 24 :=
 215  transportPermOfDiff (diffMaskA s t) (diffMaskB s t)
 216
 217def slotAreaCov (s : Fin 24) (t : Fin 10) : Fin 15 → ℝ :=
 218  fun d =>
 219    if maskOf d = diffMaskA s t then (1 / 4 : ℝ)
 220    else if maskOf d = diffMaskB s t then (1 / 4 : ℝ)
 221    else 0
 222
 223def slotDeficitKer (s : Fin 24) (t : Fin 10) : Fin 15 → ℝ :=
 224  transportedDeficit (slotTransportPerm s t)
 225
 226def transportedSlotTerm (H : Mat4) (m : Fin 4 → ℝ)
 227    (s : Fin 24) (t : Fin 10) : ℝ :=
 228  if isT11 s t then
 229    phasedClassDot (slotAreaCov s t) H m (hingeBase s t) *
 230      phasedClassDot (slotDeficitKer s t) H m (hingeBase s t)
 231  else 0
 232
 233/-- Honest transported finite-momentum `(1,1)` Bloch fold (72 instances). -/
 234def blochFold11 (H : Mat4) (m : Fin 4 → ℝ) : ℝ :=
 235  ∑ s : Fin 24, ∑ t : Fin 10, transportedSlotTerm H m s t
 236
 237def blochFold11Bilinear (A B : Mat4) (m : Fin 4 → ℝ) : ℝ :=
 238  (1 / 2 : ℝ) *
 239    (∑ s : Fin 24, ∑ t : Fin 10,
 240      if isT11 s t then
 241        phasedClassDot (slotAreaCov s t) A m (hingeBase s t) *
 242            phasedClassDot (slotDeficitKer s t) B m (hingeBase s t) +
 243          phasedClassDot (slotAreaCov s t) B m (hingeBase s t) *
 244            phasedClassDot (slotDeficitKer s t) A m (hingeBase s t)
 245      else (0 : ℝ))
 246
 247theorem blochFold11_eq_bilinear (H : Mat4) (m : Fin 4 → ℝ) :
 248    blochFold11 H m = blochFold11Bilinear H H m := by
 249  unfold blochFold11 blochFold11Bilinear transportedSlotTerm
 250  have h : ∀ s t,
 251      (if isT11 s t then
 252        phasedClassDot (slotAreaCov s t) H m (hingeBase s t) *
 253          phasedClassDot (slotDeficitKer s t) H m (hingeBase s t)
 254       else (0 : ℝ)) =
 255        (1 / 2 : ℝ) *
 256          (if isT11 s t then
 257            phasedClassDot (slotAreaCov s t) H m (hingeBase s t) *
 258                phasedClassDot (slotDeficitKer s t) H m (hingeBase s t) +
 259              phasedClassDot (slotAreaCov s t) H m (hingeBase s t) *
 260                phasedClassDot (slotDeficitKer s t) H m (hingeBase s t)
 261           else 0) := by
 262    intro s t
 263    by_cases ht : isT11 s t
 264    · simp only [ht, ite_true]; ring
 265    · simp only [ht, ite_false]; ring
 266  simp_rw [h]
 267  -- ∑∑ (1/2) * f = (1/2) * ∑∑ f
 268  simp_rw [← Finset.mul_sum]
 269
 270theorem blochFold11Bilinear_symm (A B : Mat4) (m : Fin 4 → ℝ) :
 271    blochFold11Bilinear A B m = blochFold11Bilinear B A m := by
 272  unfold blochFold11Bilinear
 273  refine congr_arg (fun z : ℝ => (1 / 2 : ℝ) * z) ?_
 274  refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ => ?_
 275  by_cases h : isT11 s t
 276  · simp only [h, ite_true]; ring
 277  · simp only [h, ite_false]
 278
 279theorem blochFold11Bilinear_add_left (A₁ A₂ B : Mat4) (m : Fin 4 → ℝ) :
 280    blochFold11Bilinear (A₁ + A₂) B m =
 281      blochFold11Bilinear A₁ B m + blochFold11Bilinear A₂ B m := by
 282  unfold blochFold11Bilinear
 283  simp_rw [phasedClassDot_add]
 284  rw [← mul_add, ← Finset.sum_add_distrib]
 285  congr 1
 286  refine Finset.sum_congr rfl fun s _ => ?_
 287  rw [← Finset.sum_add_distrib]
 288  refine Finset.sum_congr rfl fun t _ => ?_
 289  by_cases h : isT11 s t
 290  · simp [h]; ring
 291  · simp [h]
 292
 293theorem blochFold11Bilinear_smul_left (c : ℝ) (A B : Mat4)
 294    (m : Fin 4 → ℝ) :
 295    blochFold11Bilinear (c • A) B m = c * blochFold11Bilinear A B m := by
 296  unfold blochFold11Bilinear
 297  simp_rw [phasedClassDot_smul]
 298  have h : ∀ s t,
 299      (if isT11 s t then
 300        c * phasedClassDot (slotAreaCov s t) A m (hingeBase s t) *
 301            phasedClassDot (slotDeficitKer s t) B m (hingeBase s t) +
 302          phasedClassDot (slotAreaCov s t) B m (hingeBase s t) *
 303            (c * phasedClassDot (slotDeficitKer s t) A m (hingeBase s t))
 304      else (0 : ℝ)) =
 305        c *
 306          (if isT11 s t then
 307            phasedClassDot (slotAreaCov s t) A m (hingeBase s t) *
 308                phasedClassDot (slotDeficitKer s t) B m (hingeBase s t) +
 309              phasedClassDot (slotAreaCov s t) B m (hingeBase s t) *
 310                phasedClassDot (slotDeficitKer s t) A m (hingeBase s t)
 311          else 0) := by
 312    intro s t
 313    by_cases h : isT11 s t
 314    · simp [h]; ring
 315    · simp [h]
 316  simp_rw [h, ← Finset.mul_sum]
 317  ring
 318
 319theorem transportedSlotTerm_zeroMomentum (H : Mat4)
 320    (s : Fin 24) (t : Fin 10) :
 321    transportedSlotTerm H (fun _ => (0 : ℝ)) s t =
 322      if isT11 s t then
 323        classDot (slotAreaCov s t) H * classDot (slotDeficitKer s t) H
 324      else 0 := by
 325  unfold transportedSlotTerm
 326  by_cases h : isT11 s t <;> simp [h, phasedClassDot_zeroMomentum]
 327
 328/-! ## §4. Structural vanishing on seed-mask orientations -/
 329
 330theorem classCoeff_axisTTPlus_mask_1 :
 331    classCoeff axisTTPlus (0 : Fin 15) = 0 := by
 332  have h2 : Nat.testBit 1 2 = false := by decide
 333  have h3 : Nat.testBit 1 3 = false := by decide
 334  simp [classCoeff_axisTTPlus, classBit, maskOf, h2, h3]
 335
 336theorem classCoeff_axisTTPlus_mask_2 :
 337    classCoeff axisTTPlus (1 : Fin 15) = 0 := by
 338  have h2 : Nat.testBit 2 2 = false := by decide
 339  have h3 : Nat.testBit 2 3 = false := by decide
 340  simp [classCoeff_axisTTPlus, classBit, maskOf, h2, h3]
 341
 342theorem classCoeff_axisTTPlus_mask_3 :
 343    classCoeff axisTTPlus (2 : Fin 15) = 0 := by
 344  have h2 : Nat.testBit 3 2 = false := by decide
 345  have h3 : Nat.testBit 3 3 = false := by decide
 346  simp [classCoeff_axisTTPlus, classBit, maskOf, h2, h3]
 347
 348theorem slotAreaCov_support (s : Fin 24) (t : Fin 10) (d : Fin 15)
 349    (h : slotAreaCov s t d ≠ 0) :
 350    maskOf d = diffMaskA s t ∨ maskOf d = diffMaskB s t := by
 351  unfold slotAreaCov at h
 352  split_ifs at h with hA hB
 353  · exact Or.inl hA
 354  · exact Or.inr hB
 355  · exact (h rfl).elim
 356
 357theorem phasedClassDot_area_axis_of_masks_1_2
 358    (s : Fin 24) (t : Fin 10) (m x : Fin 4 → ℝ)
 359    (ha : diffMaskA s t = 1) (hb : diffMaskB s t = 2) :
 360    phasedClassDot (slotAreaCov s t) axisTTPlus m x = 0 := by
 361  unfold phasedClassDot planeWaveClassPert
 362  refine Finset.sum_eq_zero fun d _ => ?_
 363  by_cases hv : slotAreaCov s t d = 0
 364  · simp [hv]
 365  · have hmask := slotAreaCov_support s t d hv
 366    have hc : classCoeff axisTTPlus d = 0 := by
 367      rcases hmask with h | h
 368      · have h1 : maskOf d = 1 := by simpa [ha] using h
 369        have : d.val = 0 := by
 370          have := congrArg (· - 1) h1
 371          simpa [maskOf] using this
 372        have hd : d = ⟨0, by decide⟩ := Fin.ext this
 373        simpa [hd] using classCoeff_axisTTPlus_mask_1
 374      · have h2 : maskOf d = 2 := by simpa [hb] using h
 375        have : d.val = 1 := by
 376          have := congrArg (· - 1) h2
 377          simpa [maskOf] using this
 378        have hd : d = ⟨1, by decide⟩ := Fin.ext this
 379        simpa [hd] using classCoeff_axisTTPlus_mask_2
 380    simp [hc]
 381
 382theorem phasedClassDot_area_axis_of_masks_2_1
 383    (s : Fin 24) (t : Fin 10) (m x : Fin 4 → ℝ)
 384    (ha : diffMaskA s t = 2) (hb : diffMaskB s t = 1) :
 385    phasedClassDot (slotAreaCov s t) axisTTPlus m x = 0 := by
 386  unfold phasedClassDot planeWaveClassPert
 387  refine Finset.sum_eq_zero fun d _ => ?_
 388  by_cases hv : slotAreaCov s t d = 0
 389  · simp [hv]
 390  · have hmask := slotAreaCov_support s t d hv
 391    have hc : classCoeff axisTTPlus d = 0 := by
 392      rcases hmask with h | h
 393      · have h2 : maskOf d = 2 := by simpa [ha] using h
 394        have : d.val = 1 := by
 395          have := congrArg (· - 1) h2
 396          simpa [maskOf] using this
 397        have hd : d = ⟨1, by decide⟩ := Fin.ext this
 398        simpa [hd] using classCoeff_axisTTPlus_mask_2
 399      · have h1 : maskOf d = 1 := by simpa [hb] using h
 400        have : d.val = 0 := by
 401          have := congrArg (· - 1) h1
 402          simpa [maskOf] using this
 403        have hd : d = ⟨0, by decide⟩ := Fin.ext this
 404        simpa [hd] using classCoeff_axisTTPlus_mask_1
 405    simp [hc]
 406
 407theorem transportedSlotTerm_axis_seedMasks
 408    (s : Fin 24) (t : Fin 10) (m : Fin 4 → ℝ)
 409    (h : (diffMaskA s t = 1 ∧ diffMaskB s t = 2) ∨
 410      (diffMaskA s t = 2 ∧ diffMaskB s t = 1)) :
 411    transportedSlotTerm axisTTPlus m s t = 0 := by
 412  unfold transportedSlotTerm
 413  by_cases ht : isT11 s t
 414  · simp only [ht, ite_true]
 415    rcases h with ⟨ha, hb⟩ | ⟨ha, hb⟩
 416    · rw [phasedClassDot_area_axis_of_masks_1_2 s t m (hingeBase s t) ha hb]
 417      ring
 418    · rw [phasedClassDot_area_axis_of_masks_2_1 s t m (hingeBase s t) ha hb]
 419      ring
 420  · simp [ht]
 421
 422/-! ## §5. Wave vector and certificate algebra -/
 423
 424/-- `m⋆ = (π/2, π/2, π/2, 0)`. -/
 425def waveStar : Fin 4 → ℝ
 426  | 0 => Real.pi / 2
 427  | 1 => Real.pi / 2
 428  | 2 => Real.pi / 2
 429  | 3 => 0
 430
 431def axisStarKind (s : Fin 24) (t : Fin 10) : ℕ :=
 432  if (s.val, t.val) ∈
 433      [(0, 6), (2, 6), (4, 9), (5, 9), (6, 6), (8, 6), (10, 9), (11, 9),
 434        (18, 9), (19, 9), (20, 9), (21, 9)] then 1
 435  else if (s.val, t.val) ∈
 436      [(2, 0), (3, 0), (8, 0), (9, 0), (12, 0), (13, 0), (14, 0), (15, 0),
 437        (19, 6), (21, 6), (22, 6), (23, 6)] then 2
 438  else 0
 439
 440def axisStarContrib (s : Fin 24) (t : Fin 10) : ℝ :=
 441  if axisStarKind s t = 1 then -Real.sqrt 2 / 8
 442  else if axisStarKind s t = 2 then -1 / 4 + Real.sqrt 2 / 8
 443  else 0
 444
 445def gaugeStarKind (s : Fin 24) (t : Fin 10) : ℕ :=
 446  if (s.val, t.val) ∈ [(7, 6), (10, 6), (13, 6), (16, 6)] then 1 else 0
 447
 448def gaugeStarContrib (s : Fin 24) (t : Fin 10) : ℝ :=
 449  if gaugeStarKind s t = 1 then -1 + Real.sqrt 2 else 0
 450
 451theorem axisStarKind_count1 :
 452    (∑ s : Fin 24, ∑ t : Fin 10,
 453        if axisStarKind s t = 1 then (1 : ℕ) else 0) = 12 := by
 454  decide
 455
 456theorem axisStarKind_count2 :
 457    (∑ s : Fin 24, ∑ t : Fin 10,
 458        if axisStarKind s t = 2 then (1 : ℕ) else 0) = 12 := by
 459  decide
 460
 461theorem gaugeStarKind_count1 :
 462    (∑ s : Fin 24, ∑ t : Fin 10,
 463        if gaugeStarKind s t = 1 then (1 : ℕ) else 0) = 4 := by
 464  decide
 465
 466/-- Certificate sum for axis TT at `m⋆`: `-3`. -/
 467theorem sum_axisStarContrib :
 468    (∑ s : Fin 24, ∑ t : Fin 10, axisStarContrib s t) = (-3 : ℝ) := by
 469  unfold axisStarContrib
 470  set a : ℝ := -Real.sqrt 2 / 8
 471  set b : ℝ := -1 / 4 + Real.sqrt 2 / 8
 472  have hterm : ∀ s t,
 473      (if axisStarKind s t = 1 then a
 474        else if axisStarKind s t = 2 then b else (0 : ℝ)) =
 475        a * (if axisStarKind s t = 1 then (1 : ℝ) else 0) +
 476          b * (if axisStarKind s t = 2 then (1 : ℝ) else 0) := by
 477    intro s t
 478    have hk : axisStarKind s t ≤ 2 := by
 479      unfold axisStarKind; split_ifs <;> simp
 480    match h : axisStarKind s t with
 481    | 0 => simp
 482    | 1 => simp
 483    | 2 => simp
 484    | n + 3 => omega
 485  simp_rw [hterm, Finset.sum_add_distrib, ← Finset.mul_sum]
 486  have hc1 :
 487      (∑ s : Fin 24, ∑ t : Fin 10,
 488          if axisStarKind s t = 1 then (1 : ℝ) else 0) = 12 := by
 489    simpa [Nat.cast_sum] using
 490      congrArg (fun n : ℕ => (n : ℝ)) axisStarKind_count1
 491  have hc2 :
 492      (∑ s : Fin 24, ∑ t : Fin 10,
 493          if axisStarKind s t = 2 then (1 : ℝ) else 0) = 12 := by
 494    simpa [Nat.cast_sum] using
 495      congrArg (fun n : ℕ => (n : ℝ)) axisStarKind_count2
 496  rw [hc1, hc2]
 497  -- a*12 + b*12 = -3
 498  unfold a b
 499  ring
 500
 501/-- Certificate sum for decoy gauge at `m⋆`: `-4 + 4√2`. -/
 502theorem sum_gaugeStarContrib :
 503    (∑ s : Fin 24, ∑ t : Fin 10, gaugeStarContrib s t) =
 504      -4 + 4 * Real.sqrt 2 := by
 505  unfold gaugeStarContrib
 506  set c : ℝ := -1 + Real.sqrt 2
 507  have hterm : ∀ s t,
 508      (if gaugeStarKind s t = 1 then c else (0 : ℝ)) =
 509        c * (if gaugeStarKind s t = 1 then (1 : ℝ) else 0) := by
 510    intro s t; by_cases h : gaugeStarKind s t = 1 <;> simp [h]
 511  simp_rw [hterm, ← Finset.mul_sum]
 512  have hc :
 513      (∑ s : Fin 24, ∑ t : Fin 10,
 514          if gaugeStarKind s t = 1 then (1 : ℝ) else 0) = 4 := by
 515    simpa [Nat.cast_sum] using
 516      congrArg (fun n : ℕ => (n : ℝ)) gaugeStarKind_count1
 517  rw [hc]
 518  unfold c
 519  ring
 520
 521/-! ## §6. Integer Bloch symbol at `waveStar`
 522
 523Every midpoint phase at `waveStar` is a natural multiple of `π/4`, so
 524each phased class dot is `a + b·(√2/2)` with decidable integers `a, b`.
 525This turns the geometric slot terms into integer certificates.
 526-/
 527
 528/-- Base-vertex quarter-turn half-count (bits 0,1,2 of the base mask). -/
 529def baseTurns (s : Fin 24) (t : Fin 10) : ℕ :=
 530  (if Nat.testBit (triangleVertexMasks s t).1 0 then 1 else 0) +
 531    (if Nat.testBit (triangleVertexMasks s t).1 1 then 1 else 0) +
 532      (if Nat.testBit (triangleVertexMasks s t).1 2 then 1 else 0)
 533
 534/-- Midpoint quarter-turn count of class `d` (bits 0,1,2 of its mask). -/
 535def dispTurns (d : Fin 15) : ℕ :=
 536  (if classBit d 0 then 1 else 0) +
 537    (if classBit d 1 then 1 else 0) +
 538      (if classBit d 2 then 1 else 0)
 539
 540/-- Total quarter turns of the midpoint phase at `waveStar`. -/
 541def quarterTurns (s : Fin 24) (t : Fin 10) (d : Fin 15) : ℕ :=
 542  2 * baseTurns s t + dispTurns d
 543
 544/-- Integer part of `cos(k·π/4)` (period-8 table). -/
 545def cosC1 : ℕ → ℤ
 546  | 0 => 1
 547  | 4 => -1
 548  | _ => 0
 549
 550/-- `√2/2`-coefficient of `cos(k·π/4)` (period-8 table). -/
 551def cosC2 : ℕ → ℤ
 552  | 1 => 1
 553  | 3 => -1
 554  | 5 => -1
 555  | 7 => 1
 556  | _ => 0
 557
 558private lemma waveStar_dot_maskCoord (M : ℕ) :
 559    (∑ i : Fin 4, waveStar i * maskCoord M i) =
 560      (((if Nat.testBit M 0 then 1 else 0) +
 561          (if Nat.testBit M 1 then 1 else 0) +
 562            (if Nat.testBit M 2 then 1 else 0) : ℕ) : ℝ) *
 563        (Real.pi / 2) := by
 564  rw [Fin.sum_univ_four]
 565  by_cases h0 : Nat.testBit M 0 <;> by_cases h1 : Nat.testBit M 1 <;>
 566    by_cases h2 : Nat.testBit M 2 <;> by_cases h3 : Nat.testBit M 3 <;>
 567    simp [waveStar, maskCoord, h0, h1, h2, h3] <;> ring
 568
 569private lemma waveStar_dot_classDisp (d : Fin 15) :
 570    (∑ i : Fin 4, waveStar i * classDisp d i) =
 571      ((dispTurns d : ℕ) : ℝ) * (Real.pi / 2) := by
 572  rw [Fin.sum_univ_four]
 573  unfold dispTurns
 574  by_cases h0 : classBit d 0 <;> by_cases h1 : classBit d 1 <;>
 575    by_cases h2 : classBit d 2 <;> by_cases h3 : classBit d 3 <;>
 576    simp [waveStar, classDisp, h0, h1, h2, h3] <;> ring
 577
 578/-- The midpoint phase at `waveStar` is `quarterTurns · π/4` exactly. -/
 579theorem classMidpointPhase_waveStar (s : Fin 24) (t : Fin 10) (d : Fin 15) :
 580    classMidpointPhase waveStar (hingeBase s t) d =
 581      (quarterTurns s t d : ℝ) * (Real.pi / 4) := by
 582  unfold classMidpointPhase hingeBase quarterTurns baseTurns
 583  rw [waveStar_dot_maskCoord, waveStar_dot_classDisp]
 584  push_cast
 585  ring
 586
 587/-- Exact table for `cos(k·π/4)`, valid for every natural `k`. -/
 588theorem cos_quarterTurns (k : ℕ) :
 589    Real.cos ((k : ℝ) * (Real.pi / 4)) =
 590      (cosC1 (k % 8) : ℝ) + (cosC2 (k % 8) : ℝ) * (Real.sqrt 2 / 2) := by
 591  have hmod : ((k % 8 : ℕ) : ℝ) + 8 * ((k / 8 : ℕ) : ℝ) = (k : ℝ) := by
 592    exact_mod_cast congrArg (fun n : ℕ => (n : ℝ)) (Nat.mod_add_div k 8)
 593  have hsplit : (k : ℝ) * (Real.pi / 4) =
 594      ((k % 8 : ℕ) : ℝ) * (Real.pi / 4) +
 595        ((k / 8 : ℕ) : ℝ) * (2 * Real.pi) := by
 596    rw [← hmod]; ring
 597  rw [hsplit,
 598    (Real.cos_periodic.nat_mul (k / 8)) (((k % 8 : ℕ) : ℝ) * (Real.pi / 4))]
 599  have h8 : k % 8 = 0 ∨ k % 8 = 1 ∨ k % 8 = 2 ∨ k % 8 = 3 ∨ k % 8 = 4 ∨
 600      k % 8 = 5 ∨ k % 8 = 6 ∨ k % 8 = 7 := by omega
 601  rcases h8 with h | h | h | h | h | h | h | h <;> rw [h]
 602  · norm_num [cosC1, cosC2, Real.cos_zero]
 603  · norm_num [cosC1, cosC2, Real.cos_pi_div_four]
 604  · rw [show ((2 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi / 2 by push_cast; ring]
 605    norm_num [cosC1, cosC2, Real.cos_pi_div_two]
 606  · rw [show ((3 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi - Real.pi / 4 by
 607      push_cast; ring]
 608    rw [Real.cos_pi_sub]
 609    norm_num [cosC1, cosC2, Real.cos_pi_div_four]
 610  · rw [show ((4 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi by push_cast; ring]
 611    norm_num [cosC1, cosC2, Real.cos_pi]
 612  · rw [show ((5 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi + Real.pi / 4 by
 613      push_cast; ring]
 614    rw [Real.cos_add]
 615    norm_num [cosC1, cosC2, Real.cos_pi, Real.sin_pi, Real.cos_pi_div_four]
 616  · rw [show ((6 : ℕ) : ℝ) * (Real.pi / 4) = Real.pi + Real.pi / 2 by
 617      push_cast; ring]
 618    rw [Real.cos_add]
 619    norm_num [cosC1, cosC2, Real.cos_pi, Real.sin_pi, Real.cos_pi_div_two]
 620  · rw [show ((7 : ℕ) : ℝ) * (Real.pi / 4) = 2 * Real.pi - Real.pi / 4 by
 621      push_cast; ring]
 622    rw [Real.cos_sub]
 623    norm_num [cosC1, cosC2, Real.cos_two_pi, Real.sin_two_pi,
 624      Real.cos_pi_div_four]
 625
 626/-- Integer (×4) slot area table. -/
 627def slotAreaCovZ4 (s : Fin 24) (t : Fin 10) (d : Fin 15) : ℤ :=
 628  if maskOf d = diffMaskA s t then 1
 629  else if maskOf d = diffMaskB s t then 1
 630  else 0
 631
 632private lemma slotAreaCov_eq_cast (s : Fin 24) (t : Fin 10) (d : Fin 15) :
 633    slotAreaCov s t d = ((slotAreaCovZ4 s t d : ℤ) : ℝ) / 4 := by
 634  unfold slotAreaCov slotAreaCovZ4
 635  split_ifs <;> norm_num
 636
 637/-- Integer symbol of the phased area dot (×4, integer part). -/
 638def slotA1 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 639  ∑ d : Fin 15,
 640    slotAreaCovZ4 s t d * cz d * cosC1 (quarterTurns s t d % 8)
 641
 642/-- Integer symbol of the phased area dot (×4, `√2/2` part). -/
 643def slotA2 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 644  ∑ d : Fin 15,
 645    slotAreaCovZ4 s t d * cz d * cosC2 (quarterTurns s t d % 8)
 646
 647/-- Integer symbol of the phased transported-kernel dot (integer part). -/
 648def slotK1 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 649  ∑ d0 : Fin 15,
 650    kernel11Sign d0 * cz (permClass (slotTransportPerm s t) d0) *
 651      cosC1 (quarterTurns s t (permClass (slotTransportPerm s t) d0) % 8)
 652
 653/-- Integer symbol of the phased transported-kernel dot (`√2/2` part). -/
 654def slotK2 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 655  ∑ d0 : Fin 15,
 656    kernel11Sign d0 * cz (permClass (slotTransportPerm s t) d0) *
 657      cosC2 (quarterTurns s t (permClass (slotTransportPerm s t) d0) % 8)
 658
 659/-- Integer certificate of a slot term (×8, integer part). -/
 660def slotN1 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 661  if isT11 s t then
 662    2 * slotA1 cz s t * slotK1 cz s t + slotA2 cz s t * slotK2 cz s t
 663  else 0
 664
 665/-- Integer certificate of a slot term (×8, `√2` part). -/
 666def slotN2 (cz : Fin 15 → ℤ) (s : Fin 24) (t : Fin 10) : ℤ :=
 667  if isT11 s t then
 668    slotA1 cz s t * slotK2 cz s t + slotA2 cz s t * slotK1 cz s t
 669  else 0
 670
 671/-- Reindexing: a phased dot against the transported kernel is the seed
 672kernel folded through the class permutation. -/
 673theorem phasedClassDot_transportedDeficit (p : Fin 24) (H : Mat4)
 674    (m x : Fin 4 → ℝ) :
 675    phasedClassDot (transportedDeficit p) H m x =
 676      ∑ d0 : Fin 15,
 677        ReggeHinge4DStarKernel.fullStarClassKernel d0 *
 678          planeWaveClassPert H m x (permClass p d0) := by
 679  unfold phasedClassDot transportedDeficit
 680  simp_rw [Finset.sum_mul]
 681  rw [Finset.sum_comm]
 682  refine Finset.sum_congr rfl fun d0 _ => ?_
 683  have h : ∀ d : Fin 15,
 684      (if permClass p d0 = d then
 685        ReggeHinge4DStarKernel.fullStarClassKernel d0 else 0) *
 686          planeWaveClassPert H m x d =
 687        (if permClass p d0 = d then
 688          ReggeHinge4DStarKernel.fullStarClassKernel d0 *
 689            planeWaveClassPert H m x d else 0) := by
 690    intro d; split_ifs <;> simp
 691  simp_rw [h]
 692  rw [Finset.sum_ite_eq]
 693  simp
 694
 695/-- Master area evaluation at `waveStar`. -/
 696theorem phasedA_waveStar (H : Mat4) (cz : Fin 15 → ℤ)
 697    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 698    phasedClassDot (slotAreaCov s t) H waveStar (hingeBase s t) =
 699      ((slotA1 cz s t : ℝ) + (slotA2 cz s t : ℝ) * (Real.sqrt 2 / 2)) / 4 := by
 700  unfold phasedClassDot slotA1 slotA2
 701  rw [Int.cast_sum, Int.cast_sum, Finset.sum_mul, ← Finset.sum_add_distrib,
 702    Finset.sum_div]
 703  refine Finset.sum_congr rfl fun d _ => ?_
 704  unfold planeWaveClassPert
 705  rw [slotAreaCov_eq_cast, hH d, classMidpointPhase_waveStar,
 706    cos_quarterTurns]
 707  push_cast
 708  ring
 709
 710/-- Master transported-kernel evaluation at `waveStar`. -/
 711theorem phasedK_waveStar (H : Mat4) (cz : Fin 15 → ℤ)
 712    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 713    phasedClassDot (slotDeficitKer s t) H waveStar (hingeBase s t) =
 714      (slotK1 cz s t : ℝ) + (slotK2 cz s t : ℝ) * (Real.sqrt 2 / 2) := by
 715  unfold slotDeficitKer
 716  rw [phasedClassDot_transportedDeficit]
 717  unfold slotK1 slotK2
 718  rw [Int.cast_sum, Int.cast_sum, Finset.sum_mul, ← Finset.sum_add_distrib]
 719  refine Finset.sum_congr rfl fun d0 _ => ?_
 720  unfold planeWaveClassPert
 721  rw [kernel11_eq_sign, hH, classMidpointPhase_waveStar, cos_quarterTurns]
 722  push_cast
 723  ring
 724
 725/-- MASTER SLOT EVALUATION: every transported slot term at `waveStar`
 726equals its integer certificate `(N1 + N2·√2)/8`. -/
 727theorem transportedSlotTerm_waveStar_eval (H : Mat4) (cz : Fin 15 → ℤ)
 728    (hH : ∀ d, classCoeff H d = (cz d : ℝ)) (s : Fin 24) (t : Fin 10) :
 729    transportedSlotTerm H waveStar s t =
 730      ((slotN1 cz s t : ℝ) + (slotN2 cz s t : ℝ) * Real.sqrt 2) / 8 := by
 731  unfold transportedSlotTerm slotN1 slotN2
 732  by_cases ht : isT11 s t
 733  · simp only [ht, ite_true]
 734    rw [phasedA_waveStar H cz hH s t, phasedK_waveStar H cz hH s t]
 735    have h2 : Real.sqrt 2 * Real.sqrt 2 = 2 :=
 736      Real.mul_self_sqrt (by norm_num)
 737    push_cast
 738    linear_combination
 739      (((slotA2 cz s t : ℤ) : ℝ) * ((slotK2 cz s t : ℤ) : ℝ) / 16) * h2
 740  · simp [ht]
 741
 742/-! ## §7. Closing the geometric ↔ certificate match at `waveStar` -/
 743
 744/-- Integer certificate of the axis table by kind:
 745kind 1 ↦ `(0,-1)` (value `-√2/8`), kind 2 ↦ `(-2,1)` (value `-1/4+√2/8`). -/
 746def axisCertN1 : ℕ → ℤ
 747  | 2 => -2
 748  | _ => 0
 749
 750def axisCertN2 : ℕ → ℤ
 751  | 1 => -1
 752  | 2 => 1
 753  | _ => 0
 754
 755def gaugeCertN1 : ℕ → ℤ
 756  | 1 => -8
 757  | _ => 0
 758
 759def gaugeCertN2 : ℕ → ℤ
 760  | 1 => 8
 761  | _ => 0
 762
 763set_option maxRecDepth 8000 in
 764/-- DECIDABLE GATE: the integer slot certificates on `axisTTPlus` match
 765the Nat-kind table on every one of the 240 oriented slots. -/
 766theorem slotN_axis_match :
 767    ∀ s : Fin 24, ∀ t : Fin 10,
 768      slotN1 axisTTPlusCoeffZ s t = axisCertN1 (axisStarKind s t) ∧
 769        slotN2 axisTTPlusCoeffZ s t = axisCertN2 (axisStarKind s t) := by
 770  decide
 771
 772/-- Integer coefficient table for the pure-gauge probe. -/
 773def decoyGaugeCoeffZ (d : Fin 15) : ℤ := 2 * (gaugeBit0 d : ℤ)
 774
 775theorem classCoeff_decoyGauge_int (d : Fin 15) :
 776    classCoeff decoyGauge d = (decoyGaugeCoeffZ d : ℝ) := by
 777  rw [classCoeff_decoyGauge_bit]
 778  unfold decoyGaugeCoeffZ
 779  push_cast
 780  ring
 781
 782set_option maxRecDepth 8000 in
 783/-- DECIDABLE GATE: the integer slot certificates on `decoyGauge` match
 784the Nat-kind table on every slot. -/
 785theorem slotN_gauge_match :
 786    ∀ s : Fin 24, ∀ t : Fin 10,
 787      slotN1 decoyGaugeCoeffZ s t = gaugeCertN1 (gaugeStarKind s t) ∧
 788        slotN2 decoyGaugeCoeffZ s t = gaugeCertN2 (gaugeStarKind s t) := by
 789  decide
 790
 791/-- GEOMETRIC ↔ CERTIFICATE MATCH (axis): every transported slot term on
 792`axisTTPlus` at `waveStar` equals its certificate entry. -/
 793theorem transportedSlotTerm_axis_waveStar (s : Fin 24) (t : Fin 10) :
 794    transportedSlotTerm axisTTPlus waveStar s t = axisStarContrib s t := by
 795  rw [transportedSlotTerm_waveStar_eval axisTTPlus axisTTPlusCoeffZ
 796    classCoeff_axisTTPlus_int s t,
 797    (slotN_axis_match s t).1, (slotN_axis_match s t).2]
 798  unfold axisStarContrib
 799  have hk : axisStarKind s t = 0 ∨ axisStarKind s t = 1 ∨
 800      axisStarKind s t = 2 := by
 801    unfold axisStarKind; split_ifs <;> simp
 802  rcases hk with h | h | h <;> rw [h]
 803  all_goals norm_num [axisCertN1, axisCertN2]
 804  all_goals ring
 805
 806/-- GEOMETRIC ↔ CERTIFICATE MATCH (gauge). -/
 807theorem transportedSlotTerm_gauge_waveStar (s : Fin 24) (t : Fin 10) :
 808    transportedSlotTerm decoyGauge waveStar s t = gaugeStarContrib s t := by
 809  rw [transportedSlotTerm_waveStar_eval decoyGauge decoyGaugeCoeffZ
 810    classCoeff_decoyGauge_int s t,
 811    (slotN_gauge_match s t).1, (slotN_gauge_match s t).2]
 812  unfold gaugeStarContrib
 813  have hk : gaugeStarKind s t = 0 ∨ gaugeStarKind s t = 1 := by
 814    unfold gaugeStarKind; split_ifs <;> simp
 815  rcases hk with h | h <;> rw [h]
 816  all_goals norm_num [gaugeCertN1, gaugeCertN2]
 817  all_goals ring
 818
 819/-- CLOSING THEOREM: the honest transported `(1,1)` Bloch fold on the
 820axis TT polarization at `m⋆ = (π/2, π/2, π/2, 0)` equals `-3`. -/
 821theorem blochFold11_axisTTPlus_waveStar :
 822    blochFold11 axisTTPlus waveStar = -3 := by
 823  unfold blochFold11
 824  simp_rw [transportedSlotTerm_axis_waveStar]
 825  exact sum_axisStarContrib
 826
 827/-- Nonvacuity of the finite-momentum fold on axis TT. -/
 828theorem blochFold11_axisTTPlus_waveStar_ne_zero :
 829    blochFold11 axisTTPlus waveStar ≠ 0 := by
 830  rw [blochFold11_axisTTPlus_waveStar]; norm_num
 831
 832/-- CLOSING THEOREM (gauge verdict): the fold on the pure-gauge probe at
 833`m⋆` equals `-4 + 4√2` (nonzero; discrete gauge invariance at finite
 834momentum holds only up to the finite-difference identity). -/
 835theorem blochFold11_decoyGauge_waveStar :
 836    blochFold11 decoyGauge waveStar = -4 + 4 * Real.sqrt 2 := by
 837  unfold blochFold11
 838  simp_rw [transportedSlotTerm_gauge_waveStar]
 839  exact sum_gaugeStarContrib
 840
 841theorem blochFold11_decoyGauge_waveStar_ne_zero :
 842    blochFold11 decoyGauge waveStar ≠ 0 := by
 843  rw [blochFold11_decoyGauge_waveStar]
 844  have hlt : (1 : ℝ) < Real.sqrt 2 := by
 845    have := Real.lt_sqrt (x := 1) (y := 2) (by norm_num)
 846    norm_num at this
 847    exact this
 848  nlinarith
 849
 850/-! ## §8. Status -/
 851
 852structure BlochFold4DStatus where
 853  factorizedZeroMomentumClosed : Bool
 854  transportedBilinearClosed : Bool
 855  seedMaskAxisVanishClosed : Bool
 856  certificateAlgebraClosed : Bool
 857  geometricCertificateMatchClosed : Bool
 858  m2EhComparisonOpen : Bool
 859  convergesEH4d : Bool
 860  gapActionRecovery : Bool
 861
 862def blochFold4DStatus : BlochFold4DStatus where
 863  factorizedZeroMomentumClosed := true
 864  transportedBilinearClosed := true
 865  seedMaskAxisVanishClosed := true
 866  certificateAlgebraClosed := true
 867  geometricCertificateMatchClosed := true
 868  m2EhComparisonOpen := true
 869  convergesEH4d := false
 870  gapActionRecovery := false
 871
 872theorem blochFold4DStatus_flags :
 873    blochFold4DStatus.factorizedZeroMomentumClosed = true ∧
 874      blochFold4DStatus.transportedBilinearClosed = true ∧
 875        blochFold4DStatus.seedMaskAxisVanishClosed = true ∧
 876          blochFold4DStatus.certificateAlgebraClosed = true ∧
 877            blochFold4DStatus.geometricCertificateMatchClosed = true ∧
 878              blochFold4DStatus.m2EhComparisonOpen = true ∧
 879                blochFold4DStatus.convergesEH4d = false ∧
 880                  blochFold4DStatus.gapActionRecovery = false := by
 881  decide
 882
 883end
 884
 885end ReggeBlochFold4D
 886end Analysis
 887end Gravity
 888end IndisputableMonolith
 889