Gravity Analysis Regge4 Dtorus Continuum Limit Finite Torus Hessian Eq All Orbit

The finite torus identity

A torus is a shape like the surface of a donut, but in four dimensions. The declaration FiniteTorusHessianEqAllOrbitFold_holds proves a precise bookkeeping identity for a discrete model of gravity on such a torus. The model divides the torus into a grid of N^4 sites, where N is the side length. The theorem states that a certain quantity, the finite torus Hessian, equals a simpler expression built from the same geometric data, for every non-zero mode and every choice of the metric field.

The proof is a definitional equality: the two expressions are the same by unfolding definitions, with no analytic work required. The theorem holds for all side lengths N in the family, all non-zero modes m, and all metric matrices E. It does not require any regularity conditions or approximations. This is a purely algebraic statement about the discrete model, verified in the machine-checked library of formal theorems.

The identity is part of a larger program to show that the discrete model converges to the continuum theory of gravity. The finite torus Hessian is the discrete analogue of the second variation of the Einstein-Hilbert action. The theorem establishes that, for the purposes of this bookkeeping, the discrete Hessian and the continuum fold agree exactly at every finite grid size. This is a necessary step before any limit can be taken.

In Recognition Science, this is a ledger fact: a discrete record of events that must balance exactly. The theorem does not claim that the continuum limit itself exists, nor that the discrete model is physically correct. It only establishes the algebraic identity between two expressions. The convergence to the continuum, and the physical interpretation, remain separate open targets.

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

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

/-- OPEN (interface name retained): finite torus Hessian equals the
distinct-hinge fold.  Holds definitionally for the upgraded Hessian. -/
def FiniteTorusHessianEqAllOrbitFold : Prop :=
  ∀ (j : ℕ) (m : IntMode4) (E : Mat4),
    m ≠ 0 →
      finiteTorusHessian (familySide j) m E =
        blochFoldAllDistinctHinge E (realMode (familySide j) m)

What this page does not claim

The continuum limit of the discrete model exists or converges to a specific value. The discrete model is a physically correct description of gravity. The identity holds for the zero mode or for modes that are not in the family. The theorem proves any statement about the actual universe, only about the formal model.

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: