latticeSpacing
plain-language theorem explainer
latticeSpacing defines the discrete site spacing a as the ratio L/N for a box of side L containing N sites. Researchers bridging Recognition Science's J-cost lattice to continuum GR would cite it when establishing the N to infinity limit that recovers the Einstein tensor. The declaration is a direct arithmetic definition with no lemmas or tactics required.
Claim. The lattice spacing $a$ is defined by $a = L/N$, where $L$ is the side length of the box and $N$ is the number of lattice sites.
background
The DiscreteBridge module maps the J-cost lattice of Recognition Science to continuum curvature via quadratic defects, lattice Laplacian, Ricci scalar, and Einstein tensor. Tier 1 results include the flat Minkowski limit, spatial metric from J-cost, Laplacian convergence at O(a²), coupling κ = 8φ⁵, and D = 3 from the forcing chain T8. This definition supplies the elementary length scale a = L/N used throughout the bridge.
proof idea
Direct definition: latticeSpacing L N is set equal to the quotient L divided by N. No lemmas from upstream results are applied; the declaration serves as the base for the sibling theorems latticeSpacing_pos and latticeSpacing_tendsto_zero.
why it matters
The definition underpins latticeSpacing_pos and latticeSpacing_tendsto_zero, which establish the vanishing spacing needed to recover the Einstein field equations from discrete J-cost. It fills the basic length-scale role in the proved Tier 1 bridge from ContinuumManifoldEmergence. The module packages the remaining nonlinear Regge convergence as the explicit ReggeConvergenceHypothesis rather than an axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.