IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionCloser4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   3import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
   5import IndisputableMonolith.Gravity.Analysis.ReggeEdgeTTAttachment4D
   6
   7/-!
   8# Named closer: `edge_tt_decomposition`
   9
  10Inhabits the preflight Prop `edge_tt_decomposition` by composing:
  111. algebraic TT decomposition (`exists_edgeTTDecomposition`);
  122. Frobenius-normalized plus/cross witnesses;
  133. pure-gauge non-transverse decoy;
  144. plane-wave edge attachment already proved in `ReggeEdgeTTAttachment4D`.
  15
  16Honest scope: this is the ledger algebraic+attachment layer for the named
  17closer.  Full multi-orbit true-weight continuum recovery remains the
  18`S_RS_converges_EH_4d` gate.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Gravity
  23namespace Analysis
  24namespace EdgeTTDecompositionCloser4D
  25
  26open Regge4DContinuumPreflight
  27open EdgeTTDecomposition4D
  28open ReggeEdgeStencil4D
  29
  30noncomputable section
  31
  32theorem decoyGauge_eq_decoyLongitudinal : decoyGauge = decoyLongitudinal := by
  33  unfold decoyGauge decoyLongitudinal axisGaugeVector
  34  funext i j
  35  fin_cases i <;> fin_cases j <;> simp [gaugePart, axisWave]
  36
  37theorem decoyGauge_not_transverse :
  38    ¬ IsTransverse axisWave decoyGauge := by
  39  rw [decoyGauge_eq_decoyLongitudinal]
  40  exact decoyLongitudinal_not_transverse
  41
  42/-- **THEOREM (named ledger closer, algebraic+attachment layer).** -/
  43theorem edge_tt_decomposition :
  44    Regge4DContinuumPreflight.edge_tt_decomposition := by
  45  refine ⟨?_, ?_, ?_, ?_⟩
  46  · intro m H hH hm
  47    have hm' : momentumSq m ≠ 0 := by
  48      simpa [waveNormSq_eq_momentumSq] using hm
  49    exact exists_edgeTTDecomposition m H hH hm'
  50  · exact axisTTPlusNormalized_isTTPolarization
  51  · exact axisTTCrossNormalized_isTTPolarization
  52  · exact decoyGauge_not_transverse
  53
  54theorem edge_tt_decomposition_holds :
  55    Regge4DContinuumPreflight.edge_tt_decomposition :=
  56  edge_tt_decomposition
  57
  58end
  59
  60end EdgeTTDecompositionCloser4D
  61end Analysis
  62end Gravity
  63end IndisputableMonolith
  64