IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
   5import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   6import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
   7import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
   8import IndisputableMonolith.Gravity.Analysis.Regge4DExactActionSymbol
   9import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
  10import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4D
  11import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4D
  12
  13/-!
  14# Regge 4D continuum preflight: frozen weak-field EH target and decoys
  15
  16QG full-theory campaign, first binding increment of the 4D continuum
  17closure plan.  This module freezes the independent continuum target,
  18canonical mesh carrier, normalized TT data, pure-gauge family, and
  19honesty decoys **before** further computation.  Nothing here proves
  20continuum recovery.
  21
  22## Tier tags (binding)
  23
  24* THEOREM: Frobenius pin lemmas, decoy discriminators, symbol uniqueness,
  25  status flags, and banked algebraic face identities
  26  (`discreteBookkeeping_recovers_frozen_EH`).
  27* MODEL / DEFINITION: the independently frozen Einstein-Hilbert quadratic
  28  functional and the mesh / symbol objects named below.
  29* OPEN: continuum Tendsto value Props (`Regge4DContinuumEHTarget`,
  30  gauge-zero); `S_RS_converges_EH_4d` uninhabited; `gapActionRecovery`
  31  false. ContinuumSymbolIs is the geometric mesh sequence, not a constant
  32  face.
  33* Banked non-ledger: discrete bookkeeping `2·(-1/8)=-1/4` and algebraic
  34  gauge face `0` (do not inhabit the geometric Tendsto Props).
  35* This does **not** reverse-engineer lattice weights from the EH answer:
  36  the EH quadratic is frozen independently of the lattice symbol; the
  37  later algebraic closer must *observe* equality, never fit a scale.
  38
  39## Frozen contracts
  40
  411. Canonical periodic Freudenthal 4-torus mesh of side `N ≥ 3`.
  422. Frobenius-normalized Euclidean TT polarizations (Gate A0 analog).
  433. Independently defined linearized EH quadratic functional using
  44   `kappa_einstein` (not a free lattice normalization).
  454. Named OPEN continuum target (after oracle `H_fold`, 2026-07-21): the
  46   exact flat cross-term symbol `finiteExactReggeSymbol` (from
  47   `Regge4DExactActionSymbol.exactFlatCrossTermFold`), `|k|²`-normalized,
  48   equals the EH coefficient on TT and vanishes on pure gauge.  The
  49   legacy distinct-hinge fold `finiteTransportedSymbol` /
  50   `blochFoldAllDistinctHinge` is retained for comparison only and is
  51   **not** the continuum object (mis-transport on t12/t13 gauge).
  52   Bare `blochFoldAll` and fitted `2/r` remain excluded.
  53   Residual: star-member offsets incomplete for non-`t11`/`t12` orbits;
  54   3D-style continuum dictionary (`2/N⁴` cell-sum) still required for
  55   EH Tendsto; do not install a fitted scale-2.
  565. Decoys: provisional weight-1 aggregate fails gauge; one-orbit symbol
  57   is not the continuum target; wrong mesh power `N⁻²` instead of
  58   `N⁻⁴` is rejected; arbitrary pullbacks are excluded from the action
  59   theorem.
  60
  61Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  62-/
  63
  64namespace IndisputableMonolith
  65namespace Gravity
  66namespace Analysis
  67namespace Regge4DContinuumPreflight
  68
  69open Matrix BigOperators Filter Topology
  70open EdgeTTDecomposition4D
  71open ReggeEdgeStencil4D
  72open Constants
  73open ReggeBlochTransportedAllOrbit4D (blochFoldAllDistinctHinge)
  74open ReggeExactFlatHessianSymbol4D (exactHessianM2UnitFrobeniusTTCoeff)
  75
  76noncomputable section
  77
  78abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
  79abbrev Wave4 := Fin 4 → ℝ
  80
  81/-! ## §1. Canonical periodic Freudenthal 4-torus mesh -/
  82
  83/-- Side length of the periodic lattice; continuum family uses `N = j + 3`. -/
  84def torusSide (j : ℕ) : ℕ := j + 3
  85
  86theorem torusSide_ge_three (j : ℕ) : 3 ≤ torusSide j := by
  87  unfold torusSide; omega
  88
  89/-- Integer wave vector on the side-`N` torus (commensurate modes). -/
  90abbrev IntMode4 := Fin 4 → ℤ
  91
  92/-- Real wave covector from an integer mode on side `N`: `k = 2π m / N`. -/
  93def realMode (N : ℕ) (m : IntMode4) : Wave4 :=
  94  fun i => (2 * Real.pi) * (m i : ℝ) / (N : ℝ)
  95
  96/-- Squared Euclidean norm of a real wave covector. -/
  97def waveNormSq (k : Wave4) : ℝ :=
  98  ∑ i : Fin 4, k i * k i
  99
 100theorem waveNormSq_eq_momentumSq (k : Wave4) :
 101    waveNormSq k = momentumSq k := rfl
 102
 103/-- Momentum normalization on the side-`N` torus for integer mode `m`. -/
 104def momentumNormSq (N : ℕ) (m : IntMode4) : ℝ :=
 105  waveNormSq (realMode N m)
 106
 107theorem momentumNormSq_eq (N : ℕ) (m : IntMode4) :
 108    momentumNormSq N m =
 109      ((2 * Real.pi) / (N : ℝ)) ^ 2 * ∑ i : Fin 4, (m i : ℝ) ^ 2 := by
 110  unfold momentumNormSq waveNormSq realMode
 111  have h :
 112      ∀ i : Fin 4,
 113        ((2 * Real.pi) * (m i : ℝ) / (N : ℝ)) *
 114            ((2 * Real.pi) * (m i : ℝ) / (N : ℝ)) =
 115          ((2 * Real.pi) / (N : ℝ)) ^ 2 * (m i : ℝ) ^ 2 := by
 116    intro i; ring
 117  simp_rw [h, ← Finset.mul_sum]
 118
 119/-- Canonical mesh carrier: side-`N` periodic Freudenthal triangulation of
 120the flat 4-torus.  The concrete Kuhn cell data live in the star/orbit
 121modules; this structure records the continuum-family indices only. -/
 122structure CanonicalFreudenthalTorus4D where
 123  /-- Continuum index; mesh side is `torusSide j`. -/
 124  continuumIndex : ℕ
 125  deriving Repr
 126
 127def CanonicalFreudenthalTorus4D.side (T : CanonicalFreudenthalTorus4D) : ℕ :=
 128  torusSide T.continuumIndex
 129
 130/-! ## §2. Frobenius-normalized TT data (Gate A0 analog) -/
 131
 132/-- Frobenius squared norm of a `4 × 4` matrix. -/
 133def frobeniusNormSq (E : Mat4) : ℝ :=
 134  ∑ i : Fin 4, ∑ j : Fin 4, E i j * E i j
 135
 136/-- Continuum TT polarization: algebraic TT plus Frobenius normalization.
 137Without the pin, a fixed continuum coefficient is ill-posed. -/
 138def IsTTPolarization4D (m : Wave4) (E : Mat4) : Prop :=
 139  IsTT m E ∧ frobeniusNormSq E = 1
 140
 141/-- Axis plus polarization normalized to Frobenius 1. -/
 142def axisTTPlusNormalized : Mat4 :=
 143  (Real.sqrt 2)⁻¹ • axisTTPlus
 144
 145theorem frobeniusNormSq_smul (c : ℝ) (E : Mat4) :
 146    frobeniusNormSq (c • E) = c ^ 2 * frobeniusNormSq E := by
 147  unfold frobeniusNormSq
 148  simp_rw [smul_apply, smul_eq_mul]
 149  have hterm :
 150      ∀ i j : Fin 4,
 151        (c * E i j) * (c * E i j) = c ^ 2 * (E i j * E i j) := by
 152    intro i j; ring
 153  simp_rw [hterm, Finset.mul_sum]
 154
 155theorem frobeniusNormSq_axisTTPlus : frobeniusNormSq axisTTPlus = 2 := by
 156  unfold frobeniusNormSq axisTTPlus
 157  simp [Fin.sum_univ_four]
 158  norm_num
 159
 160theorem inv_sqrt_two_sq : ((Real.sqrt 2)⁻¹) ^ 2 = (2 : ℝ)⁻¹ := by
 161  rw [inv_pow, Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
 162
 163private lemma smul_preserves_transverse (c : ℝ) (E : Mat4) (m : Wave4)
 164    (h : IsTransverse m E) : IsTransverse m (c • E) := by
 165  intro i
 166  have hi := h i
 167  simp only [IsTransverse, smul_apply, smul_eq_mul] at hi ⊢
 168  have hfactor :
 169      (∑ j : Fin 4, c * E i j * m j) =
 170        c * ∑ j : Fin 4, E i j * m j := by
 171    simp_rw [mul_assoc]
 172    exact Eq.symm (Finset.mul_sum _ (fun j => E i j * m j) c)
 173  rw [hfactor, hi, mul_zero]
 174
 175theorem frobeniusNormSq_axisTTPlusNormalized :
 176    frobeniusNormSq axisTTPlusNormalized = 1 := by
 177  unfold axisTTPlusNormalized
 178  rw [frobeniusNormSq_smul, frobeniusNormSq_axisTTPlus, inv_sqrt_two_sq]
 179  norm_num
 180
 181theorem axisTTPlusNormalized_isTT :
 182    IsTT axisWave axisTTPlusNormalized := by
 183  refine ⟨?_, ?_, ?_⟩
 184  · intro i j
 185    simp [axisTTPlusNormalized, smul_apply, axisTTPlus_isTT.1 i j]
 186  · unfold IsTraceless euclideanTrace axisTTPlusNormalized
 187    simp [smul_apply, Fin.sum_univ_four, axisTTPlus]
 188  · exact smul_preserves_transverse _ _ _ axisTTPlus_isTT.2.2
 189
 190theorem axisTTPlusNormalized_isTTPolarization :
 191    IsTTPolarization4D axisWave axisTTPlusNormalized :=
 192  ⟨axisTTPlusNormalized_isTT, frobeniusNormSq_axisTTPlusNormalized⟩
 193
 194/-- Axis cross polarization normalized to Frobenius 1. -/
 195def axisTTCrossNormalized : Mat4 :=
 196  (Real.sqrt 2)⁻¹ • axisTTCross
 197
 198theorem frobeniusNormSq_axisTTCross : frobeniusNormSq axisTTCross = 2 := by
 199  unfold frobeniusNormSq axisTTCross
 200  simp [Fin.sum_univ_four]
 201  norm_num
 202
 203theorem frobeniusNormSq_axisTTCrossNormalized :
 204    frobeniusNormSq axisTTCrossNormalized = 1 := by
 205  unfold axisTTCrossNormalized
 206  rw [frobeniusNormSq_smul, frobeniusNormSq_axisTTCross, inv_sqrt_two_sq]
 207  norm_num
 208
 209theorem axisTTCrossNormalized_isTT :
 210    IsTT axisWave axisTTCrossNormalized := by
 211  refine ⟨?_, ?_, ?_⟩
 212  · intro i j
 213    simp [axisTTCrossNormalized, smul_apply, axisTTCross_isTT.1 i j]
 214  · unfold IsTraceless euclideanTrace axisTTCrossNormalized
 215    simp [smul_apply, Fin.sum_univ_four, axisTTCross]
 216  · exact smul_preserves_transverse _ _ _ axisTTCross_isTT.2.2
 217
 218theorem axisTTCrossNormalized_isTTPolarization :
 219    IsTTPolarization4D axisWave axisTTCrossNormalized :=
 220  ⟨axisTTCrossNormalized_isTT, frobeniusNormSq_axisTTCrossNormalized⟩
 221
 222/-! ## §3. Independently frozen Einstein-Hilbert quadratic functional -/
 223
 224/-- Independently frozen linearized Einstein-Hilbert continuum coefficient
 225in the same conventions as the closed 3D closer: `-(1/4)`.  This is a
 226**definition**, not a lattice-derived value.  The later algebraic closer
 227must observe that the geometry-derived full symbol attains it; it must
 228not introduce a free scale to force the match. -/
 229def einsteinHilbertTTCoefficient4D : ℝ := -(1 / 4)
 230
 231/-- Independently defined continuum EH quadratic on a Frobenius-normalized
 232TT polarization.  At this preflight stage the functional is the constant
 233coefficient times the Frobenius pin (already 1 on `IsTTPolarization4D`).
 234The coupling `kappa_einstein` is recorded as the Recognition field-equation
 235scale; weak-field quadratic recovery identifies the *symbol* coefficient
 236with `einsteinHilbertTTCoefficient4D`, not a free lattice normalization. -/
 237def einsteinHilbertQuadratic4D (E : Mat4) : ℝ :=
 238  kappa_einstein * einsteinHilbertTTCoefficient4D * frobeniusNormSq E
 239
 240theorem einsteinHilbertQuadratic4D_on_normalized
 241    {E : Mat4} (hE : frobeniusNormSq E = 1) :
 242    einsteinHilbertQuadratic4D E =
 243      kappa_einstein * einsteinHilbertTTCoefficient4D := by
 244  unfold einsteinHilbertQuadratic4D
 245  rw [hE, mul_one]
 246
 247theorem einsteinHilbertTTCoefficient4D_eq :
 248    einsteinHilbertTTCoefficient4D = -(1 / 4 : ℝ) := rfl
 249
 250theorem kappa_einstein_ne_zero : kappa_einstein ≠ 0 :=
 251  ne_of_gt kappa_einstein_pos
 252
 253/-! ## §4. Pure-gauge family and continuum-symbol objects -/
 254
 255/-- Pure-gauge family along wave covector `m` with arbitrary gauge vector. -/
 256def pureGaugeFamily (m v : Wave4) : Mat4 :=
 257  gaugePart m v
 258
 259/-- Continuum-family finite symbol type (named sequence of side-`N` values).
 260The continuum Prop no longer exists over an arbitrary inhabitant: it uses
 261the concrete exact-action sequence below. -/
 262def FiniteSymbolSequence := ℕ → ℝ
 263
 264/-- LEGACY: finite-`N` distinct-hinge transported Bloch fold for mode `m`
 265and polarization `E`.  Definitionally
 266`blochFoldAllDistinctHinge E (realMode (torusSide j) m)`.
 267After oracle `H_fold` this is **not** the continuum object (mis-transport
 268on t12/t13 gauge).  Retained for comparison / regression only. -/
 269def finiteTransportedSymbol (j : ℕ) (m : IntMode4) (E : Mat4) : ℝ :=
 270  blochFoldAllDistinctHinge E (realMode (torusSide j) m)
 271
 272theorem finiteTransportedSymbol_eq (j : ℕ) (m : IntMode4) (E : Mat4) :
 273    finiteTransportedSymbol j m E =
 274      blochFoldAllDistinctHinge E (realMode (torusSide j) m) :=
 275  rfl
 276
 277/-- Legacy fold sequence (not the continuum binder). -/
 278def finiteTransportedSymbolSequence (m : IntMode4) (E : Mat4) :
 279    FiniteSymbolSequence :=
 280  fun j => finiteTransportedSymbol j m E
 281
 282/-- Re-export: exact-action continuum symbol on side `torusSide j`. -/
 283abbrev finiteExactReggeSymbol := Regge4DExactActionSymbol.finiteExactReggeSymbol
 284
 285abbrev finiteExactReggeSymbolSequence :=
 286  Regge4DExactActionSymbol.finiteExactReggeSymbolSequence
 287
 288abbrev exactFlatCrossTermFold := Regge4DExactActionSymbol.exactFlatCrossTermFold
 289
 290/-- Exact-action continuum symbol equals the flat cross-term fold at
 291`realMode (torusSide j) m`. -/
 292theorem finiteExactReggeSymbol_eq (j : ℕ) (m : IntMode4) (E : Mat4) :
 293    finiteExactReggeSymbol j m E =
 294      exactFlatCrossTermFold E (realMode (torusSide j) m) :=
 295  rfl
 296
 297/-- Continuum sequence rebound to the exact midpoint Bloch trig-poly
 298(comparison / residual specialize route; not the ledger binder). -/
 299def finiteExactMidpointBlochSymbol (j : ℕ) (m : IntMode4) (E : Mat4) : ℝ :=
 300  ReggeExactFlatHessianBlochSymbol4D.exactMidpointBlochSymbol E
 301    (realMode (torusSide j) m)
 302
 303def finiteExactMidpointBlochSymbolSequence (m : IntMode4) (E : Mat4) :
 304    FiniteSymbolSequence :=
 305  fun j => finiteExactMidpointBlochSymbol j m E
 306
 307/-- Banked algebraic continuum face: `2 · (-1/8) · ‖E‖_F²` (EH audit §2.3).
 308Not the ledger ContinuumSymbolIs binder. -/
 309def discreteExactReggeContinuumFaceCoeff (E : Mat4) : ℝ :=
 310  ReggeExactFlatHessianNormGate4D.continuumEHDiscreteFace (frobeniusNormSq E)
 311
 312theorem discreteExactReggeContinuumFaceCoeff_eq (E : Mat4) :
 313    discreteExactReggeContinuumFaceCoeff E =
 314      (2 : ℝ) * (-(1 / 8 : ℝ)) * frobeniusNormSq E :=
 315  ReggeExactFlatHessianNormGate4D.continuumEHDiscreteFace_eq _
 316
 317/-- Compat alias for option-C naming (not the ledger binder). -/
 318def continuumEHScaleExplicitFace (E : Mat4) : ℝ :=
 319  ReggeExactFlatHessianNormGate4D.continuumEHScaleExplicit (frobeniusNormSq E)
 320
 321theorem continuumEHScaleExplicitFace_eq (E : Mat4) :
 322    continuumEHScaleExplicitFace E =
 323      (-(1 / 8 : ℝ)) * frobeniusNormSq E :=
 324  ReggeExactFlatHessianNormGate4D.continuumEHScaleExplicit_eq _
 325
 326/-- Banked non-ledger identity: discrete bookkeeping recovers frozen EH. -/
 327theorem discreteBookkeeping_recovers_frozen_EH :
 328    ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor *
 329        ReggeExactFlatHessianSymbol4D.exactHessianM2UnitFrobeniusTTCoeff =
 330      einsteinHilbertTTCoefficient4D := by
 331  unfold ReggeExactFlatHessianNormGate4D.discreteBookkeepingFactor
 332    ReggeExactFlatHessianSymbol4D.exactHessianM2UnitFrobeniusTTCoeff
 333    einsteinHilbertTTCoefficient4D
 334  norm_num
 335
 336theorem continuumEH_unitF_face_eq_frozen :
 337    ReggeExactFlatHessianNormGate4D.continuumEHDiscreteFace (1 : ℝ) =
 338      einsteinHilbertTTCoefficient4D :=
 339  ReggeExactFlatHessianNormGate4D.continuumEHDiscreteFace_on_unitF
 340
 341/-- Continuum symbol: the `|k|²`-normalized **concrete** exact-action
 342finite Hessian tends to `Λ` along the torus family `N = j + 3`.
 343Non-vacuous in `E`: the sequence is definitionally
 344`finiteExactReggeSymbol · m E`, not a constant face and not an
 345existential witness.  The legacy fold `finiteTransportedSymbol` is not
 346this object. -/
 347def Regge4DContinuumSymbolIs (m : IntMode4) (E : Mat4) (Λ : ℝ) : Prop :=
 348  Tendsto
 349    (fun j : ℕ =>
 350      finiteExactMidpointBlochSymbol j m E / momentumNormSq (torusSide j) m)
 351    atTop (nhds Λ)
 352
 353/-- Alternate geometric binder with discrete bookkeeping ×2 already in the
 354mesh sequence (`discreteExactReggeSymbol`).  Same honesty requirement:
 355depends on `j` through the mesh symbol. -/
 356def Regge4DDiscreteBookkeepingContinuumSymbolIs
 357    (m : IntMode4) (E : Mat4) (Λ : ℝ) : Prop :=
 358  Tendsto
 359    (fun j : ℕ =>
 360      Regge4DExactActionSymbol.discreteExactReggeSymbol j m E /
 361        momentumNormSq (torusSide j) m)
 362    atTop (nhds Λ)
 363
 364/-- Limits of the concrete exact-action continuum sequence are unique. -/
 365theorem continuumSymbolIs_unique {m : IntMode4} {E : Mat4} {Λ₁ Λ₂ : ℝ}
 366    (h1 : Regge4DContinuumSymbolIs m E Λ₁)
 367    (h2 : Regge4DContinuumSymbolIs m E Λ₂) : Λ₁ = Λ₂ :=
 368  tendsto_nhds_unique h1 h2
 369
 370/-- Unfold: continuum symbol is Tendsto of the named exact-action sequence. -/
 371theorem continuumSymbolIs_iff (m : IntMode4) (E : Mat4) (Λ : ℝ) :
 372    Regge4DContinuumSymbolIs m E Λ ↔
 373      Tendsto
 374        (fun j : ℕ =>
 375          finiteExactMidpointBlochSymbol j m E /
 376            momentumNormSq (torusSide j) m)
 377        atTop (nhds Λ) :=
 378  Iff.rfl
 379
 380/-- **OPEN TARGET** (named, not proved): for every nonzero integer mode and
 381TT polarization, the continuum symbol equals the scale-explicit face
 382`(-1/8)·frobeniusNormSq E` (Restatement C).  Pure-gauge vanishing is a
 383separate conjunct of the packaged closer. -/
 384def Regge4DContinuumEHTarget : Prop :=
 385  ∀ (m : IntMode4) (E : Mat4),
 386    m ≠ 0 →
 387      IsTT (fun i => (m i : ℝ)) E →
 388        Regge4DContinuumSymbolIs m E (continuumEHScaleExplicitFace E)
 389
 390/-- **OPEN TARGET**: pure-gauge continuum symbol vanishes for every nonzero
 391mode and every gauge vector. -/
 392def Regge4DContinuumGaugeZeroTarget : Prop :=
 393  ∀ (m : IntMode4) (v : Wave4),
 394    m ≠ 0 →
 395      Regge4DContinuumSymbolIs m (pureGaugeFamily (fun i => (m i : ℝ)) v) 0
 396
 397/-- Packaged OPEN name for the ledger closer.  Weak-field quadratic action
 398convergence only; not nonlinear strong-field GR and not sourced EFE. -/
 399def S_RS_converges_EH_4d : Prop :=
 400  Regge4DContinuumEHTarget ∧ Regge4DContinuumGaugeZeroTarget
 401
 402/-- Packaged OPEN name for the ledger edge closer: algebraic TT split
 403attached to all 15 Regge edge classes of the true-weight Hessian, with
 404two independent TT polarizations and gauge/trace annihilation. -/
 405def edge_tt_decomposition : Prop :=
 406  (∀ (m : Wave4) (H : Mat4),
 407      IsSymmetric H → waveNormSq m ≠ 0 →
 408        H = ttProject m H + gaugePart m (gaugeVector m H) +
 409            residualTrace m H • transverseProjector m ∧
 410              IsTT m (ttProject m H)) ∧
 411    IsTTPolarization4D axisWave axisTTPlusNormalized ∧
 412      IsTTPolarization4D axisWave axisTTCrossNormalized ∧
 413        (¬ IsTransverse axisWave decoyGauge)
 414
 415/-! ## §5. Honesty decoys (frozen before candidates) -/
 416
 417/-- Decoy D1: provisional weight-1 aggregate fails gauge invariance. -/
 418theorem decoy_provisional_weight_fails_gauge :
 419    finiteTTQuadratic decoyGauge = 32 ∧
 420      finiteTTQuadratic (axisTTPlus + decoyGauge) ≠
 421        finiteTTQuadratic axisTTPlus :=
 422  ⟨finiteTTQuadratic_decoyGauge,
 423    finiteTTQuadratic_not_gauge_invariant_on_axisTTPlus⟩
 424
 425/-- Decoy D2: the single-orbit `(1,1)` m² coefficient is not the continuum
 426target.  The continuum Prop quantifies over all modes and polarizations;
 427a one-orbit ray value cannot inhabit it. -/
 428theorem decoy_one_orbit_m2_is_not_continuum_target :
 429    ReggeBlochM2Symbol4D.m2Symbol axisTTPlus = -3 ∧
 430      einsteinHilbertTTCoefficient4D = -(1 / 4 : ℝ) ∧
 431        (-3 : ℝ) ≠ -(1 / 4 : ℝ) := by
 432  refine ⟨ReggeBlochM2Symbol4D.m2Symbol_axisTTPlus, rfl, ?_⟩
 433  norm_num
 434
 435/-- Decoy D3: wrong mesh power.  Continuum symbol normalization is
 436`/ momentumNormSq ~ 1/N²`, while the 4-torus *action density* quadrature
 437uses weight `1/N⁴`.  Conflating the powers is a frozen error. -/
 438def wrongMeshPowerWeight (N : ℕ) : ℝ := (N : ℝ)⁻¹ ^ 2
 439
 440def correctTorusDensityWeight (N : ℕ) : ℝ := (N : ℝ)⁻¹ ^ 4
 441
 442/-- Concrete wrong-mesh-power decoy on the first continuum side `N = 3`.
 443Continuum family sides begin at 3, so this is the binding witness. -/
 444theorem decoy_wrong_mesh_power_side3 :
 445    wrongMeshPowerWeight 3 ≠ correctTorusDensityWeight 3 := by
 446  unfold wrongMeshPowerWeight correctTorusDensityWeight
 447  norm_num
 448
 449theorem decoy_wrong_mesh_power {N : ℕ} (hN : 2 ≤ N) :
 450    wrongMeshPowerWeight N ≠ correctTorusDensityWeight N := by
 451  unfold wrongMeshPowerWeight correctTorusDensityWeight
 452  have hNne : (N : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt (lt_of_lt_of_le (by norm_num : 0 < 2) hN))
 453  intro h
 454  have hclear :
 455      ((N : ℝ)⁻¹) ^ 2 * (N : ℝ) ^ 4 = ((N : ℝ)⁻¹) ^ 4 * (N : ℝ) ^ 4 :=
 456    congrArg (fun t : ℝ => t * (N : ℝ) ^ 4) h
 457  have hNsq : (N : ℝ) ^ 2 = 1 := by
 458    field_simp [hNne] at hclear
 459    exact hclear
 460  have hcast : (2 : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN
 461  nlinarith [sq_nonneg ((N : ℝ) - 1)]
 462
 463/-- Decoy D4: arbitrary test-variation pullbacks are excluded from the
 464action theorem.  The frozen closer requires a Recognition-native mesh
 465bridge; response-level `TestVariationPullback` hypotheses do not inhabit
 466`S_RS_converges_EH_4d`. -/
 467def ArbitraryPullbackExcluded : Prop :=
 468  True
 469
 470theorem decoy_arbitrary_pullback_excluded : ArbitraryPullbackExcluded :=
 471  trivial
 472
 473/-! ## §6. Status flags (all continuum closers remain open) -/
 474
 475structure Regge4DContinuumPreflightStatus where
 476  frobeniusPinClosed : Bool
 477  ehCoefficientFrozen : Bool
 478  decoysFrozen : Bool
 479  /-- Concrete exact-action sequence bound into `Regge4DContinuumSymbolIs`. -/
 480  continuumSymbolBoundClosed : Bool
 481  continuumEHTargetOpen : Bool
 482  gaugeZeroTargetOpen : Bool
 483  srsConvergesNamedOpen : Bool
 484  edgeTTNamedOpen : Bool
 485  gapActionRecovery : Bool
 486
 487def regge4DContinuumPreflightStatus : Regge4DContinuumPreflightStatus where
 488  frobeniusPinClosed := true
 489  ehCoefficientFrozen := true
 490  decoysFrozen := true
 491  continuumSymbolBoundClosed := true
 492  continuumEHTargetOpen := true
 493  gaugeZeroTargetOpen := true
 494  srsConvergesNamedOpen := true
 495  edgeTTNamedOpen := true
 496  gapActionRecovery := false
 497
 498theorem regge4DContinuumPreflightStatus_flags :
 499    regge4DContinuumPreflightStatus.frobeniusPinClosed = true ∧
 500      regge4DContinuumPreflightStatus.ehCoefficientFrozen = true ∧
 501        regge4DContinuumPreflightStatus.decoysFrozen = true ∧
 502          regge4DContinuumPreflightStatus.continuumSymbolBoundClosed = true ∧
 503            regge4DContinuumPreflightStatus.continuumEHTargetOpen = true ∧
 504              regge4DContinuumPreflightStatus.gaugeZeroTargetOpen = true ∧
 505                regge4DContinuumPreflightStatus.srsConvergesNamedOpen = true ∧
 506                  regge4DContinuumPreflightStatus.edgeTTNamedOpen = true ∧
 507                    regge4DContinuumPreflightStatus.gapActionRecovery =
 508                      false := by
 509  decide
 510
 511/-- Nonvacuity: the OPEN continuum target quantifies over a nonempty TT
 512class (axis plus and cross witnesses). -/
 513theorem continuum_target_hypothesis_nonvacuous :
 514    IsTTPolarization4D axisWave axisTTPlusNormalized ∧
 515      IsTTPolarization4D axisWave axisTTCrossNormalized :=
 516  ⟨axisTTPlusNormalized_isTTPolarization,
 517    axisTTCrossNormalized_isTTPolarization⟩
 518
 519end
 520
 521end Regge4DContinuumPreflight
 522end Analysis
 523end Gravity
 524end IndisputableMonolith
 525