IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   5import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
   6import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
   7import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12
   8import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel13
   9import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22
  10
  11/-!
  12# Regge 4D Bloch symbol: all-orbit factorized fold and m² moment
  13
  14Generic orbit-indexed fold over the six S4 hinge types
  15`(1,1)`, `(1,2)`, `(2,1)`, `(1,3)`, `(3,1)`, `(2,2)` (four orbits under
  16S4+complement), consuming the committed Heron area covectors and deficit
  17kernels from `ReggeFlat4DHessianAssembly`.
  18
  19## Tier tags (binding)
  20
  21* THEOREM: orbit-count identity, zero-momentum reductions, evenness of
  22  the ray fold, complement kernel identities, status/decoy flags.
  23* DEFINITION: finite-momentum all-orbit fold and all-orbit m² moment
  24  polynomial (cosine two-jet formal coefficient).
  25* OPEN (named `Prop`, status `false`): arbitrary-direction cosine
  26  two-jet Tendsto per orbit and for the all-orbit sum.
  27* Scope: factorized (orbit-constant) kernels. Does **not** replace the
  28  transported `(1,1)` fold of `ReggeBlochFold4D`.
  29* Does **not** prove continuum Einstein–Hilbert recovery.
  30* Does **not** flip `gap_action_recovery`.
  31* Decoy: one-orbit symbol ≠ continuum target.
  32
  33Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  34-/
  35
  36namespace IndisputableMonolith
  37namespace Gravity
  38namespace Analysis
  39namespace ReggeBlochAllOrbitSymbol4D
  40
  41open BigOperators Filter Topology
  42open ReggeEdgeStencil4D
  43open ReggeHinge4DOrbitClassification
  44open ReggeBlochFold4D
  45open ReggeFlat4DHessianAssembly
  46open EdgeTTDecomposition4D
  47
  48noncomputable section
  49
  50/-! ## §1. Orbit predicate and proved slot counts -/
  51
  52/-- Slot belongs to lattice orbit type `ty`. -/
  53def isOrbit (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) : Prop :=
  54  hingeOrbitType s t = ty
  55
  56instance (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) :
  57    Decidable (isOrbit ty s t) :=
  58  inferInstanceAs (Decidable (hingeOrbitType s t = ty))
  59
  60theorem isOrbit_iff_pop (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) :
  61    isOrbit ty s t ↔ hingeTypePop s t = ty.toPop := by
  62  constructor
  63  · intro h
  64    have hpop := hingeOrbitType_toPop s t
  65    simp only [isOrbit] at h
  66    rw [h] at hpop
  67    exact hpop.symm
  68  · intro h
  69    simp only [isOrbit, hingeOrbitType]
  70    rw [h]
  71    cases ty <;> rfl
  72
  73theorem isOrbit_t11_iff_isT11 (s : Fin 24) (t : Fin 10) :
  74    isOrbit .t11 s t ↔ isT11 s t := by
  75  simp [isOrbit, isT11]
  76
  77/-- Oriented slot count for each orbit type equals the committed cell count. -/
  78theorem orbit_slot_count_nat (ty : HingeOrbitType) :
  79    (∑ s : Fin 24, ∑ t : Fin 10, (if isOrbit ty s t then (1 : ℕ) else 0)) =
  80      orbitCellCount ty := by
  81  rw [orbitCellCount_eq_classification]
  82  unfold cellTriangleCount triangleTypeNat
  83  refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ => ?_
  84  by_cases h : isOrbit ty s t
  85  · have hp : hingeTypePop s t = ty.toPop := (isOrbit_iff_pop ty s t).mp h
  86    simp [h, hp]
  87  · have : hingeTypePop s t ≠ ty.toPop := fun happ =>
  88      h ((isOrbit_iff_pop ty s t).mpr happ)
  89    simp [h, this]
  90
  91theorem orbit_slot_count_real (ty : HingeOrbitType) :
  92    (∑ s : Fin 24, ∑ t : Fin 10, (if isOrbit ty s t then (1 : ℝ) else 0)) =
  93      (orbitCellCount ty : ℝ) := by
  94  have := congrArg (fun n : ℕ => (n : ℝ)) (orbit_slot_count_nat ty)
  95  refine Eq.trans ?_ this
  96  simp_rw [Nat.cast_sum]
  97  refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ => ?_
  98  by_cases h : isOrbit ty s t <;> simp [h]
  99
 100/-- Complement pairs share deficit kernels (S4+complement four-orbit merge). -/
 101theorem complement_orbit_deficit_kernels :
 102    (∀ d : Fin 15, orbitDeficitKernel .t21 d = orbitDeficitKernel .t12 d) ∧
 103      (∀ d : Fin 15, orbitDeficitKernel .t31 d = orbitDeficitKernel .t13 d) := by
 104  constructor
 105  · intro d; rfl
 106  · intro d; rfl
 107
 108/-- Area covectors are the committed Heron edge gradients on seed supports. -/
 109theorem orbitAreaCov_uses_heron_grads :
 110    (areaCov11 0 = areaGradA 1 1 2 ∧
 111      areaCov11 1 = areaGradB 1 1 2 ∧
 112        areaCov11 2 = areaGradC 1 1 2) ∧
 113      (areaCov12 0 = areaGradA 1 2 3 ∧
 114        areaCov12 5 = areaGradB 1 2 3 ∧
 115          areaCov12 6 = areaGradC 1 2 3) ∧
 116        (areaCov22 2 = areaGradA 2 2 4 ∧
 117          areaCov22 11 = areaGradB 2 2 4 ∧
 118            areaCov22 14 = areaGradC 2 2 4) :=
 119  ⟨areaCov11_eq_grads, areaCov12_eq_grads, areaCov22_eq_grads⟩
 120
 121/-! ## §2. Generic factorized orbit fold -/
 122
 123/-- Factorized slot term: orbit-constant area covector × deficit kernel,
 124phased by the midpoint plane-wave convention. -/
 125def factorizedOrbitSlotTerm (ty : HingeOrbitType) (H : Mat4) (m : Fin 4 → ℝ)
 126    (s : Fin 24) (t : Fin 10) : ℝ :=
 127  if isOrbit ty s t then
 128    phasedClassDot (orbitAreaCov ty) H m (hingeBase s t) *
 129      phasedClassDot (orbitDeficitKernel ty) H m (hingeBase s t)
 130  else 0
 131
 132/-- Finite-momentum factorized Bloch fold for one orbit type. -/
 133def factorizedBlochFoldOrbit (ty : HingeOrbitType) (H : Mat4)
 134    (m : Fin 4 → ℝ) : ℝ :=
 135  ∑ s : Fin 24, ∑ t : Fin 10, factorizedOrbitSlotTerm ty H m s t
 136
 137/-- Full finite-momentum all-orbit factorized fold (sum of six S4 types). -/
 138def factorizedBlochFoldAll (H : Mat4) (m : Fin 4 → ℝ) : ℝ :=
 139  ∑ ty : HingeOrbitType, factorizedBlochFoldOrbit ty H m
 140
 141theorem factorizedBlochFoldOrbit_t11_eq (H : Mat4) (m : Fin 4 → ℝ) :
 142    factorizedBlochFoldOrbit .t11 H m = factorizedBlochFold11 H m := by
 143  unfold factorizedBlochFoldOrbit factorizedBlochFold11
 144    factorizedOrbitSlotTerm factorizedSlotTerm
 145  refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ => ?_
 146  by_cases h : isOrbit .t11 s t
 147  · have ht : isT11 s t := (isOrbit_t11_iff_isT11 s t).mp h
 148    simp [h, ht, orbitAreaCov, orbitDeficitKernel]
 149  · have ht : ¬ isT11 s t := fun ht => h ((isOrbit_t11_iff_isT11 s t).mpr ht)
 150    simp [h, ht]
 151
 152/-- Consistency gate: each orbit fold at zero momentum recovers the
 153committed `orbitZeroMomQuadratic`. -/
 154theorem factorizedBlochFoldOrbit_zeroMomentum (ty : HingeOrbitType)
 155    (H : Mat4) :
 156    factorizedBlochFoldOrbit ty H (fun _ => (0 : ℝ)) =
 157      orbitZeroMomQuadratic ty H := by
 158  unfold factorizedBlochFoldOrbit orbitZeroMomQuadratic
 159  have hterm : ∀ s t,
 160      factorizedOrbitSlotTerm ty H (fun _ => (0 : ℝ)) s t =
 161        (if isOrbit ty s t then (1 : ℝ) else 0) *
 162          (classDot (orbitAreaCov ty) H *
 163            classDot (orbitDeficitKernel ty) H) := by
 164    intro s t
 165    unfold factorizedOrbitSlotTerm
 166    by_cases h : isOrbit ty s t <;> simp [h, phasedClassDot_zeroMomentum]
 167  simp_rw [hterm]
 168  rw [show
 169      (∑ s : Fin 24, ∑ t : Fin 10,
 170          (if isOrbit ty s t then (1 : ℝ) else 0) *
 171            (classDot (orbitAreaCov ty) H *
 172              classDot (orbitDeficitKernel ty) H)) =
 173        (∑ s : Fin 24, ∑ t : Fin 10, (if isOrbit ty s t then (1 : ℝ) else 0)) *
 174          (classDot (orbitAreaCov ty) H *
 175            classDot (orbitDeficitKernel ty) H) by
 176    simp_rw [Finset.sum_mul]]
 177  rw [orbit_slot_count_real]
 178  ring
 179
 180/-- All-orbit fold at zero momentum is the committed true-weight Hessian. -/
 181theorem factorizedBlochFoldAll_zeroMomentum (H : Mat4) :
 182    factorizedBlochFoldAll H (fun _ => (0 : ℝ)) =
 183      trueWeightZeroMomQuadratic H := by
 184  unfold factorizedBlochFoldAll trueWeightZeroMomQuadratic
 185  exact Finset.sum_congr rfl fun ty _ =>
 186    factorizedBlochFoldOrbit_zeroMomentum ty H
 187
 188theorem factorizedBlochFoldAll_axis_zeroMomentum :
 189    factorizedBlochFoldAll axisTTPlus (fun _ => (0 : ℝ)) = 0 := by
 190  rw [factorizedBlochFoldAll_zeroMomentum, trueWeightZeroMomQuadratic_axisTTPlus]
 191
 192theorem factorizedBlochFoldAll_gauge_zeroMomentum :
 193    factorizedBlochFoldAll decoyGauge (fun _ => (0 : ℝ)) = 0 := by
 194  rw [factorizedBlochFoldAll_zeroMomentum, trueWeightZeroMomQuadratic_decoyGauge]
 195
 196/-! ## §3. Ray folds and evenness -/
 197
 198/-- Scale a wave direction: `m = μ · dir`. -/
 199def foldOrbitAlong (ty : HingeOrbitType) (H : Mat4) (dir : Fin 4 → ℝ)
 200    (μ : ℝ) : ℝ :=
 201  factorizedBlochFoldOrbit ty H (fun i => μ * dir i)
 202
 203def foldAllAlong (H : Mat4) (dir : Fin 4 → ℝ) (μ : ℝ) : ℝ :=
 204  factorizedBlochFoldAll H (fun i => μ * dir i)
 205
 206/-- Midpoint phase linear in the ray parameter. -/
 207def phaseScaleDir (dir : Fin 4 → ℝ) (x : Fin 4 → ℝ) (d : Fin 15) : ℝ :=
 208  (∑ i : Fin 4, dir i * x i) +
 209    (∑ i : Fin 4, dir i * classDisp d i) / 2
 210
 211theorem classMidpointPhase_scaleDir (dir : Fin 4 → ℝ) (μ : ℝ)
 212    (x : Fin 4 → ℝ) (d : Fin 15) :
 213    classMidpointPhase (fun i => μ * dir i) x d =
 214      μ * phaseScaleDir dir x d := by
 215  unfold classMidpointPhase phaseScaleDir
 216  have hx :
 217      (∑ i : Fin 4, (μ * dir i) * x i) =
 218        μ * ∑ i : Fin 4, dir i * x i := by
 219    simp [mul_assoc, Finset.mul_sum]
 220  have hd :
 221      (∑ i : Fin 4, (μ * dir i) * classDisp d i) =
 222        μ * ∑ i : Fin 4, dir i * classDisp d i := by
 223    simp [mul_assoc, Finset.mul_sum]
 224  rw [hx, hd]; ring
 225
 226theorem phasedClassDot_scaleDir (v : Fin 15 → ℝ) (H : Mat4)
 227    (dir : Fin 4 → ℝ) (μ : ℝ) (x : Fin 4 → ℝ) :
 228    phasedClassDot v H (fun i => μ * dir i) x =
 229      ∑ d : Fin 15, v d * classCoeff H d * Real.cos (μ * phaseScaleDir dir x d) := by
 230  unfold phasedClassDot planeWaveClassPert
 231  refine Finset.sum_congr rfl fun d _ => ?_
 232  rw [classMidpointPhase_scaleDir]; ring
 233
 234theorem foldOrbitAlong_neg (ty : HingeOrbitType) (H : Mat4)
 235    (dir : Fin 4 → ℝ) (μ : ℝ) :
 236    foldOrbitAlong ty H dir (-μ) = foldOrbitAlong ty H dir μ := by
 237  unfold foldOrbitAlong factorizedBlochFoldOrbit factorizedOrbitSlotTerm
 238  refine Finset.sum_congr rfl fun s _ => Finset.sum_congr rfl fun t _ => ?_
 239  by_cases ht : isOrbit ty s t
 240  · simp only [ht, ite_true]
 241    have hphase (v : Fin 15 → ℝ) :
 242        phasedClassDot v H (fun i => (-μ) * dir i) (hingeBase s t) =
 243          phasedClassDot v H (fun i => μ * dir i) (hingeBase s t) := by
 244      rw [phasedClassDot_scaleDir, phasedClassDot_scaleDir]
 245      refine Finset.sum_congr rfl fun d _ => ?_
 246      rw [neg_mul, Real.cos_neg]
 247    rw [hphase (orbitAreaCov ty), hphase (orbitDeficitKernel ty)]
 248  · simp [ht]
 249
 250theorem foldOrbitAlong_even (ty : HingeOrbitType) (H : Mat4)
 251    (dir : Fin 4 → ℝ) : Function.Even (foldOrbitAlong ty H dir) :=
 252  fun μ => foldOrbitAlong_neg ty H dir μ
 253
 254theorem foldAllAlong_neg (H : Mat4) (dir : Fin 4 → ℝ) (μ : ℝ) :
 255    foldAllAlong H dir (-μ) = foldAllAlong H dir μ := by
 256  unfold foldAllAlong factorizedBlochFoldAll
 257  refine Finset.sum_congr rfl fun ty _ => foldOrbitAlong_neg ty H dir μ
 258
 259theorem foldAllAlong_even (H : Mat4) (dir : Fin 4 → ℝ) :
 260    Function.Even (foldAllAlong H dir) :=
 261  fun μ => foldAllAlong_neg H dir μ
 262
 263private lemma zero_smul_dir (dir : Fin 4 → ℝ) :
 264    (fun i : Fin 4 => (0 : ℝ) * dir i) = fun _ => (0 : ℝ) := by
 265  funext i; ring
 266
 267theorem foldAllAlong_zero (H : Mat4) (dir : Fin 4 → ℝ) :
 268    foldAllAlong H dir 0 = trueWeightZeroMomQuadratic H := by
 269  unfold foldAllAlong
 270  simp_rw [zero_smul_dir]
 271  exact factorizedBlochFoldAll_zeroMomentum H
 272
 273theorem foldAllAlong_axis_zero (dir : Fin 4 → ℝ) :
 274    foldAllAlong axisTTPlus dir 0 = 0 := by
 275  rw [foldAllAlong_zero, trueWeightZeroMomQuadratic_axisTTPlus]
 276
 277theorem foldAllAlong_gauge_zero (dir : Fin 4 → ℝ) :
 278    foldAllAlong decoyGauge dir 0 = 0 := by
 279  rw [foldAllAlong_zero, trueWeightZeroMomQuadratic_decoyGauge]
 280
 281/-! ## §4. All-orbit m² moment polynomial (definition) -/
 282
 283/-- Formal cosine two-jet m² coefficient for one orbit at direction `dir`.
 284This is the algebraic moment polynomial; Tendsto glue is OPEN below. -/
 285def m2OrbitMomentPoly (ty : HingeOrbitType) (H : Mat4)
 286    (dir : Fin 4 → ℝ) : ℝ :=
 287  ∑ s : Fin 24, ∑ t : Fin 10,
 288    if isOrbit ty s t then
 289      classDot (orbitAreaCov ty) H *
 290        (-(1 / 2 : ℝ) *
 291          ∑ d : Fin 15,
 292            orbitDeficitKernel ty d * classCoeff H d *
 293              (phaseScaleDir dir (hingeBase s t) d) ^ 2)
 294    else 0
 295
 296/-- Full all-orbit m² moment polynomial. -/
 297def m2AllOrbitMomentPoly (H : Mat4) (dir : Fin 4 → ℝ) : ℝ :=
 298  ∑ ty : HingeOrbitType, m2OrbitMomentPoly ty H dir
 299
 300/-- At vanishing area·H the moment polynomial is identically zero. -/
 301theorem m2OrbitMomentPoly_of_area_zero (ty : HingeOrbitType) (H : Mat4)
 302    (dir : Fin 4 → ℝ) (hA : classDot (orbitAreaCov ty) H = 0) :
 303    m2OrbitMomentPoly ty H dir = 0 := by
 304  unfold m2OrbitMomentPoly
 305  refine Finset.sum_eq_zero fun s _ => Finset.sum_eq_zero fun t _ => ?_
 306  by_cases ht : isOrbit ty s t <;> simp [ht, hA]
 307
 308/-- Ray fold at μ = 0 recovers the committed zero-momentum orbit quadratic. -/
 309theorem foldOrbitAlong_zero (ty : HingeOrbitType) (H : Mat4)
 310    (dir : Fin 4 → ℝ) :
 311    foldOrbitAlong ty H dir 0 = orbitZeroMomQuadratic ty H := by
 312  unfold foldOrbitAlong
 313  simp_rw [zero_smul_dir]
 314  exact factorizedBlochFoldOrbit_zeroMomentum ty H
 315
 316theorem foldOrbitAlong_axis_zero (ty : HingeOrbitType) (dir : Fin 4 → ℝ) :
 317    foldOrbitAlong ty axisTTPlus dir 0 = 0 := by
 318  rw [foldOrbitAlong_zero]
 319  unfold orbitZeroMomQuadratic
 320  rw [orbitDeficit_dot_axisTTPlus ty, mul_zero]
 321
 322theorem foldOrbitAlong_gauge_zero (ty : HingeOrbitType) (dir : Fin 4 → ℝ) :
 323    foldOrbitAlong ty decoyGauge dir 0 = 0 := by
 324  rw [foldOrbitAlong_zero]
 325  unfold orbitZeroMomQuadratic
 326  rw [orbitDeficit_dot_decoyGauge ty, mul_zero]
 327/-! ## §5. OPEN Props: arbitrary-direction cosine two-jets / Tendsto -/
 328
 329/-- OPEN: punctured Tendsto of one-orbit ray fold / μ² to the moment poly. -/
 330def OrbitFoldAlongM2Tendsto (ty : HingeOrbitType) (H : Mat4)
 331    (dir : Fin 4 → ℝ) : Prop :=
 332  Tendsto (fun μ : ℝ => foldOrbitAlong ty H dir μ / μ ^ 2) (𝓝[≠] (0 : ℝ))
 333    (𝓝 (m2OrbitMomentPoly ty H dir))
 334
 335/-- OPEN: punctured Tendsto of the all-orbit ray fold / μ². -/
 336def AllOrbitFoldAlongM2Tendsto (H : Mat4) (dir : Fin 4 → ℝ) : Prop :=
 337  Tendsto (fun μ : ℝ => foldAllAlong H dir μ / μ ^ 2) (𝓝[≠] (0 : ℝ))
 338    (𝓝 (m2AllOrbitMomentPoly H dir))
 339
 340/-- OPEN: cosine two-jet / Tendsto holds for every nonzero direction. -/
 341def ArbitraryDirectionCosineTwoJet (ty : HingeOrbitType) (H : Mat4) : Prop :=
 342  ∀ dir : Fin 4 → ℝ, dir ≠ 0 → OrbitFoldAlongM2Tendsto ty H dir
 343
 344/-- OPEN: all-orbit arbitrary-direction cosine two-jet. -/
 345def AllOrbitArbitraryDirectionCosineTwoJet (H : Mat4) : Prop :=
 346  ∀ dir : Fin 4 → ℝ, dir ≠ 0 → AllOrbitFoldAlongM2Tendsto H dir
 347
 348/-! ## §6. Status flags and decoys -/
 349
 350structure BlochAllOrbitSymbol4DStatus where
 351  orbitCountsClosed : Bool
 352  zeroMomentumReductionClosed : Bool
 353  rayEvennessClosed : Bool
 354  heronAreaGradientsWired : Bool
 355  complementKernelsClosed : Bool
 356  m2MomentPolyDefined : Bool
 357  /-- Arbitrary-direction Tendsto per orbit: still OPEN. -/
 358  orbitM2TendstoClosed : Bool
 359  /-- All-orbit arbitrary-direction Tendsto: still OPEN. -/
 360  allOrbitM2TendstoClosed : Bool
 361  /-- Continuum EH / full Hessian symbol: not claimed here. -/
 362  continuumEHClosed : Bool
 363  /-- Ledger flag must stay false. -/
 364  gapActionRecovery : Bool
 365  /-- Honesty: one-orbit symbol is not the continuum target. -/
 366  oneOrbitIsNotContinuumTarget : Bool
 367
 368def blochAllOrbitSymbol4DStatus : BlochAllOrbitSymbol4DStatus where
 369  orbitCountsClosed := true
 370  zeroMomentumReductionClosed := true
 371  rayEvennessClosed := true
 372  heronAreaGradientsWired := true
 373  complementKernelsClosed := true
 374  m2MomentPolyDefined := true
 375  orbitM2TendstoClosed := false
 376  allOrbitM2TendstoClosed := false
 377  continuumEHClosed := false
 378  gapActionRecovery := false
 379  oneOrbitIsNotContinuumTarget := true
 380
 381theorem blochAllOrbitSymbol4DStatus_flags :
 382    blochAllOrbitSymbol4DStatus.orbitCountsClosed = true ∧
 383      blochAllOrbitSymbol4DStatus.zeroMomentumReductionClosed = true ∧
 384        blochAllOrbitSymbol4DStatus.rayEvennessClosed = true ∧
 385          blochAllOrbitSymbol4DStatus.heronAreaGradientsWired = true ∧
 386            blochAllOrbitSymbol4DStatus.complementKernelsClosed = true ∧
 387              blochAllOrbitSymbol4DStatus.m2MomentPolyDefined = true ∧
 388                blochAllOrbitSymbol4DStatus.orbitM2TendstoClosed = false ∧
 389                  blochAllOrbitSymbol4DStatus.allOrbitM2TendstoClosed = false ∧
 390                    blochAllOrbitSymbol4DStatus.continuumEHClosed = false ∧
 391                      blochAllOrbitSymbol4DStatus.gapActionRecovery = false ∧
 392                        blochAllOrbitSymbol4DStatus.oneOrbitIsNotContinuumTarget =
 393                          true := by
 394  decide
 395
 396/-- DECOY: the closed one-orbit `(1,1)` m² coefficient `-3` is not the
 397continuum EH target; continuum recovery requires the full all-orbit symbol. -/
 398theorem decoy_one_orbit_m2_is_not_continuum_target :
 399    ReggeBlochM2Symbol4D.m2Symbol axisTTPlus = -3 ∧
 400      blochAllOrbitSymbol4DStatus.continuumEHClosed = false ∧
 401        blochAllOrbitSymbol4DStatus.oneOrbitIsNotContinuumTarget = true ∧
 402          blochAllOrbitSymbol4DStatus.gapActionRecovery = false := by
 403  refine ⟨ReggeBlochM2Symbol4D.m2Symbol_axisTTPlus, rfl, rfl, rfl⟩
 404
 405/-- Named OPEN props remain uninhabited status markers (not theorems). -/
 406theorem open_props_are_status_false :
 407    blochAllOrbitSymbol4DStatus.orbitM2TendstoClosed = false ∧
 408      blochAllOrbitSymbol4DStatus.allOrbitM2TendstoClosed = false := by
 409  decide
 410
 411end
 412
 413end ReggeBlochAllOrbitSymbol4D
 414end Analysis
 415end Gravity
 416end IndisputableMonolith
 417