Pith. sign in
module module high

IndisputableMonolith.Foundation.ContinuumLimit

show as:
view Lean formalization →

In the small-perturbation regime the Recognition J-cost is quadratic to leading order, so discrete lattice costs become continuum Laplacians. Anyone deriving continuum field equations or Regge-to-Einstein limits from the RS ledger cites this bridge. The module expands J about the identity, defines lattice fields and neighbor costs, and identifies the discrete Laplacian as the quadratic form of those costs.

claimFor $x$ near $1$, $J(x)=\frac12(x+x^{-1})-1$ expands as $J(e^t)=\cosh t-1=\frac12 t^2+O(t^4)$. On a lattice field $\phi:\mathbb{Z}^D\to\mathbb{R}$, neighbor costs induce a discrete Laplacian $\Delta\phi$ (linear, translation-invariant) that is the continuum bridge under mesh refinement.

background

Recognition Science builds continuum physics from a single cost $J$. In multiplicative coordinates $J(x)=\frac12(x+x^{-1})-1$ on $\mathbb{R}_+$; in log coordinates $J(e^t)=\cosh t-1$. Both are strictly convex with unique minimum at the identity (Cost.Convexity), which is the uniqueness input T5 and the discreteness-forcing bowl centered at zero defect.

DiscretenessForcing already shows that the cost landscape forces a discrete ledger rather than a continuum a priori. This module takes the complementary step: once the ledger exists, small defects live in the quadratic well of $J$, so the discrete energy is a lattice Dirichlet form. DimensionForcing supplies $D=3$ as the ambient lattice rank when the continuum limit is taken in physical space.

The local objects are lattice fields (maps from $\mathbb{Z}^D$ to scalars), shift operators, the discrete Laplacian built from neighbor differences, and the neighbor-cost functional whose Hessian is that Laplacian. Relative-error statements quantify how fast the quadratic model tracks full $J$ as the log-amplitude tends to zero.

proof idea

The module is a short development chain, not a single theorem. First it records the Taylor fact that $\cosh t-1$ is $\frac12 t^2$ plus higher even powers, and packages the corresponding quadratic model of $J$ on multiplicative coordinates, with a vanishing relative-error lemma as the perturbation shrinks.

It then introduces lattice fields and the $\pm$ shifts, defines the standard discrete Laplacian as a linear operator, and checks the elementary algebraic identities (kills constants, additive, homogeneous). Neighbor cost is the sum of pairwise $J$-penalties on edges; its small-amplitude expansion is identified with the quadratic form of the Laplacian. Downstream continuum arguments only need this operator calculus plus the quadratic leading term.

why it matters in Recognition Science

This is the discrete-to-continuous hinge in the foundation layer. ContinuumManifoldEmergence imports it to run the chain "J-cost lattice $\to$ quadratic cost $\to$ Laplacian $\to\nabla^2\to$ Lorentzian interval $\to$ Einstein equations from defect." LatticeConvergence extends the one-dimensional second-order continuum limit here to the full $D=3$ product lattice by summing independent one-dimensional Laplacians.

ReggeConvergence, CubicReggeProof, and CubicReggeConvergence use the same quadratic/Laplacian identification to replace a general CMS regularity axiom with an RS-specific direct proof on the cubic lattice (perfect shape quality, identical cubes). UnifiedLatticeManifoldCorrespondence packages the deformed-cubic / curved-manifold correspondence that closes the backlog gap between ledger geometry and $S_{\mathrm{EH}}[g]$.

Without the quadratic leading term, neighbor costs would not produce a second-order elliptic operator, and the continuum gravity modules would have no continuum PDE to converge to.

scope and limits

used by (6)

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

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (32)