lattice_laplacian_const
plain-language theorem explainer
The lattice Laplacian of any constant real field vanishes at every site of ℤ^D. Continuum-limit and discrete-PDE arguments cite this as the kernel fact for the nearest-neighbor operator. The proof unfolds the sum over ±e_k shifts and cancels by elementary algebra.
Claim. For any dimension $D \in \mathbb{N}$, constant $c \in \mathbb{R}$, and lattice point $x \in \mathbb{Z}^D$, if $f \equiv c$ then $(\Delta_{\mathrm{lat}} f)(x) = 0$, where $(\Delta_{\mathrm{lat}} f)(x) = \sum_{k=1}^{D}\bigl(f(x+e_k)+f(x-e_k)-2f(x)\bigr)$.
background
Module F-014 (Continuum Limit) shows how discrete J-cost dynamics on the ledger lattice produce smooth continuum PDEs. The bridge is: J(exp(t)) = cosh(t) − 1 has leading Taylor term t²/2; quadratic costs on a lattice yield a discrete Laplacian; that operator scales to ∇² and thence to Klein–Gordon structure.
The lattice Laplacian is the standard nearest-neighbor operator on ℤ^D: (Δ_lat f)(x) = ∑_k [f(x+e_k) + f(x−e_k) − 2f(x)], with shifts along each coordinate axis. Lattice fields are maps (Fin D → ℤ) → ℝ. Spatial dimension D is forced to 3 by the T8/T9 chain elsewhere in the monolith, but this lemma is stated for general D.
Constants are the zero modes of any discrete Laplacian; the identity is the first algebraic sanity check before linearity and continuum scaling.
proof idea
Tactic proof in three steps. Unfold the definition of lattice_laplacian to the finite sum over k : Fin D of f(shift_plus k x) + f(shift_minus k x) − 2 f x. With f the constant function fun _ => c, simp reduces every evaluation to c, so each summand is c + c − 2c. ring closes the identity to 0. No external lemmas beyond the definition and the shift helpers.
why it matters
Feeds continuum_limit_certificate (F-014 certificate), which packages quadratic leading order of J_log, CPT symmetry, vacuum structure, and the path lattice Laplacian → continuous ∇² → Klein–Gordon. Without Δ_lat(const) = 0, the discrete operator would not match the continuum Laplacian (which annihilates constants) and the Gaussian/universality-class story would fail at the first algebraic check.
In the forcing chain this sits after T5 (J-uniqueness) and T8 (D = 3): the continuum emerges from discrete J-cost on ℤ³ precisely because the quadratic piece produces this Laplacian. The lemma is local scaffolding for lattice_laplacian_add / lattice_laplacian_smul and the neighbor-cost variational picture, not a deep analytic result, but it is required for the certificate’s LAPLACIAN clause.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.