Pith. sign in
module module high

IndisputableMonolith.Gravity.CubicReggeConvergence

show as:
view Lean formalization →

Defines the RS J-cost action on the cubic lattice Z³ and packages weak-field O(a²) convergence of that action to the continuum Dirichlet energy. Gravity and continuum-limit workers cite it when specializing Regge convergence to the regular cubic case. The module supplies lattice/continuum actions, error estimates, UV cutoffs, and cubic shape-quality hypotheses consumed by the cubic-lattice limit theorem.

claimOn the cubic lattice $\mathbb{Z}^3$ with spacing $a$, the RS lattice action of a scalar field $\varepsilon$ is $S_{\mathrm{RS}}(\varepsilon,a)=a^3\sum_x\sum_{\mu=1}^3 J\bigl(e^{\varepsilon(x+a\hat{e}_\mu)-\varepsilon(x)}\bigr)$. It expands to the discrete Dirichlet energy $\frac{a^3}{2}\sum_x|\nabla_a\varepsilon|^2$ and, under weak-field cubic conditions, converges to $\frac12\int|\nabla\varepsilon|^2\,d^3x$ at order $O(a^2)$.

background

Recognition Science gravity is built from the J-cost $J(x)=(x+x^{-1})/2-1$ on discrete edges. ContinuumLimit shows that discrete J-cost dynamics on $\mathbb{Z}^3$ produce, in the long-wavelength limit, second-order continuum equations matching Klein-Gordon structure. ReggeCalculus formalizes the full nonlinear Regge framework on the RS lattice; ReggeConvergence and NonlinearConvergence record the lattice-to-Einstein-Hilbert programme and the CMS-style convergence inputs (with the documented correction that CMS gives weak curvature-measure convergence, not a plain action estimate).

This module specializes to the cubic mesh and the weak-field scalar regime. It introduces the RS lattice action $S_{\mathrm{RS}}(\varepsilon,a)$ and its continuum counterpart, UV cutoffs, $\varphi$-exponential growth controls from GrowthBounds, and shape-quality hypotheses that keep the cubic lattice regular enough for an $O(a^2)$ comparison.

proof idea

Not a single theorem: a definition-and-estimate package. It defines the cubic RS lattice action and continuum action, then records quartic remainder control and weak-field error estimates under named cubic conditions. A weak-field convergence structure bundles those hypotheses with shape quality and an explicit convergence bound. UV-cutoff positivity and $\varphi$-exponential growth supply the analytic side conditions inherited from GrowthBounds and ContinuumLimit. Downstream ReggeCubicLatticeLimit consumes the package to isolate the plain $O(a^2)$ cubic case from the weaker general CMS statement.

why it matters in Recognition Science

General Regge convergence yields a weak curvature-measure limit, not a plain $O(a^2)$ action estimate. Downstream ReggeCubicLatticeLimit states that the $O(a^2)$ claim belongs to the regular weak-field cubic-lattice case and imports this module to isolate that special case for the canonical second-order Regge action. Within the RS gravity chain this pins continuum recovery of the J-cost action on $\mathbb{Z}^3$ (the spatial lattice forced by T8, $D=3$) to the Dirichlet energy that seeds Einstein-Hilbert recovery in the weak field. It sits between ContinuumLimit / ReggeCalculus and the cubic-lattice limit theorem.

scope and limits

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (15)