IndisputableMonolith.Gravity.Analysis.Regge4DTensorAlgebraicCloser

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4D
   4import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   5import IndisputableMonolith.Gravity.Analysis.Regge4DTorusContinuumLimit
   6import IndisputableMonolith.Gravity.Analysis.Regge4DTransportedAlgebraicCloser
   7import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   8import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
   9
  10/-!
  11# Regge 4D tensor algebraic closer (partial)
  12
  134D counterpart of the 3D `ReggeTTAlgebraicCloser` adjugate identity.
  14Banks the transported distinct-hinge m² as a quadratic form in
  15`(E, dir)` on the TT variety, with every closed ray evaluation available
  16today.  Full closed-form equality to a universal tensor contraction
  17(adjugate-style) remains OPEN.
  18
  19## THEOREM (banked)
  20
  21* Homogeneity: `m2TransportedAllOrbitMomentDistinctHinge (c • E) dir =
  22  c² · m2TransportedAllOrbitMomentDistinctHinge E dir`.
  23* `symbolDir` plus/cross distinct-hinge `-1/4` (normalized `-1/8`).
  24* `e0Dir` plus `0`, cross `-1/8` (normalized `-1/16`).
  25* Arithmetic residual: continuum face `-1/16` vs EH `-1/4` is ratio 4;
  26  density dictionary survivor is `1` (does not close the 4).
  27
  28## OPEN
  29
  30* `Regge4DDistinctHingeTensorClosedFormOpen`: universal bilinear form in
  31  `(E, dir)` matching the distinct-hinge moment on all TT / nonzero dir.
  32* `Regge4DDistinctHingePinnedVsEHFactor4`: geometric (Schläfli / path B)
  33  account of the residual 4.  No magic-4 multiplier installed.
  34* Axis-mode isotropy blocker (imported from M2Eval; negative fact closed).
  35
  36Does **not** flip `gap_action_recovery`.
  37-/
  38
  39namespace IndisputableMonolith
  40namespace Gravity
  41namespace Analysis
  42namespace Regge4DTensorAlgebraicCloser
  43
  44open BigOperators
  45open ReggeBlochTransportedAllOrbit4D
  46open ReggeBlochTransportedAllOrbitM2Eval4D
  47open Regge4DContinuumPreflight
  48open Regge4DTorusContinuumLimit
  49open Regge4DTransportedAlgebraicCloser (symbolDir_normSq)
  50open EdgeTTDecomposition4D (axisTTPlus axisTTCross)
  51open ReggeBlochM2Symbol4D (symbolDir)
  52
  53abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
  54
  55noncomputable section
  56
  57/-! ## §1. Quadratic form object -/
  58
  59/-- Distinct-hinge transported m² as a quadratic form in the polarization. -/
  60def distinctHingeMomentForm (E : Mat4) (dir : Fin 4 → ℝ) : ℝ :=
  61  m2TransportedAllOrbitMomentDistinctHinge E dir
  62
  63theorem distinctHingeMomentForm_smul (c : ℝ) (E : Mat4) (dir : Fin 4 → ℝ) :
  64    distinctHingeMomentForm (c • E) dir =
  65      c ^ 2 * distinctHingeMomentForm E dir :=
  66  m2TransportedAllOrbitMomentDistinctHinge_smul c E dir
  67
  68theorem distinctHingeMomentForm_zero (dir : Fin 4 → ℝ) :
  69    distinctHingeMomentForm 0 dir = 0 := by
  70  simpa using distinctHingeMomentForm_smul (0 : ℝ) (1 : Mat4) dir
  71
  72/-! ## §2. Banked ray evaluations -/
  73
  74theorem distinctHingeMomentForm_axisTTPlus_symbolDir :
  75    distinctHingeMomentForm axisTTPlus symbolDir = (-1 / 4 : ℝ) :=
  76  m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir
  77
  78theorem distinctHingeMomentForm_axisTTCross_symbolDir :
  79    distinctHingeMomentForm axisTTCross symbolDir = (-1 / 4 : ℝ) :=
  80  m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_symbolDir
  81
  82theorem distinctHingeMomentForm_axisTTPlus_e0Dir :
  83    distinctHingeMomentForm axisTTPlus e0Dir = (0 : ℝ) :=
  84  m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_e0Dir
  85
  86theorem distinctHingeMomentForm_axisTTCross_e0Dir :
  87    distinctHingeMomentForm axisTTCross e0Dir = (-1 / 8 : ℝ) :=
  88  m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_e0Dir
  89
  90/-- Continuum-facing coefficient after `/|dir|²` on the pinned symbolDir
  91normalized plus ray: `-1/16`. -/
  92theorem continuumFace_normalizedPlus_symbolDir :
  93    distinctHingeMomentForm ((Real.sqrt 2)⁻¹ • axisTTPlus) symbolDir /
  94        (∑ i : Fin 4, symbolDir i * symbolDir i) =
  95      (-1 / 16 : ℝ) := by
  96  unfold distinctHingeMomentForm
  97  rw [m2TransportedAllOrbitMomentDistinctHinge_axisTTPlusNormalized_symbolDir,
  98    symbolDir_normSq]
  99  norm_num
 100
 101/-- On `e0Dir`, normalized cross already hits continuum face `-1/16`
 102(since `|e0Dir|² = 1`); normalized plus hits `0`. -/
 103theorem continuumFace_normalizedCross_e0Dir :
 104    distinctHingeMomentForm ((Real.sqrt 2)⁻¹ • axisTTCross) e0Dir /
 105        (∑ i : Fin 4, e0Dir i * e0Dir i) =
 106      (-1 / 16 : ℝ) := by
 107  unfold distinctHingeMomentForm
 108  rw [m2TransportedAllOrbitMomentDistinctHinge_axisTTCrossNormalized_e0Dir,
 109    e0Dir_normSq]
 110  norm_num
 111
 112theorem continuumFace_normalizedPlus_e0Dir_vanishes :
 113    distinctHingeMomentForm ((Real.sqrt 2)⁻¹ • axisTTPlus) e0Dir /
 114        (∑ i : Fin 4, e0Dir i * e0Dir i) =
 115      (0 : ℝ) := by
 116  unfold distinctHingeMomentForm
 117  rw [m2TransportedAllOrbitMomentDistinctHinge_axisTTPlusNormalized_e0Dir,
 118    e0Dir_normSq]
 119  norm_num
 120
 121/-! ## §3. OPEN closed-form and factor-4 obligations -/
 122
 123/-- **OPEN**: a universal tensor closed form on TT × nonzero directions,
 124in the spirit of the 3D adjugate identity
 125`K = (1/2) xᵀ adj(E) x = -(1/4)|x|²‖E‖_F²`. -/
 126def Regge4DDistinctHingeTensorClosedFormOpen : Prop :=
 127  ∃ (Q : Mat4 → (Fin 4 → ℝ) → ℝ),
 128    (∀ (c : ℝ) (E : Mat4) (dir : Fin 4 → ℝ),
 129        Q (c • E) dir = c ^ 2 * Q E dir) ∧
 130      (∀ (E : Mat4) (dir : Fin 4 → ℝ),
 131        IsTTPolarization4D dir E →
 132          (∑ i : Fin 4, dir i * dir i) ≠ 0 →
 133            distinctHingeMomentForm E dir = Q E dir)
 134
 135/-- Arithmetic residual (THEOREM side): pinned continuum face vs EH. -/
 136theorem residual_factor_four_arithmetic :
 137    einsteinHilbertTTCoefficient4D = (4 : ℝ) * (-1 / 16 : ℝ) ∧
 138      DistinctHingePinnedMomentVsEH ∧
 139        survivingDictionaryFactor4D = 1 :=
 140  ⟨by rw [einsteinHilbertTTCoefficient4D_eq]; norm_num,
 141    distinctHinge_pinned_ne_eh, rfl⟩
 142
 143/-- **OPEN**: geometric (Schläfli elevation / 3D-style local-incidence
 144path B) identity that forces the residual factor 4.  Naming only; no
 145theorem inhabits this Prop, and no magic-4 multiplier is installed on
 146the continuum sequence. -/
 147def Regge4DDistinctHingePinnedVsEHFactor4 : Prop :=
 148  Regge4DContinuumEHTarget
 149
 150/-- Status flag: factor-4 geometric closure still open. -/
 151theorem Regge4DDistinctHingePinnedVsEHFactor4_status_open :
 152    regge4DTorusContinuumLimitStatus.ehTendstoInhabited = false :=
 153  rfl
 154
 155theorem axis_isotropy_blocker_negated :
 156    ¬ Regge4DContinuumIsotropyBlockedOnAxisMode :=
 157  Regge4DContinuumIsotropyBlockedOnAxisMode_status_false
 158
 159structure Regge4DTensorAlgebraicCloserStatus where
 160  rayEvaluationsBanked : Bool
 161  homogeneityClosed : Bool
 162  tensorClosedFormOpen : Bool
 163  factor4GeometricOpen : Bool
 164  axisIsotropyBlocked : Bool
 165  gapActionRecovery : Bool
 166
 167def regge4DTensorAlgebraicCloserStatus : Regge4DTensorAlgebraicCloserStatus where
 168  rayEvaluationsBanked := true
 169  homogeneityClosed := true
 170  tensorClosedFormOpen := true
 171  factor4GeometricOpen := true
 172  axisIsotropyBlocked := true
 173  gapActionRecovery := false
 174
 175theorem regge4DTensorAlgebraicCloserStatus_flags :
 176    regge4DTensorAlgebraicCloserStatus.rayEvaluationsBanked = true ∧
 177      regge4DTensorAlgebraicCloserStatus.homogeneityClosed = true ∧
 178        regge4DTensorAlgebraicCloserStatus.tensorClosedFormOpen = true ∧
 179          regge4DTensorAlgebraicCloserStatus.factor4GeometricOpen = true ∧
 180            regge4DTensorAlgebraicCloserStatus.axisIsotropyBlocked = true ∧
 181              regge4DTensorAlgebraicCloserStatus.gapActionRecovery =
 182                false := by
 183  decide
 184
 185theorem does_not_flip_gap_action_recovery :
 186    regge4DTensorAlgebraicCloserStatus.gapActionRecovery = false :=
 187  rfl
 188
 189end
 190
 191end Regge4DTensorAlgebraicCloser
 192end Analysis
 193end Gravity
 194end IndisputableMonolith
 195