Pith. sign in
module module moderate

IndisputableMonolith.Gravity.LatticeConvergence

show as:
view Lean formalization →

Establishes that the discrete Laplacian of J-cost dynamics on the cubic lattice ℤ³ converges, at second order, to the continuum Laplacian as the lattice spacing vanishes. Gravity and continuum-limit arguments cite it when replacing abstract Regge axioms by an RS-native lattice calculation. The argument factors the 3D operator into three 1D second differences, scales by the mesh, and reads off the O(h²) remainder.

claimOn the cubic lattice $\mathbb{Z}^3$ with spacing $h>0$, the scaled discrete Laplacian of a smooth field $f$ equals $\Delta f + O(h^2)$ pointwise. In particular, neighbor differences of the J-cost reproduce the continuum second-derivative structure forced by $D=3$ spatial dimensions.

background

Recognition Science works from discrete J-cost dynamics on a lattice and must recover smooth field equations in the long-wavelength limit. The companion continuum-limit development (F-014) states that discrete J-cost dynamics on $\mathbb{Z}^3$ produce a second-order diffusion equation whose structure matches the Klein-Gordon equation. This module supplies the concrete 3D lattice calculus behind that claim.

Spatial dimension $D=3$ is taken from the forcing chain (T8). A lattice field is a real-valued map on $\mathbb{Z}^3$. The discrete Laplacian is the sum of three axial second differences; after mesh scaling it is the natural discrete stand-in for $\Delta$. Neighbor increments of the J-cost $J(x)=(x+x^{-1})/2-1$ are controlled so that the discrete interaction linearizes to this Laplacian at leading order.

Constants enter only through the RS unit system imported from the constants module; the local analysis is pure finite-difference calculus on the cubic lattice.

proof idea

The module is a short development, not a single theorem. It fixes $D=3$, defines 3D lattice fields, and writes the discrete Laplacian as the sum of three 1D second differences along the coordinate axes. A scaled operator multiplies by the appropriate power of the mesh $h$. Sign and normalization lemmas pin the continuum limit. Taylor expansion of a smooth test field then yields pointwise convergence of the scaled lattice Laplacian to $\Delta f$ with an explicit $O(h^2)$ remainder (second-order consistency). A final lemma transfers the same expansion to J-cost neighbor increments. A small certificate packages the convergence statement for downstream import.

why it matters in Recognition Science

Cubic Regge convergence imports this module to replace the Cheeger–Müller–Schrader axiom by a direct proof for J-cost interactions on $\mathbb{Z}^D$. Downstream documentation states that a direct proof suffices because the RS case is the cubic lattice with J-cost weights, not an arbitrary simplicial complex. Without second-order lattice consistency, the discrete curvature/action could not be identified with the continuum Einstein–Hilbert (or diffusion/KG) structure in the continuum limit. The development therefore sits between the continuum-limit foundation (F-014) and the gravity-side Regge argument, and it uses the forced $D=3$ from the T0–T8 chain rather than leaving dimension free.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)