lattice_laplacian
plain-language theorem explainer
Defines the standard nearest-neighbor lattice Laplacian on ℤ^D for a real-valued lattice field: sum over axes of f(x+e_k)+f(x−e_k)−2f(x). Continuum-limit and Klein–Gordon arguments in F-014 cite it as the discrete operator that quadratic J-cost produces. The body is a direct Fin-sum of the two one-step shifts.
Claim. For dimension $D\in\mathbb{N}$ and a lattice field $f:\mathbb{Z}^D\to\mathbb{R}$, the lattice Laplacian at site $x$ is $(\Delta_{\mathrm{lat}} f)(x)=\sum_{k=1}^{D}\bigl(f(x+e_k)+f(x-e_k)-2f(x)\bigr)$, where $e_k$ is the unit step along axis $k$.
background
Module F-014 (Continuum Limit) shows how discrete J-cost dynamics on the ledger lattice yield smooth field equations. The bridge is: J(exp(t))=cosh(t)−1 expands as t²/2+O(t⁴); small log-ratio perturbations therefore carry a quadratic cost; quadratic nearest-neighbor costs assemble into a discrete Laplacian; that operator continuum-limits to ∇² and feeds Klein–Gordon structure.
A lattice field is any map f:(Fin D → ℤ) → ℝ, i.e. a real value at each site of ℤ^D (typically a log-ratio perturbation). The helpers shift_plus and shift_minus translate a site by ±1 along a single axis k via Function.update. Spatial dimension D is forced to 3 elsewhere (T8/T9), but the definition is written for general D.
This object is the standard graph Laplacian of the integer lattice with nearest-neighbor edges; no continuum or J-cost content is baked into the definition itself.
proof idea
Pure definition: unfold to a Finset sum over k : Fin D of the three-point stencil f(shift_plus k x) + f(shift_minus k x) − 2·f x. No lemmas, tactics, or sorry. Downstream linearity proofs (add, smul, const) simply unfold this sum and ring/simp.
why it matters
F-014’s certificate packages four claims: quadratic leading order of J_log, CPT symmetry, vacuum, and the path quadratic cost → lattice Laplacian → continuous ∇² → Klein–Gordon. This definition is the discrete operator named in step 2–3. Immediate children prove it annihilates constants, is additive, and is homogeneous (lattice_laplacian_const/add/smul). neighbor_cost builds the full nearest-neighbor J-cost whose quadratic regime recovers this Laplacian; mass_from_curvature and the Klein–Gordon structure theorem sit further down the same chain. Gravity’s CubicReggeConvergenceCert and expansion_convergence_ratio also consume it when matching discrete curvature expansions. Framework landmarks: T8 forces D=3; the eight-tick and φ-ladder enter only later via mass, not here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.