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 yield Laplacians and open the continuum limit. Gravity and lattice-convergence authors cite this module as the discrete-to-continuous bridge. The development expands J about equilibrium, defines lattice fields and neighbor costs, and identifies the resulting discrete Laplacian.

claimFor $x$ near $1$, $J(x)=\frac12(x+x^{-1})-1$ admits $J(e^t)=\cosh t-1=\frac12 t^2+O(t^4)$. On a lattice field $\phi$, neighbor costs induce a discrete Laplacian $\Delta\phi$ whose continuum limit is $\nabla^2$.

background

Recognition Science starts from the cost $J(x)=\frac12(x+x^{-1})-1$, equivalently $J(e^t)=\cosh t-1$, unique by T5 and strictly convex on $\mathbb{R}_+$ (Cost.Convexity). DiscretenessForcing records that this bowl forces discrete structure: the unique minimum sits at $x=1$ ($t=0$).

This module works in the small-perturbation regime around that minimum. It introduces a quadratic cost that approximates $J$ in log coordinates with vanishing relative error, lattice fields with shift operators, neighbor costs, and the lattice Laplacian (with linearity lemmas: constants to zero, additivity, scalar homogeneity). Dimension forcing ($D=3$) and the discrete ledger skeleton sit upstream as ambient geometry.

The local setting is foundation-layer operator extraction: turn cost geometry into continuum operators before gravity modules consume them.

proof idea

The module is an expansion-plus-operator chain, not a single theorem. First expand $J\circ\exp$ about zero to extract the quadratic leading term and control the remainder (relative error vanishes as the perturbation tends to zero). Package that quadratic form as an explicit cost on lattice fields. Neighbor costs between shifted sites assemble into a discrete Laplacian; algebraic lemmas record that it annihilates constants and is linear. Continuum identification is left for downstream use: quadratic lattice costs give Laplacians, which converge to $\nabla^2$.

why it matters in Recognition Science

This is the bridge named in ContinuumManifoldEmergence: J-cost lattice to quadratic cost to Laplacian to $\nabla^2$, then Lorentzian interval, Minkowski flat limit, curved metric from defect, and Einstein equations. LatticeConvergence extends the 1D continuum-limit second-order result here to the full $D=3$ product lattice by summing independent 1D Laplacians. CubicReggeProof and CubicReggeConvergence replace the general CMS axiom with direct RS-lattice arguments that rest on this quadratic/Laplacian identification. ReggeConvergence and UnifiedLatticeManifoldCorrespondence package the same limit into Einstein-Hilbert and EFE convergence. Without the small-perturbation quadratic bridge, the discrete ledger never produces continuum geometry.

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)