IndisputableMonolith.Gravity.Analysis.Regge4DTransportedAlgebraicCloser

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   3import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
   5import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Tendsto4D
   6import IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D
   7import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   8import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
   9import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification
  10
  11/-!
  12# Transported 4D algebraic closer: concrete continuum sequence + banked ids
  13
  14Binds the preflight continuum Prop to the transported multi-orbit fold and
  15banks every algebraic identity available without claiming EH Tendsto
  16`-(1/4)` or inhabiting `S_RS_converges_EH_4d`.
  17
  18## THEOREM (banked here)
  19
  20* Continuum symbol sequence is definitionally
  21  `blochFoldAllDistinctHinge` (weight `1/r_τ`) on the torus family
  22  (`finiteTransportedSymbol`).
  23* Limit uniqueness for that concrete sequence.
  24* Quadratic homogeneity of `blochFoldAllDistinctHinge` /
  25  `finiteTransportedSymbol`.
  26* Distinct-hinge orbit-sum decomposition of the finite transported symbol.
  27* `(1,1)`-orbit `FoldAlongM2Tendsto` for axis TT (`-3`) and decoy gauge
  28  (`0`), via `ReggeBlochM2Tendsto4D`.
  29* One-orbit ray normalized coefficient `m2Symbol / |symbolDir|²` is not
  30  the frozen EH coefficient (decoy strengthening).
  31* Area-convention match: `blochFoldOrbit .t11 = blochFold11` and
  32  `AreaPushforwardMatchOpen` (via `slotOrbitAreaCov_t11`).
  33
  34## OPEN (named; status `false`; no fake inhabit)
  35
  36* `Regge4DContinuumEHTarget`: Tendsto of normalized transported fold to
  37  `-(1/4)` on Frobenius TT.
  38* `Regge4DContinuumGaugeZeroTarget`: Tendsto to `0` on pure gauge.
  39
  40## Disclosures
  41
  42* Factorized `ReggeBlochAllOrbitSymbol4D` is not the continuum object
  43  (`L-p1-factorized-vs-transported-fold`).
  44* Does **not** flip `gap_action_recovery`.
  45* No `sorry` / `admit` / new axioms / `native_decide` / `: True` headlines.
  46
  47Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  48-/
  49
  50namespace IndisputableMonolith
  51namespace Gravity
  52namespace Analysis
  53namespace Regge4DTransportedAlgebraicCloser
  54
  55open BigOperators Filter Topology
  56open Regge4DContinuumPreflight
  57open ReggeBlochTransportedAllOrbit4D
  58open ReggeBlochM2Symbol4D
  59open ReggeBlochM2Tendsto4D
  60open ReggeBlochFold4D
  61open ReggeHinge4DOrbitClassification
  62open ReggeEdgeStencil4D
  63open EdgeTTDecomposition4D
  64
  65abbrev Mat4 := Regge4DContinuumPreflight.Mat4
  66
  67noncomputable section
  68
  69/-! ## §1. Concrete continuum sequence binding -/
  70
  71theorem finiteTransportedSymbol_eq_blochFoldAllDistinctHinge
  72    (j : ℕ) (m : IntMode4) (E : Mat4) :
  73    finiteTransportedSymbol j m E =
  74      blochFoldAllDistinctHinge E (realMode (torusSide j) m) :=
  75  finiteTransportedSymbol_eq j m E
  76
  77/-- Compatibility alias: continuum sequence is the distinct-hinge fold. -/
  78theorem finiteTransportedSymbol_eq_blochFoldAll (j : ℕ) (m : IntMode4)
  79    (E : Mat4) :
  80    finiteTransportedSymbol j m E =
  81      blochFoldAllDistinctHinge E (realMode (torusSide j) m) :=
  82  finiteTransportedSymbol_eq_blochFoldAllDistinctHinge j m E
  83
  84theorem continuumSymbolIs_unique_limit {m : IntMode4} {E : Mat4}
  85    {Λ₁ Λ₂ : ℝ} (h1 : Regge4DContinuumSymbolIs m E Λ₁)
  86    (h2 : Regge4DContinuumSymbolIs m E Λ₂) : Λ₁ = Λ₂ :=
  87  continuumSymbolIs_unique h1 h2
  88
  89theorem finiteTransportedSymbol_eq_orbit_sum (j : ℕ) (m : IntMode4)
  90    (E : Mat4) :
  91    finiteTransportedSymbol j m E =
  92      ∑ ty : HingeOrbitType,
  93        (orbitStarSize ty)⁻¹ *
  94          blochFoldOrbit ty E (realMode (torusSide j) m) := by
  95  rw [finiteTransportedSymbol_eq_blochFoldAllDistinctHinge]
  96  rfl
  97
  98/-- `(1,1)` orbit slice of the concrete continuum sequence (unweighted). -/
  99def finiteTransportedT11Symbol (j : ℕ) (m : IntMode4) (E : Mat4) : ℝ :=
 100  blochFoldOrbit .t11 E (realMode (torusSide j) m)
 101
 102theorem finiteTransportedT11Symbol_eq (j : ℕ) (m : IntMode4) (E : Mat4) :
 103    finiteTransportedT11Symbol j m E =
 104      blochFoldOrbit .t11 E (realMode (torusSide j) m) :=
 105  rfl
 106
 107/-! ## §2. Quadratic homogeneity -/
 108
 109theorem finiteTransportedSymbol_smul (c : ℝ) (j : ℕ) (m : IntMode4)
 110    (E : Mat4) :
 111    finiteTransportedSymbol j m (c • E) =
 112      c ^ 2 * finiteTransportedSymbol j m E := by
 113  simp_rw [finiteTransportedSymbol_eq_blochFoldAllDistinctHinge,
 114    blochFoldAllDistinctHinge_smul]
 115
 116theorem finiteTransportedSymbol_zero (j : ℕ) (m : IntMode4) :
 117    finiteTransportedSymbol j m 0 = 0 := by
 118  simpa using finiteTransportedSymbol_smul (0 : ℝ) j m (1 : Mat4)
 119
 120/-! ## §3. Banked (1,1) m² Tendsto witnesses (not continuum EH) -/
 121
 122/-- Axis TT: `(1,1)` foldAlong / μ² → `m2Symbol = -3`. -/
 123theorem t11_foldAlong_m2_tendsto_axisTTPlus :
 124    FoldAlongM2Tendsto axisTTPlus :=
 125  FoldAlongM2Tendsto_of_axisTTPlus
 126
 127/-- Pure gauge decoy: `(1,1)` foldAlong / μ² → `0`. -/
 128theorem t11_foldAlong_m2_tendsto_decoyGauge :
 129    FoldAlongM2Tendsto decoyGauge :=
 130  FoldAlongM2Tendsto_of_decoyGauge
 131
 132theorem t11_m2Symbol_axisTTPlus :
 133    m2Symbol axisTTPlus = -3 :=
 134  m2Symbol_axisTTPlus
 135
 136theorem t11_m2Symbol_decoyGauge :
 137    m2Symbol decoyGauge = 0 :=
 138  m2Symbol_decoyGauge
 139
 140/-- Integer mode along the closed `(1,1)` symbol ray `(1,1,0,0)`. -/
 141def symbolDirIntMode : IntMode4 :=
 142  fun i => if i.val < 2 then (1 : ℤ) else 0
 143
 144theorem symbolDir_normSq :
 145    (∑ i : Fin 4, symbolDir i * symbolDir i) = (2 : ℝ) := by
 146  simp [symbolDir, Fin.sum_univ_four]
 147  norm_num
 148
 149theorem realMode_symbolDirIntMode (N : ℕ) (_hN : N ≠ 0) :
 150    realMode N symbolDirIntMode =
 151      fun i => ((2 * Real.pi) / (N : ℝ)) * symbolDir i := by
 152  funext i
 153  unfold realMode symbolDirIntMode symbolDir
 154  fin_cases i <;> simp
 155
 156/-- One-orbit ray coefficient after `/|k|²` normalization on `symbolDir`:
 157`m2Symbol / |symbolDir|²`.  For axis TT this is `-3/2`, not EH `-1/4`. -/
 158def oneOrbitRayNormalizedCoeff (H : Mat4) : ℝ :=
 159  m2Symbol H / (∑ i : Fin 4, symbolDir i * symbolDir i)
 160
 161theorem oneOrbitRayNormalizedCoeff_axisTTPlus :
 162    oneOrbitRayNormalizedCoeff axisTTPlus = (-3 : ℝ) / 2 := by
 163  unfold oneOrbitRayNormalizedCoeff
 164  rw [m2Symbol_axisTTPlus, symbolDir_normSq]
 165
 166theorem oneOrbit_ray_normalized_ne_eh_coefficient :
 167    oneOrbitRayNormalizedCoeff axisTTPlus ≠
 168      einsteinHilbertTTCoefficient4D := by
 169  rw [oneOrbitRayNormalizedCoeff_axisTTPlus, einsteinHilbertTTCoefficient4D_eq]
 170  norm_num
 171
 172theorem oneOrbit_m2_ne_eh_coefficient :
 173    m2Symbol axisTTPlus ≠ einsteinHilbertTTCoefficient4D := by
 174  rw [m2Symbol_axisTTPlus, einsteinHilbertTTCoefficient4D_eq]
 175  norm_num
 176
 177/-! ## §4. OPEN continuum value targets (transported; honest) -/
 178
 179/-- **OPEN**: Frobenius-normalized TT transported continuum symbol equals
 180`einsteinHilbertTTCoefficient4D = -1/4`. -/
 181def Regge4DTransportedTTIsotropyOpen : Prop :=
 182  Regge4DContinuumEHTarget
 183
 184/-- **OPEN**: pure-gauge transported continuum symbol vanishes. -/
 185def Regge4DTransportedGaugeZeroOpen : Prop :=
 186  Regge4DContinuumGaugeZeroTarget
 187
 188/-- Formerly OPEN area-covector convention match; now THEOREM. -/
 189def Regge4DTransportedAreaMatchOpen : Prop :=
 190  AreaPushforwardMatchOpen
 191
 192theorem Regge4DTransportedAreaMatchOpen_holds :
 193    Regge4DTransportedAreaMatchOpen :=
 194  AreaPushforwardMatchOpen_holds
 195
 196/-- `(1,1)` orbit fold recovers the classical `blochFold11`. -/
 197theorem blochFoldOrbit_t11_eq_blochFold11 (H : Mat4) (m : Fin 4 → ℝ) :
 198    blochFoldOrbit .t11 H m = blochFold11 H m :=
 199  blochFoldOrbit_t11 H m
 200
 201/-- Packaged OPEN algebraic closer (area match removed; now proved). -/
 202def Regge4DTransportedAlgebraicCloserTarget : Prop :=
 203  Regge4DTransportedTTIsotropyOpen ∧ Regge4DTransportedGaugeZeroOpen
 204
 205theorem transported_targets_eq_preflight :
 206    Regge4DTransportedTTIsotropyOpen = Regge4DContinuumEHTarget ∧
 207      Regge4DTransportedGaugeZeroOpen = Regge4DContinuumGaugeZeroTarget :=
 208  ⟨rfl, rfl⟩
 209
 210/-! ## §5. Status flags -/
 211
 212structure Regge4DTransportedAlgebraicCloserStatus where
 213  continuumSymbolBoundClosed : Bool
 214  quadraticHomogeneityClosed : Bool
 215  t11M2TendstoClosed : Bool
 216  oneOrbitDecoyClosed : Bool
 217  /-- Full TT isotropy at EH `-1/4`: still OPEN. -/
 218  transportedTTIsotropyClosed : Bool
 219  /-- Pure-gauge continuum vanishing: still OPEN. -/
 220  transportedGaugeZeroClosed : Bool
 221  /-- Area convention match t11: closed via `slotOrbitAreaCov_t11`. -/
 222  areaConventionMatchClosed : Bool
 223  srsConvergesEH4d : Bool
 224  gapActionRecovery : Bool
 225
 226def regge4DTransportedAlgebraicCloserStatus :
 227    Regge4DTransportedAlgebraicCloserStatus where
 228  continuumSymbolBoundClosed := true
 229  quadraticHomogeneityClosed := true
 230  t11M2TendstoClosed := true
 231  oneOrbitDecoyClosed := true
 232  transportedTTIsotropyClosed := false
 233  transportedGaugeZeroClosed := false
 234  areaConventionMatchClosed := true
 235  srsConvergesEH4d := false
 236  gapActionRecovery := false
 237
 238theorem regge4DTransportedAlgebraicCloserStatus_flags :
 239    regge4DTransportedAlgebraicCloserStatus.continuumSymbolBoundClosed =
 240        true ∧
 241      regge4DTransportedAlgebraicCloserStatus.quadraticHomogeneityClosed =
 242        true ∧
 243        regge4DTransportedAlgebraicCloserStatus.t11M2TendstoClosed = true ∧
 244          regge4DTransportedAlgebraicCloserStatus.oneOrbitDecoyClosed =
 245            true ∧
 246            regge4DTransportedAlgebraicCloserStatus.transportedTTIsotropyClosed =
 247              false ∧
 248              regge4DTransportedAlgebraicCloserStatus.transportedGaugeZeroClosed =
 249                false ∧
 250                regge4DTransportedAlgebraicCloserStatus.areaConventionMatchClosed =
 251                  true ∧
 252                  regge4DTransportedAlgebraicCloserStatus.srsConvergesEH4d =
 253                    false ∧
 254                    regge4DTransportedAlgebraicCloserStatus.gapActionRecovery =
 255                      false := by
 256  decide
 257
 258/-- Honesty: banked (1,1) identities do not inhabit continuum EH Tendsto,
 259and the ledger flag stays false. -/
 260theorem banked_does_not_inhabit_eh_or_flip_gap :
 261    regge4DTransportedAlgebraicCloserStatus.transportedTTIsotropyClosed =
 262        false ∧
 263      regge4DTransportedAlgebraicCloserStatus.gapActionRecovery = false ∧
 264        oneOrbitRayNormalizedCoeff axisTTPlus ≠
 265          einsteinHilbertTTCoefficient4D :=
 266  ⟨rfl, rfl, oneOrbit_ray_normalized_ne_eh_coefficient⟩
 267
 268end
 269
 270end Regge4DTransportedAlgebraicCloser
 271end Analysis
 272end Gravity
 273end IndisputableMonolith
 274