Gravity Analysis Regge4 Dtorus Continuum Limit Surviving Dictionary Factor4 D Eq

The surviving factor

In numerical work on gravity, one often approximates a smooth four-dimensional space by a fine grid or mesh. The action, a quantity whose variation gives the field equations, is then a sum over the grid's sites. As the grid spacing shrinks, this discrete sum should approach the continuum expression. A subtlety is that different ways of writing the discrete sum carry different powers of the grid size N, and these powers must cancel exactly for the limit to exist.

The declaration survivingDictionaryFactor4D_eq_cancellation is a theorem in the framework's machine-checked library of formal theorems. It states that a particular bookkeeping factor, called the surviving dictionary factor, equals the product of two other factors: the density weight, which scales as 2/N⁴, and the cell-sum factor, which scales as N⁴/2. Their product is exactly 1. The proof is a direct algebraic cancellation, shown in the formal theorem survivingDictionaryFactor4D_eq_cancellation.

This cancellation is the four-dimensional analogue of a similar result in three dimensions. In both cases, the bookkeeping factors that arise from the discrete mesh and from summing over cells cancel precisely. The consequence is that the canonical finite Hamiltonian, the discrete expression for the action, equals the raw cosine fold without any extra multiplicative constant. The dictionary, the mapping between discrete and continuum quantities, is consistent.

The theorem does not claim that the full four-dimensional continuum limit has been established. The 4D cosine cell-sum identity, a key ingredient, remains an open target. The theorem also does not claim that the discrete action recovers the Einstein-Hilbert action; in fact, a separate theorem shows the distinct-hinge moment differs from the Einstein-Hilbert coefficient. The cancellation is a necessary bookkeeping step, not a complete derivation.

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

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 canonicalFiniteH4D_eq (N : ℕ) (m : IntMode4) (E : Mat4) :
    canonicalFiniteH4D N m E =
      blochFoldAllDistinctHinge E (realMode N m) :=
  rfl

What this page does not claim

The theorem does not prove the full four-dimensional continuum limit, which depends on the open cell-sum identity. The theorem does not claim the discrete action reproduces the Einstein-Hilbert action; a separate result shows the distinct-hinge moment differs from it.

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: