IndisputableMonolith.Gravity.Analysis.Regge4DAlgebraicCloser

   1import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   2import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
   3import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   4import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   5import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
   6
   7/-!
   8# Regge 4D algebraic closer: banked witnesses, full-moment skeleton, OPEN isotropy
   9
  10QG full-theory campaign, 4D counterpart of `ReggeTTAlgebraicCloser`.
  11Consumes the frozen continuum preflight target and the geometry-derived
  12orbit / (1,1)-symbol stack.  Banks every immediately available algebraic
  13identity; names the full TT isotropy / gauge / plus-cross agreement
  14targets as OPEN Props with status flags `false`.
  15
  16## What this module proves (THEOREM)
  17
  18* Decoy: one-orbit `(1,1)` `m2Symbol` equals `-3`, not the frozen EH
  19  coefficient `einsteinHilbertTTCoefficient4D = -1/4` (via preflight).
  20* Plus / cross Frobenius-normalized TT witnesses inhabit
  21  `IsTTPolarization4D` (via preflight).
  22* Gauge: `(1,1)`-orbit `m2Symbol decoyGauge = 0` (via M2 module).
  23* Full zero-momentum moment object: sum over `HingeOrbitType` of
  24  `orbitZeroMomQuadratic`, identified with
  25  `trueWeightZeroMomQuadratic`, vanishing on axis TT plus and decoy
  26  gauge (via assembly theorems).
  27
  28## OPEN (named Prop + status `false`; no sorry-as-proof)
  29
  30* `Regge4DFullTTIsotropyTarget`: for every nonzero real direction and
  31  every Frobenius-normalized TT polarization, the all-orbit m² moment
  32  divided by `|k|²` equals `einsteinHilbertTTCoefficient4D = -1/4`.
  33* `Regge4DPureGaugeVanishesTarget`: pure-gauge all-orbit m² moment
  34  vanishes for every nonzero direction.
  35* `Regge4DPlusCrossAgreeTarget`: plus and cross normalized symbols agree.
  36
  37## Disclosures (binding)
  38
  39* Continuum symbol Prop is now the concrete transported sequence
  40  `finiteTransportedSymbol` (see `Regge4DTransportedAlgebraicCloser`);
  41  factorized `ReggeBlochAllOrbitSymbol4D` is not that object.
  42* Zero-momentum full-moment identities below remain banked witnesses;
  43  finite-momentum EH Tendsto lives in the transported closer as OPEN.
  44* This does **not** prove `S_RS_converges_EH_4d`.
  45* This does **not** flip `gap_action_recovery`.
  46* No `sorry`, no `admit`, no new axioms, no `native_decide`, no `: True`
  47  shells as headlines.
  48
  49Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  50-/
  51
  52namespace IndisputableMonolith
  53namespace Gravity
  54namespace Analysis
  55namespace Regge4DAlgebraicCloser
  56
  57open BigOperators
  58open Regge4DContinuumPreflight
  59open ReggeBlochM2Symbol4D
  60open ReggeFlat4DHessianAssembly
  61open ReggeHinge4DOrbitClassification
  62open ReggeEdgeStencil4D
  63open EdgeTTDecomposition4D (axisWave axisTTPlus IsTT)
  64
  65/-- Prefer the preflight matrix alias; both are definitionally `Matrix (Fin 4) (Fin 4) ℝ`. -/
  66abbrev Mat4 := Regge4DContinuumPreflight.Mat4
  67
  68noncomputable section
  69
  70/-! ## §1. Banked decoy and normalized TT witnesses -/
  71
  72/-- Decoy: the single-orbit `(1,1)` m² coefficient is not the continuum EH
  73target. -/
  74theorem decoy_one_orbit_m2_ne_eh_coefficient :
  75    ReggeBlochM2Symbol4D.m2Symbol axisTTPlus = -3 ∧
  76      einsteinHilbertTTCoefficient4D = -(1 / 4 : ℝ) ∧
  77        (-3 : ℝ) ≠ -(1 / 4 : ℝ) :=
  78  decoy_one_orbit_m2_is_not_continuum_target
  79
  80/-- Axis plus polarization, Frobenius-normalized, is TT. -/
  81theorem plus_normalized_isTTPolarization :
  82    IsTTPolarization4D axisWave axisTTPlusNormalized :=
  83  axisTTPlusNormalized_isTTPolarization
  84
  85/-- Axis cross polarization, Frobenius-normalized, is TT. -/
  86theorem cross_normalized_isTTPolarization :
  87    IsTTPolarization4D axisWave axisTTCrossNormalized :=
  88  axisTTCrossNormalized_isTTPolarization
  89
  90/-- Nonvacuity of the TT hypothesis class used by continuum targets. -/
  91theorem tt_witnesses_nonvacuous :
  92    IsTTPolarization4D axisWave axisTTPlusNormalized ∧
  93      IsTTPolarization4D axisWave axisTTCrossNormalized :=
  94  continuum_target_hypothesis_nonvacuous
  95
  96/-! ## §2. Banked (1,1)-orbit gauge vanishing on the symbolDir ray -/
  97
  98/-- Gauge: the closed-form `(1,1)` m² symbol vanishes on `decoyGauge`. -/
  99theorem gauge_m2Symbol_vanishes_on_decoy :
 100    ReggeBlochM2Symbol4D.m2Symbol decoyGauge = 0 :=
 101  m2Symbol_decoyGauge
 102
 103/-- TT nonvacuity of the same one-orbit coefficient. -/
 104theorem one_orbit_m2Symbol_axis_ne_zero :
 105    ReggeBlochM2Symbol4D.m2Symbol axisTTPlus ≠ 0 :=
 106  m2Symbol_axisTTPlus_ne_zero
 107
 108/-- Frozen EH coefficient value (definitional). -/
 109theorem eh_tt_coefficient_eq :
 110    einsteinHilbertTTCoefficient4D = -(1 / 4 : ℝ) :=
 111  einsteinHilbertTTCoefficient4D_eq
 112
 113/-! ## §3. Full-moment object as orbit sum (AllOrbit module absent) -/
 114
 115/-- Per-orbit contribution to the full zero-momentum moment. -/
 116def fullMomentOrbitContribution (ty : HingeOrbitType) (H : Mat4) : ℝ :=
 117  orbitZeroMomQuadratic ty H
 118
 119/-- Full zero-momentum moment: sum of orbit contributions over every
 120`HingeOrbitType`.  When `ReggeBlochAllOrbitSymbol4D` lands, its finite-
 121momentum m² polynomial is the intended continuum-facing upgrade of this
 122object; the zero-momentum reduction must continue to match. -/
 123def fullMomentZeroMomentum (H : Mat4) : ℝ :=
 124  ∑ ty : HingeOrbitType, fullMomentOrbitContribution ty H
 125
 126theorem fullMomentZeroMomentum_eq_trueWeight (H : Mat4) :
 127    fullMomentZeroMomentum H = trueWeightZeroMomQuadratic H := by
 128  unfold fullMomentZeroMomentum fullMomentOrbitContribution
 129    trueWeightZeroMomQuadratic
 130  rfl
 131
 132theorem fullMomentOrbitContribution_eq_bilinear (ty : HingeOrbitType)
 133    (H : Mat4) :
 134    fullMomentOrbitContribution ty H = orbitZeroMomBilinear ty H H :=
 135  orbitZeroMomQuadratic_eq_bilinear ty H
 136
 137theorem fullMomentZeroMomentum_eq_bilinear (H : Mat4) :
 138    fullMomentZeroMomentum H = trueWeightZeroMomBilinear H H := by
 139  rw [fullMomentZeroMomentum_eq_trueWeight,
 140    trueWeightZeroMomQuadratic_eq_bilinear]
 141
 142/-- Zero-momentum full moment vanishes on axis TT plus. -/
 143theorem fullMomentZeroMomentum_axisTTPlus :
 144    fullMomentZeroMomentum axisTTPlus = 0 := by
 145  rw [fullMomentZeroMomentum_eq_trueWeight,
 146    trueWeightZeroMomQuadratic_axisTTPlus]
 147
 148/-- Zero-momentum full moment vanishes on decoy gauge. -/
 149theorem fullMomentZeroMomentum_decoyGauge :
 150    fullMomentZeroMomentum decoyGauge = 0 := by
 151  rw [fullMomentZeroMomentum_eq_trueWeight,
 152    trueWeightZeroMomQuadratic_decoyGauge]
 153
 154/-- Zero-momentum full moment vanishes on decoy trace / homothety. -/
 155theorem fullMomentZeroMomentum_decoyTrace :
 156    fullMomentZeroMomentum decoyTrace = 0 := by
 157  rw [fullMomentZeroMomentum_eq_trueWeight,
 158    trueWeightZeroMomQuadratic_decoyTrace]
 159
 160/-- Per-orbit deficit annihilation implies per-orbit contribution zero. -/
 161theorem fullMomentOrbitContribution_of_deficit_zero
 162    (ty : HingeOrbitType) (H : Mat4)
 163    (h : classDot (orbitDeficitKernel ty) H = 0) :
 164    fullMomentOrbitContribution ty H = 0 := by
 165  unfold fullMomentOrbitContribution orbitZeroMomQuadratic
 166  rw [h, mul_zero]
 167
 168theorem fullMomentOrbitContribution_axisTTPlus (ty : HingeOrbitType) :
 169    fullMomentOrbitContribution ty axisTTPlus = 0 :=
 170  fullMomentOrbitContribution_of_deficit_zero ty _
 171    (orbitDeficit_dot_axisTTPlus ty)
 172
 173theorem fullMomentOrbitContribution_decoyGauge (ty : HingeOrbitType) :
 174    fullMomentOrbitContribution ty decoyGauge = 0 :=
 175  fullMomentOrbitContribution_of_deficit_zero ty _
 176    (orbitDeficit_dot_decoyGauge ty)
 177
 178/-! ## §4. OPEN algebraic continuum targets
 179
 180These are the algebraic-layer packaging of the preflight continuum Props.
 181They quantify over real directions and Frobenius-normalized TT data.
 182Status flags below stay `false`; inhabitation is deferred to later
 183modules that supply the all-orbit finite-momentum m² moment.
 184-/
 185
 186/-- Integer mode matching the axis wave `(1,0,0,0)` used by the plus/cross
 187witnesses. -/
 188def axisIntMode : IntMode4 :=
 189  fun i => if i = 0 then (1 : ℤ) else 0
 190
 191/-- **OPEN**: algebraic packaging of the preflight continuum EH target.
 192For every nonzero integer mode and Frobenius-normalized TT polarization,
 193the `|k|²`-normalized **concrete transported** continuum symbol equals
 194`einsteinHilbertTTCoefficient4D = -1/4`. -/
 195def Regge4DFullTTIsotropyTarget : Prop :=
 196  Regge4DContinuumEHTarget
 197
 198/-- **OPEN**: pure-gauge continuum symbol vanishes for every nonzero mode
 199and every gauge vector (preflight packaging). -/
 200def Regge4DPureGaugeVanishesTarget : Prop :=
 201  Regge4DContinuumGaugeZeroTarget
 202
 203/-- **OPEN**: plus and cross normalized continuum symbols agree on the
 204axis mode (concrete transported sequences for each polarization). -/
 205def Regge4DPlusCrossAgreeTarget : Prop :=
 206  ∀ Λplus Λcross : ℝ,
 207    Regge4DContinuumSymbolIs axisIntMode axisTTPlusNormalized Λplus →
 208      Regge4DContinuumSymbolIs axisIntMode axisTTCrossNormalized Λcross →
 209        Λplus = Λcross
 210
 211/-- Packaged algebraic closer target (all three OPEN conjuncts). -/
 212def Regge4DAlgebraicCloserTarget : Prop :=
 213  Regge4DFullTTIsotropyTarget ∧
 214    Regge4DPureGaugeVanishesTarget ∧
 215      Regge4DPlusCrossAgreeTarget
 216
 217/-- Convenience: full isotropy implies the frozen coefficient value. -/
 218theorem fullTTIsotropyTarget_mentions_eh_coefficient :
 219    einsteinHilbertTTCoefficient4D = -(1 / 4 : ℝ) ∧
 220      Regge4DFullTTIsotropyTarget = Regge4DContinuumEHTarget :=
 221  ⟨einsteinHilbertTTCoefficient4D_eq, rfl⟩
 222
 223/-! ## §5. Status flags (gap_action_recovery stays false) -/
 224
 225structure Regge4DAlgebraicCloserStatus where
 226  decoyOneOrbitClosed : Bool
 227  plusCrossWitnessesClosed : Bool
 228  gaugeM2SymbolClosed : Bool
 229  fullMomentZeroMomClosed : Bool
 230  /-- Full TT isotropy at EH coefficient: still OPEN. -/
 231  fullTTIsotropyClosed : Bool
 232  /-- Pure-gauge vanishing for every direction: still OPEN. -/
 233  pureGaugeVanishesClosed : Bool
 234  /-- Plus/cross continuum agreement: still OPEN. -/
 235  plusCrossAgreeClosed : Bool
 236  /-- Continuum action recovery: not claimed here. -/
 237  srsConvergesEH4d : Bool
 238  /-- Ledger flag must stay false. -/
 239  gapActionRecovery : Bool
 240
 241def regge4DAlgebraicCloserStatus : Regge4DAlgebraicCloserStatus where
 242  decoyOneOrbitClosed := true
 243  plusCrossWitnessesClosed := true
 244  gaugeM2SymbolClosed := true
 245  fullMomentZeroMomClosed := true
 246  fullTTIsotropyClosed := false
 247  pureGaugeVanishesClosed := false
 248  plusCrossAgreeClosed := false
 249  srsConvergesEH4d := false
 250  gapActionRecovery := false
 251
 252theorem regge4DAlgebraicCloserStatus_flags :
 253    regge4DAlgebraicCloserStatus.decoyOneOrbitClosed = true ∧
 254      regge4DAlgebraicCloserStatus.plusCrossWitnessesClosed = true ∧
 255        regge4DAlgebraicCloserStatus.gaugeM2SymbolClosed = true ∧
 256          regge4DAlgebraicCloserStatus.fullMomentZeroMomClosed = true ∧
 257            regge4DAlgebraicCloserStatus.fullTTIsotropyClosed = false ∧
 258              regge4DAlgebraicCloserStatus.pureGaugeVanishesClosed = false ∧
 259                regge4DAlgebraicCloserStatus.plusCrossAgreeClosed = false ∧
 260                  regge4DAlgebraicCloserStatus.srsConvergesEH4d = false ∧
 261                    regge4DAlgebraicCloserStatus.gapActionRecovery = false := by
 262  decide
 263
 264/-- Honesty: banked one-orbit identities do not inhabit the OPEN isotropy
 265target, and the ledger flag stays false. -/
 266theorem banked_does_not_flip_gap_or_isotropy :
 267    regge4DAlgebraicCloserStatus.fullTTIsotropyClosed = false ∧
 268      regge4DAlgebraicCloserStatus.gapActionRecovery = false ∧
 269        ReggeBlochM2Symbol4D.m2Symbol axisTTPlus ≠
 270          einsteinHilbertTTCoefficient4D := by
 271  refine ⟨rfl, rfl, ?_⟩
 272  rw [m2Symbol_axisTTPlus, einsteinHilbertTTCoefficient4D_eq]
 273  norm_num
 274
 275end
 276
 277end Regge4DAlgebraicCloser
 278end Analysis
 279end Gravity
 280end IndisputableMonolith
 281