linearized_el_zero_iff_laplacian_zero
plain-language theorem explainer
The linearized Euler-Lagrange stationarity condition for a real lattice field on ℤ^D is equivalent to the lattice Laplace equation vanishing at each site. Continuum-limit and discrete-gravity arguments cite this when reducing J-cost first variations to discrete harmonicity. The proof rewrites through the identity that linearized EL equals minus the lattice Laplacian, then both directions by linear arithmetic.
Claim. For any dimension $D$, lattice field $f:\mathbb{Z}^D\to\mathbb{R}$, and site $x$, the sum over axes $k$ of the centered first differences $(f(x)-f(x-e_k))-(f(x+e_k)-f(x))$ vanishes if and only if the lattice Laplacian $(\Delta_{\mathrm{lat}} f)(x)=0$.
background
The module gives a direct cubic-lattice Regge convergence proof for RS: J-cost interactions on ℤ^D, replacing the general Cheeger-Müller-Schrader axiom. A lattice field is a map from integer sites to ℝ (log-ratio perturbations). Shifts move one step along a coordinate axis. The lattice Laplacian is the standard nearest-neighbor operator $(\Delta_{\mathrm{lat}} f)(x)=\sum_k\bigl(f(x+e_k)+f(x-e_k)-2f(x)\bigr)$.
Tier 2 of the strategy linearizes the Euler-Lagrange equation of the J-cost action. Because $J(e^\varepsilon)=\cosh\varepsilon-1$ and $\sinh'(0)=1$, the first variation collapses to a discrete second-difference sum. The sibling identity records that this linearized EL expression equals $-\Delta_{\mathrm{lat}} f$ pointwise.
proof idea
One rewrite applies the sibling identity that the linearized EL sum equals the negative lattice Laplacian. The goal becomes $-\Delta_{\mathrm{lat}} f(x)=0\leftrightarrow\Delta_{\mathrm{lat}} f(x)=0$. Both directions are immediate linear arithmetic (constructor; intro; linarith). No expansion of the Laplacian definition is needed once the identity is in place.
why it matters
This is the equivalence half of Tier 2 (EL linearization) in the cubic Regge program: linearized stationarity of the J-cost action is exactly discrete harmonicity. With Tier 1 (bond action error $O(\varepsilon^4)$ from the quadratic approximation of $J\circ\log$) and Tier 3 (lattice Laplacian over $a^2$ tends to $\nabla^2$), it supports convergence of the RS variational principle on ℤ^D to the continuum linearized field equations at $O(a^2)$.
No downstream theorems are wired yet. Sibling results (flat fields satisfy EL; continuum limit of the Laplacian) sit on the same spine. In the broader framework this is the discrete bridge from the Recognition cost $J$ to continuum gravity on the forced cubic lattice, without invoking general simplicial CMS machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.