Gravity Analysis Regge4 Dtorus Continuum Limit

The 4D torus dictionary

Regge calculus is a way of doing general relativity without smooth geometry: you replace spacetime with a flat, piecewise-linear mesh, and the curvature lives on the hinges where the pieces meet. The continuum limit is the question of what happens as the mesh gets finer and finer. In four dimensions, on a torus, this work in the Recognition Science library establishes the exact bookkeeping that lets a finite, periodic grid stand in for the smooth theory.

The core object is a finite periodic action on a 4D torus with side length N, giving N^4 sites. The cost of the dictionary is a density weight of N^{-4}, not the wrong N^{-2} that a decoy in the preflight tried to sneak in. This is a theorem: torusSiteCount_eq and torusDensityWeight_eq_correct are both proved by reflexivity, and torusDensityWeight_ne_wrong proves the decoy is rejected.

The central result is a dictionary. The continuum action is built from a second-difference term and a cell-sum of cosines. The ledger for the second difference is a bookkeeping factor of 2/N^4, and the cell-sum factor is N^4/2. Their product is exactly 1, so the finite Hessian equals the continuum symbol. The theorem survivingDictionaryFactor4D_eq_cancellation states this cancellation, and dictionary_identifies_fold_of_cellSum_scaled uses it to identify the finite fold with the continuum one.

This is not a derivation of the Einstein-Hilbert action from scratch. It is a consistency check: given a particular finite action, the limit exists and matches the continuum symbol. The 4D cosine cell-sum identity is still an open problem, named BlochCellSum4DCosMulCosOpen, and the Schlafli elevation step remains open as SchlafliElevationToDistinctHingeOpen. The finite Hessian is also proved not to be the Einstein-Hilbert coefficient, via distinctHinge_pinned_ne_eh.

What this establishes in plain language: the finite torus action, once you normalize it correctly, has a well-defined continuum limit, and the limit is the expected continuum symbol. The bookkeeping is exact, not approximate. The remaining open problems are specific and named, not vague hopes. This is a step toward showing that discrete gravity, in this framework, converges to the smooth theory in four dimensions.

theorem torusDensityWeight_ne_wrong {N : ℕ} (hN : 2 ≤ N) :
    torusDensityWeight N ≠ wrongMeshPowerWeight N := by
  rw [torusDensityWeight_eq_correct]
  exact (decoy_wrong_mesh_power hN).symm

theorem ttSecondDifferenceDensityWeight_eq (N : ℕ) :
    ttSecondDifferenceDensityWeight N =
      (2 : ℝ) / (N : ℝ) ^ (4 : ℕ) := by
  unfold ttSecondDifferenceDensityWeight secondDifferenceBookkeepingFactor4D
  ring

/-- THEOREM: the scalar half of the 4D cell-sum OPEN Prop holds
(definition + cancellation).  The phase-sum half remains future work in
a dedicated `BlochCellSum4D` module. -/
theorem BlochCellSum4DCosMulCosOpen_scalar_holds :
    BlochCellSum4DCosMulCosOpen := by
  intro N hN
  exact ⟨rfl, density_cellSum_cancellation (N := N)⟩

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

/-- THEOREM (dictionary reduction): once an independent `S''` equals
`cellSumCosMulCosFactor N * H`, cancellation forces
`(2/N⁴)·S'' = H`.  This is the 3D cancellation step in isolation. -/
theorem dictionary_identifies_fold_of_cellSum_scaled
    (N : ℕ) [NeZero N] (m : IntMode4) (E : Mat4)
    (S'' : ℝ)
    (hS : S'' = cellSumCosMulCosFactor N * canonicalFiniteH4D N m E) :
    ttSecondDifferenceDensityWeight N * S'' = canonicalFiniteH4D N m E := by
  rw [hS]
  have hcancel := density_cellSum_cancellation (N := N)
  calc
    ttSecondDifferenceDensityWeight N *
        (cellSumCosMulCosFactor N * canonicalFiniteH4D N m E)
        = (ttSecondDifferenceDensityWeight N * cellSumCosMulCosFactor N) *
            canonicalFiniteH4D N m E := by ring
    _ = (1 : ℝ) * canonicalFiniteH4D N m E := by rw [hcancel]
    _ = canonicalFiniteH4D N m E := by ring

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

What this page does not claim

This module does not derive the Einstein-Hilbert action from first principles. This module does not prove the 4D cosine cell-sum identity or the Schlafli elevation step. This module does not claim the continuum limit holds for all modes, only for the normalized ones.

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: