IndisputableMonolith.Gravity.Analysis.Regge4DTorusContinuumLimit

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   3import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D
   5import IndisputableMonolith.Gravity.Analysis.QuadratureLimit
   6
   7/-!
   8# 4D torus continuum limit: action↔symbol dictionary
   9
  10Finite periodic Freudenthal action sequence on side `N = j+3`, with
  11`N^4` sites and density weight `N^{-4}` (frozen against the wrong-power
  12decoy in the preflight).
  13
  14Parallel to the closed 3D path
  15`ReggeTTBlochAssembly` → `ReggeTTContinuumLimit`:
  16
  17* 3D: `ttSecondDifference = (2/N³)·S''` and cell-sum `cos·cos → N³/2`
  18  cancel as `(2/N³)·(N³/2) = 1`, so `canonicalFiniteH` equals the raw
  19  cosine fold.
  20* 4D: same bookkeeping with `N^4` sites:
  21  `(2/N⁴)·(N⁴/2) = 1`, so `canonicalFiniteH4D` equals the
  22  distinct-hinge fold `blochFoldAllDistinctHinge` once Schläfli elevation
  23  and the 4D cell-sum identity are closed.
  24
  25## Status
  26
  27* THEOREM: product mesh cardinality / density weight identities; decoy
  28  discrimination against `N^{-2}`; algebraic cell-sum cancellation
  29  `(2/N⁴)·(N⁴/2) = 1`; surviving dictionary factor equals `1`.
  30* DEFINITION: `canonicalFiniteH4D` remains the legacy distinct-hinge fold
  31  for density-dictionary bookkeeping; continuum Tendsto
  32  (`Regge4DContinuumSymbolIs`) binds to `finiteExactMidpointBlochSymbol`
  33  (Option-C midpoint trig-poly mesh sequence).
  34* OPEN (named, non-tautological): 4D cosine cell-sum identity; residual
  35  star-member offsets for non-`t11`/`t12` orbits on the legacy fold.
  36* Does **not** flip `gap_action_recovery`.
  37-/
  38
  39namespace IndisputableMonolith
  40namespace Gravity
  41namespace Analysis
  42namespace Regge4DTorusContinuumLimit
  43
  44open BigOperators Filter Topology
  45open Regge4DContinuumPreflight
  46open ReggeBlochTransportedAllOrbit4D
  47open ReggeBlochAllOrbitSymbol4D
  48
  49noncomputable section
  50
  51/-- Local alias: preflight `Mat4` (avoids clash with transported abbrev). -/
  52abbrev Mat4 := Regge4DContinuumPreflight.Mat4
  53
  54/-! ## §1. Mesh cardinality and density weight -/
  55
  56/-- Number of sites on the side-`N` 4-torus. -/
  57def torusSiteCount (N : ℕ) : ℕ := N ^ 4
  58
  59theorem torusSiteCount_eq (N : ℕ) : torusSiteCount N = N * N * N * N := by
  60  unfold torusSiteCount
  61  ring
  62
  63/-- Density weight for the action average on the 4-torus. -/
  64def torusDensityWeight (N : ℕ) : ℝ := (N : ℝ)⁻¹ ^ 4
  65
  66theorem torusDensityWeight_eq_correct (N : ℕ) :
  67    torusDensityWeight N = correctTorusDensityWeight N := rfl
  68
  69theorem torusDensityWeight_ne_wrong {N : ℕ} (hN : 2 ≤ N) :
  70    torusDensityWeight N ≠ wrongMeshPowerWeight N := by
  71  rw [torusDensityWeight_eq_correct]
  72  exact (decoy_wrong_mesh_power hN).symm
  73
  74/-- Continuum family side. -/
  75def familySide (j : ℕ) : ℕ := torusSide j
  76
  77/-- Integer mode as a real direction (unnormalized); the continuum family
  78scales by `2π/N` separately via `momentumNormSq`. -/
  79def intModeDir (m : IntMode4) : Fin 4 → ℝ :=
  80  fun i => (m i : ℝ)
  81
  82/-! ## §2. Action↔symbol dictionary (3D parallel) -/
  83
  84/-- Second-difference bookkeeping factor in the C10 / 3D conventions:
  85the finite symbol is `(2 / N^d) · S''`, not bare `S''`. Dimension-
  86independent; here `d = 4`. -/
  87def secondDifferenceBookkeepingFactor4D : ℝ := 2
  88
  89/-- Density-normalized second-difference prefactor `(2 / N⁴)`. -/
  90def ttSecondDifferenceDensityWeight (N : ℕ) : ℝ :=
  91  secondDifferenceBookkeepingFactor4D / (N : ℝ) ^ (4 : ℕ)
  92
  93theorem ttSecondDifferenceDensityWeight_eq (N : ℕ) :
  94    ttSecondDifferenceDensityWeight N =
  95      (2 : ℝ) / (N : ℝ) ^ (4 : ℕ) := by
  96  unfold ttSecondDifferenceDensityWeight secondDifferenceBookkeepingFactor4D
  97  ring
  98
  99/-- Classical Bloch cell-sum factor for `∑_x cos(θ+α) cos(θ+β)` under
 100non-aliasing of `2m`: `N^d / 2`.  Here `d = 4`.  The full 4D cell-sum
 101theorem (analog of `BlochCellSum.cellSum_cos_mul_cos`) is OPEN below;
 102this records the forced scalar that enters the cancellation. -/
 103def cellSumCosMulCosFactor (N : ℕ) : ℝ :=
 104  (N : ℝ) ^ (4 : ℕ) / 2
 105
 106/-- HEADLINE dictionary identity (algebraic, THEOREM): the bookkeeping
 107factor cancels the cell-sum cosine average, exactly as in 3D
 108`(2/N³)·(N³/2) = 1`. -/
 109theorem density_cellSum_cancellation (N : ℕ) [NeZero N] :
 110    ttSecondDifferenceDensityWeight N * cellSumCosMulCosFactor N = 1 := by
 111  have hNcast : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
 112  have hNpow : (N : ℝ) ^ (4 : ℕ) ≠ 0 := by positivity
 113  unfold ttSecondDifferenceDensityWeight cellSumCosMulCosFactor
 114    secondDifferenceBookkeepingFactor4D
 115  field_simp [hNcast, hNpow]
 116
 117/-- Surviving dictionary factor after cell-sum cancellation: `1`.
 118Equals the 3D survivor `(2/N³)·(N³/2) = 1`.  This is not a fitted
 119lattice rescale; it is the forced product of the second-difference
 120bookkeeping factor and the cosine cell-sum average. -/
 121def survivingDictionaryFactor4D : ℝ := 1
 122
 123theorem survivingDictionaryFactor4D_eq_one :
 124    survivingDictionaryFactor4D = 1 := rfl
 125
 126theorem survivingDictionaryFactor4D_eq_cancellation (N : ℕ) [NeZero N] :
 127    survivingDictionaryFactor4D =
 128      ttSecondDifferenceDensityWeight N * cellSumCosMulCosFactor N := by
 129  rw [survivingDictionaryFactor4D_eq_one, density_cellSum_cancellation]
 130
 131/-! ## §3. Canonical finite Hessian (distinct-hinge) -/
 132
 133/-- Legacy finite-`N` 4D Hessian: distinct-hinge fold (density-dictionary
 134scaffold).  Continuum Props bind to `finiteExactReggeSymbol`, not this. -/
 135def canonicalFiniteH4D (N : ℕ) (m : IntMode4) (E : Mat4) : ℝ :=
 136  blochFoldAllDistinctHinge E (realMode N m)
 137
 138theorem canonicalFiniteH4D_eq (N : ℕ) (m : IntMode4) (E : Mat4) :
 139    canonicalFiniteH4D N m E =
 140      blochFoldAllDistinctHinge E (realMode N m) :=
 141  rfl
 142
 143theorem canonicalFiniteH4D_eq_finiteTransportedSymbol (j : ℕ)
 144    (m : IntMode4) (E : Mat4) :
 145    canonicalFiniteH4D (familySide j) m E =
 146      finiteTransportedSymbol j m E := by
 147  unfold canonicalFiniteH4D finiteTransportedSymbol familySide
 148  rfl
 149
 150theorem canonicalFiniteH4D_smul (c : ℝ) (N : ℕ) (m : IntMode4) (E : Mat4) :
 151    canonicalFiniteH4D N m (c • E) =
 152      c ^ 2 * canonicalFiniteH4D N m E := by
 153  unfold canonicalFiniteH4D
 154  exact blochFoldAllDistinctHinge_smul c E (realMode N m)
 155
 156/-- Upgraded finite torus Hessian: distinct-hinge fold (replaces the
 157previous m²-poly placeholder that was tautological against itself). -/
 158def finiteTorusHessian (N : ℕ) (m : IntMode4) (E : Mat4) : ℝ :=
 159  canonicalFiniteH4D N m E
 160
 161theorem finiteTorusHessian_eq_canonical (N : ℕ) (m : IntMode4) (E : Mat4) :
 162    finiteTorusHessian N m E = canonicalFiniteH4D N m E :=
 163  rfl
 164
 165theorem finiteTorusHessian_eq_finiteTransportedSymbol (j : ℕ)
 166    (m : IntMode4) (E : Mat4) :
 167    finiteTorusHessian (familySide j) m E =
 168      finiteTransportedSymbol j m E :=
 169  canonicalFiniteH4D_eq_finiteTransportedSymbol j m E
 170
 171/-! ## §4. OPEN elevation / cell-sum Props (non-tautological) -/
 172
 173/-- OPEN: 4D analog of `BlochCellSum.cellSum_cos_mul_cos`.
 174States that the forced cell-sum scalar under non-aliasing is exactly
 175`cellSumCosMulCosFactor N = N⁴/2`, and that this scalar is the one that
 176cancels `ttSecondDifferenceDensityWeight`.  The full phase-sum over
 177`(Fin N)⁴` with explicit `theta` is the remaining Lean work; this Prop
 178records the scalar obligation without a `: True` shell. -/
 179def BlochCellSum4DCosMulCosOpen : Prop :=
 180  ∀ (N : ℕ) [NeZero N],
 181    cellSumCosMulCosFactor N = (N : ℝ) ^ (4 : ℕ) / 2 ∧
 182      ttSecondDifferenceDensityWeight N * cellSumCosMulCosFactor N = 1
 183
 184/-- THEOREM: the scalar half of the 4D cell-sum OPEN Prop holds
 185(definition + cancellation).  The phase-sum half remains future work in
 186a dedicated `BlochCellSum4D` module. -/
 187theorem BlochCellSum4DCosMulCosOpen_scalar_holds :
 188    BlochCellSum4DCosMulCosOpen := by
 189  intro N hN
 190  exact ⟨rfl, density_cellSum_cancellation (N := N)⟩
 191
 192/-- Independent nonlinear-action second variation placeholder type.
 193Consumers of the Schläfli elevation supply a concrete `S''` sequence;
 194until then the elevation Prop quantifies over all candidates. -/
 195def NonlinearSecondVariation4D := ℕ → IntMode4 → Mat4 → ℝ
 196
 197/-- OPEN: there exists an independent nonlinear flat second variation
 198`S''` (from Schläfli elevation of the edge-length Regge action) such that
 199for every non-aliased side,
 200`(2/N⁴) · S''(N,m,E) = canonicalFiniteH4D N m E`.
 201
 202Falsifier: inhabiting this by setting
 203`S'' := cellSumCosMulCosFactor N * canonicalFiniteH4D`
 204without a Schläfli derivation from the nonlinear action
 205(`Regge4DFlatSecondVariation.Regge4DSchlafliSecondVariation`). -/
 206def SchlafliElevationToDistinctHingeOpen : Prop :=
 207  ∃ S'' : NonlinearSecondVariation4D,
 208    ∀ (N : ℕ) [NeZero N] (m : IntMode4) (E : Mat4),
 209      (∃ i : Fin 4, ¬ (N : ℤ) ∣ 2 * m i) →
 210        ttSecondDifferenceDensityWeight N * S'' N m E =
 211          canonicalFiniteH4D N m E
 212
 213/-- Cleaner OPEN name used by status flags: Schläfli elevation not closed. -/
 214def CanonicalFiniteH4DEqDistinctHingeFoldOpen : Prop :=
 215  SchlafliElevationToDistinctHingeOpen
 216
 217/-- THEOREM (dictionary reduction): once an independent `S''` equals
 218`cellSumCosMulCosFactor N * H`, cancellation forces
 219`(2/N⁴)·S'' = H`.  This is the 3D cancellation step in isolation. -/
 220theorem dictionary_identifies_fold_of_cellSum_scaled
 221    (N : ℕ) [NeZero N] (m : IntMode4) (E : Mat4)
 222    (S'' : ℝ)
 223    (hS : S'' = cellSumCosMulCosFactor N * canonicalFiniteH4D N m E) :
 224    ttSecondDifferenceDensityWeight N * S'' = canonicalFiniteH4D N m E := by
 225  rw [hS]
 226  have hcancel := density_cellSum_cancellation (N := N)
 227  calc
 228    ttSecondDifferenceDensityWeight N *
 229        (cellSumCosMulCosFactor N * canonicalFiniteH4D N m E)
 230        = (ttSecondDifferenceDensityWeight N * cellSumCosMulCosFactor N) *
 231            canonicalFiniteH4D N m E := by ring
 232    _ = (1 : ℝ) * canonicalFiniteH4D N m E := by rw [hcancel]
 233    _ = canonicalFiniteH4D N m E := by ring
 234
 235/-- OPEN (interface name retained): finite torus Hessian equals the
 236distinct-hinge fold.  Holds definitionally for the upgraded Hessian. -/
 237def FiniteTorusHessianEqAllOrbitFold : Prop :=
 238  ∀ (j : ℕ) (m : IntMode4) (E : Mat4),
 239    m ≠ 0 →
 240      finiteTorusHessian (familySide j) m E =
 241        blochFoldAllDistinctHinge E (realMode (familySide j) m)
 242
 243theorem FiniteTorusHessianEqAllOrbitFold_holds :
 244    FiniteTorusHessianEqAllOrbitFold := by
 245  intro j m E _hm
 246  unfold finiteTorusHessian canonicalFiniteH4D
 247  rfl
 248
 249/-! ## §5. Continuum Tendsto wiring -/
 250
 251/-- Continuum limit for the normalized Option-C midpoint Bloch mesh
 252symbol along the torus family (matches `Regge4DContinuumSymbolIs`). -/
 253def TorusNormalizedTendsto (m : IntMode4) (E : Mat4) (Λ : ℝ) : Prop :=
 254  Filter.Tendsto
 255    (fun j : ℕ =>
 256      finiteExactMidpointBlochSymbol j m E /
 257        momentumNormSq (familySide j) m)
 258    Filter.atTop (nhds Λ)
 259
 260theorem torusNormalized_eq_continuumSymbol (m : IntMode4) (E : Mat4) (Λ : ℝ) :
 261    TorusNormalizedTendsto m E Λ ↔ Regge4DContinuumSymbolIs m E Λ :=
 262  Iff.rfl
 263
 264/-- Legacy exact-action fold Tendsto (not the Option-C continuum binder). -/
 265def TorusNormalizedTendstoExactAction (m : IntMode4) (E : Mat4) (Λ : ℝ) :
 266    Prop :=
 267  Filter.Tendsto
 268    (fun j : ℕ =>
 269      finiteExactReggeSymbol j m E /
 270        momentumNormSq (familySide j) m)
 271    Filter.atTop (nhds Λ)
 272
 273/-- Alternate geometric binder with discrete bookkeeping ×2 in the mesh
 274sequence (not a constant face). -/
 275def TorusNormalizedTendstoDiscreteBookkeeping
 276    (m : IntMode4) (E : Mat4) (Λ : ℝ) : Prop :=
 277  Regge4DDiscreteBookkeepingContinuumSymbolIs m E Λ
 278
 279/-- Legacy fold Tendsto (not the continuum binder after `H_fold`). -/
 280def TorusNormalizedTendstoLegacyFold (m : IntMode4) (E : Mat4) (Λ : ℝ) :
 281    Prop :=
 282  Filter.Tendsto
 283    (fun j : ℕ =>
 284      finiteTorusHessian (familySide j) m E /
 285        momentumNormSq (familySide j) m)
 286    Filter.atTop (nhds Λ)
 287
 288/-- Axis arithmetic (MEASURED externally; Lean decide in M2Eval):
 289distinct-hinge raw m² on `axisTTPlus`/`symbolDir` is `-1/4`; after
 290`/|dir|² = 2` and Frobenius pin `1/2` the continuum-facing coefficient is
 291`-1/16`.  Frozen EH target is `-1/4`.  The density dictionary survivor
 292is `1`, so it does **not** close the residual factor `4`.  EH Tendsto
 293therefore remains uninhabited here (no fitted rescale). -/
 294def DistinctHingePinnedMomentVsEH : Prop :=
 295  (-1 / 16 : ℝ) ≠ einsteinHilbertTTCoefficient4D
 296
 297theorem distinctHinge_pinned_ne_eh :
 298    DistinctHingePinnedMomentVsEH := by
 299  unfold DistinctHingePinnedMomentVsEH
 300  rw [einsteinHilbertTTCoefficient4D_eq]
 301  norm_num
 302
 303/-- OPEN: C² / smooth density extension from finite Fourier sums.
 304Named as an equality obligation, not a `: True` shell. -/
 305def TorusC2DensityExtensionOpen : Prop :=
 306  ∀ (m : IntMode4) (E : Mat4),
 307    m ≠ 0 →
 308      IsTTPolarization4D (fun i => (m i : ℝ)) E →
 309        ∃ Λ : ℝ, TorusNormalizedTendsto m E Λ
 310
 311structure Regge4DTorusContinuumLimitStatus where
 312  densityWeightFrozen : Bool
 313  dictionaryCancellationClosed : Bool
 314  survivingFactorIsOne : Bool
 315  finiteHessianWiredToDistinctHinge : Bool
 316  schlafliElevationOpen : Bool
 317  cellSumPhaseIdentityOpen : Bool
 318  ehTendstoInhabited : Bool
 319  gapActionRecovery : Bool
 320
 321def regge4DTorusContinuumLimitStatus : Regge4DTorusContinuumLimitStatus where
 322  densityWeightFrozen := true
 323  dictionaryCancellationClosed := true
 324  survivingFactorIsOne := true
 325  finiteHessianWiredToDistinctHinge := true
 326  schlafliElevationOpen := true
 327  cellSumPhaseIdentityOpen := true
 328  ehTendstoInhabited := false
 329  gapActionRecovery := false
 330
 331theorem regge4DTorusContinuumLimitStatus_flags :
 332    regge4DTorusContinuumLimitStatus.densityWeightFrozen = true ∧
 333      regge4DTorusContinuumLimitStatus.dictionaryCancellationClosed = true ∧
 334        regge4DTorusContinuumLimitStatus.survivingFactorIsOne = true ∧
 335          regge4DTorusContinuumLimitStatus.finiteHessianWiredToDistinctHinge =
 336            true ∧
 337            regge4DTorusContinuumLimitStatus.schlafliElevationOpen = true ∧
 338              regge4DTorusContinuumLimitStatus.cellSumPhaseIdentityOpen =
 339                true ∧
 340                regge4DTorusContinuumLimitStatus.ehTendstoInhabited = false ∧
 341                  regge4DTorusContinuumLimitStatus.gapActionRecovery =
 342                    false := by
 343  decide
 344
 345/-- Honesty: the dictionary alone does not inhabit
 346`Regge4DContinuumEHTarget` and does not flip the ledger flag. -/
 347theorem dictionary_does_not_inhabit_eh_or_flip_gap :
 348    survivingDictionaryFactor4D = 1 ∧
 349      DistinctHingePinnedMomentVsEH ∧
 350        regge4DTorusContinuumLimitStatus.ehTendstoInhabited = false ∧
 351          regge4DTorusContinuumLimitStatus.gapActionRecovery = false :=
 352  ⟨rfl, distinctHinge_pinned_ne_eh, rfl, rfl⟩
 353
 354end
 355
 356end Regge4DTorusContinuumLimit
 357end Analysis
 358end Gravity
 359end IndisputableMonolith
 360