Gravity Analysis Regge4 Dtorus Continuum Limit Regge4 Dtorus Continuum Limit Sta

The 4D torus dictionary

A discrete approximation to a physical theory on a four-dimensional torus must reproduce the smooth continuum theory as the lattice spacing shrinks. The framework's machine-checked library of formal theorems records this dictionary for a periodic Freudenthal action sequence. The finite model places N^4 sites on a torus of side N, and weights each site by N^-4, the correct density for four dimensions. The declaration regge4DTorusContinuumLimitStatus_flags is the status report for that dictionary: it states which identities are proved, which definitions are in play, and which claims remain open.

The central proved identity is a bookkeeping cancellation. The second-difference factor contributes 2/N^4, and the cell-sum of cosine products contributes N^4/2; their product is exactly 1. This mirrors the three-dimensional case, where the same cancellation holds with N^3 sites. The theorem survivingDictionaryFactor4D_eq_one proves that the surviving factor equals 1, and survivingDictionaryFactor4D_eq_cancellation shows this equals the product of the two bookkeeping factors. Other proved identities include the site count N^4, the density weight N^-4, and the rejection of the wrong N^-2 power as a decoy. The finite Hessian, the second variation of the action, is proved equal to the canonical distinct-hinge fold, and the whole normalized finite symbol is equivalent to the continuum symbol.

The declaration also names what remains open. The 4D cosine cell-sum identity, which would close the algebraic cancellation for the full fold, is not proved. Residual offsets for star members on non-t11 or t12 orbits of the legacy fold remain open. The Schläfli elevation to the distinct-hinge fold is open, and the smooth extension of the density to a C2 function is open. These are targets, not impossibilities.

What the declaration does not claim is as important as what it proves. It does not establish that the continuum limit exists for all polarizations; the open propositions TorusC2DensityExtensionOpen and SchlafliElevationToDistinctHingeOpen are precisely the missing pieces. It does not claim that the distinct-hinge fold matches the Einstein-Hilbert coefficient; in fact, the theorem distinctHinge_pinned_ne_eh proves they differ. And it does not flip the separate gap_action_recovery flag. The dictionary is a precise bookkeeping ledger, not a claim that all of four-dimensional gravity has been discretized.

theorem torusSiteCount_eq (N : ℕ) : torusSiteCount N = N * N * N * N := by
  unfold torusSiteCount
  ring

theorem torusDensityWeight_eq_correct (N : ℕ) :
    torusDensityWeight N = correctTorusDensityWeight N := rfl

theorem survivingDictionaryFactor4D_eq_cancellation (N : ℕ) [NeZero N] :
    survivingDictionaryFactor4D =
      ttSecondDifferenceDensityWeight N * cellSumCosMulCosFactor N := by
  rw [survivingDictionaryFactor4D_eq_one, density_cellSum_cancellation]

theorem survivingDictionaryFactor4D_eq_one :
    survivingDictionaryFactor4D = 1 := rfl

theorem FiniteTorusHessianEqAllOrbitFold_holds :
    FiniteTorusHessianEqAllOrbitFold := by
  intro j m E _hm
  unfold finiteTorusHessian canonicalFiniteH4D
  rfl

theorem torusNormalized_eq_continuumSymbol (m : IntMode4) (E : Mat4) (Λ : ℝ) :
    TorusNormalizedTendsto m E Λ ↔ Regge4DContinuumSymbolIs m E Λ :=
  Iff.rfl

theorem distinctHinge_pinned_ne_eh :
    DistinctHingePinnedMomentVsEH := by
  unfold DistinctHingePinnedMomentVsEH
  rw [einsteinHilbertTTCoefficient4D_eq]
  norm_num

What this page does not claim

The declaration does not prove the continuum limit exists for all polarizations. The declaration does not claim the distinct-hinge fold matches the Einstein-Hilbert coefficient; it proves they differ. The declaration does not flip the separate gap_action_recovery flag.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/Regge4DTorusContinuumLimit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: