linearized_el_plus_laplacian_zero
plain-language theorem explainer
On any cubic lattice ℤ^D, the linearized Euler–Lagrange operator (sinh replaced by its argument) plus the nearest-neighbor lattice Laplacian vanishes identically at every site. Gravity and continuum-limit arguments cite this as the algebraic bridge from the J-cost EL equation to discrete Laplace theory. The proof is a one-line ring identity after unfolding the Laplacian and distributing the sum.
Claim. For any dimension $D$, any lattice field $f:\mathbb{Z}^D\to\mathbb{R}$, and any site $x$, $$\sum_{k=1}^{D}\bigl[(f(x)-f(x-e_k))-(f(x+e_k)-f(x))\bigr]+\Delta_{\mathrm{lat}}f(x)=0,$$ where $\Delta_{\mathrm{lat}}f(x)=\sum_k\bigl[f(x+e_k)+f(x-e_k)-2f(x)\bigr]$ is the standard nearest-neighbor lattice Laplacian and $e_k$ are the unit axis shifts.
background
The module gives a direct cubic-lattice proof that J-cost Regge calculus on $\mathbb{Z}^D$ converges to the continuum variational principle, replacing the general Cheeger–Müller–Schrader axiom. Tier 2 of that strategy linearizes the Euler–Lagrange equation of the J-cost action; after $\sinh(\varepsilon)\mapsto\varepsilon$, the discrete EL operator becomes a pure second-difference sum.
A lattice field is a real-valued function on sites of $\mathbb{Z}^D$. Axis shifts $x\mapsto x\pm e_k$ move one coordinate by $\pm 1$. The lattice Laplacian is the usual nearest-neighbor operator $\Delta_{\mathrm{lat}}f(x)=\sum_k[f(x+e_k)+f(x-e_k)-2f(x)]$. The linearized EL sum is exactly the opposite rearrangement of those same second differences.
Dimension $D$ is the RS-forced spatial dimension (T8/T9), but the identity holds for every $D$; no continuum or curvature hypothesis enters.
proof idea
Term-mode algebraic cancellation. Unfold the definition of the lattice Laplacian, so the goal is a sum of linearized EL increments plus a sum of Laplacian increments. Rewrite via Finset.sum_add_distrib into a single sum over axes $k$. For each $k$, ring shows the two summands cancel:
$(f(x)-f(x-e_k))-(f(x+e_k)-f(x))+\bigl(f(x+e_k)+f(x-e_k)-2f(x)\bigr)=0$.
No external lemmas beyond the definitions of the shifts and Laplacian are required.
why it matters
This is the core algebraic identity of Tier 2 in the cubic Regge convergence program: after linearizing $\sinh$, the discrete EL operator is minus the lattice Laplacian. The immediate parent is linearized_el_eq_neg_laplacian, which rearranges the same identity into equality form and feeds the chain toward linearized_el_zero_iff_laplacian_zero and the continuum limit of the Laplacian.
In the broader Recognition framework this closes the gap between the J-cost variational principle (with $J(e^\varepsilon)=\cosh\varepsilon-1$) on the cubic lattice and the discrete Laplace equation that converges to $\nabla^2$ at $O(a^2)$. Combined with Tier 1 action convergence and Tier 3 continuum extraction, it supports replacing the CMS axiom by an RS-specific direct proof that the lattice variational principle tends to the linearized Einstein equation. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.