Pith. sign in
module module high

IndisputableMonolith.Gravity.ReggeConvergence

show as:
view Lean formalization →

In the linearized weak-field regime, the Regge action on Z^3 equals a lattice Laplacian action that converges to the continuum Einstein-Hilbert action at O(a^2). Gravity researchers bridging RS discrete curvature to continuum GR cite this for the linearized half of Axiom 1. The module chains five upstream results: J-cost quadratic expansion, Laplacian identification, continuum limit at O(a^2), Newtonian-gauge Ricci match, and linearized EH equality.

claimIn the linearized regime on $\mathbb{Z}^3$, the Regge action equals the lattice Laplacian action and converges to the continuum Einstein-Hilbert action at $O(a^2)$. Chain: $J$-cost quadratic $\cosh(\varepsilon)-1=\varepsilon^2/2+O(\varepsilon^4)$; quadratic sum $=$ lattice Laplacian; Laplacian$/a^2\to\nabla^2$ at $O(a^2)$; $\nabla^2\Phi=R$ in Newtonian gauge; Ricci-scalar action $=$ linearized EH action. This discharges Axiom 1 linearized.

background

Recognition Science gravity lives on a discrete ledger on the cubic lattice $\mathbb{Z}^3$, with edge costs from the J-cost $J(x)=\cosh(\log x)-1$ (equivalently $(x+x^{-1})/2-1$). The ContinuumLimit module shows discrete J-cost dynamics produce second-order continuum equations in the long-wavelength limit. ReggeCalculus supplies the exact nonlinear discrete curvature via deficit angles on hinges, replacing a linearized deficit ansatz. RicciTensor defines $R_{\mu\nu}$, scalar $R$, and Einstein $G_{\mu\nu}$ from the Riemann tensor, with symmetry of $G_{\mu\nu}$.

This module is the linearized interface: small perturbations about flat space, Newtonian gauge, and identification of the lattice Laplacian of the Newtonian potential with the Ricci scalar. CMS (Cheeger-Müller-Schrader) regularity conditions appear as named hypotheses for nonlinear extension; the linearized path does not need the full CMS package. Constants supplies the RS time quantum used in lattice scaling.

proof idea

The module assembles a five-step chain proved in preceding modules rather than re-deriving each step. (1) J-cost expands as $\cosh(\varepsilon)-1=\varepsilon^2/2+O(\varepsilon^4)$. (2) The quadratic piece sums to a lattice Laplacian action. (3) ContinuumLimit gives lattice Laplacian$/a^2\to\nabla^2$ at $O(a^2)$. (4) In Newtonian gauge, $\nabla^2\Phi$ equals the Ricci scalar. (5) The Ricci-scalar action is the linearized Einstein-Hilbert action.

Named objects package the assembly: linearized convergence and error estimates, cubic shape bounds (optimal on identical cubes), weak-field covers, and a ReggeConvergenceCert. Nonlinear convergence is stated under CMS-type conditions, not discharged unconditionally here.

why it matters in Recognition Science

CubicReggeConvergence and CubicReggeProof specialize the story to the RS cubic lattice: perfect shape quality ($\sigma=1$) makes CMS aspect-ratio conditions automatic, and a direct proof replaces the general CMS axiom for J-cost interactions on $\mathbb{Z}^D$. FullEFE imports the convergence package to derive the complete nonlinear sourced Einstein field equations from the RS ledger, conditional on Regge convergence axioms. UnifiedLatticeManifoldCorrespondence packages the deformed-cubic-lattice / curved-manifold correspondence: sequences of lattices whose Regge action converges to $S_{EH}[g]$ and whose equations converge to the EFE.

In the broader framework this is the gravity-side continuum bridge after T8 ($D=3$ spatial dimensions) and the eight-tick lattice structure, not a new forcing step. It closes the linearized half of Axiom 1 in the discrete-to-continuum gravity programme.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (11)