euler_lagrange
plain-language theorem explainer
Defines the discrete Euler-Lagrange operator of the lattice J-cost action at a site x on ℤ^D. It is the sum over axes of sinh of backward bond jumps minus sinh of forward bond jumps. Gravity convergence certificates and the flat-field vacuum check cite it. The body is the explicit variational formula, not a proved identity.
Claim. For a lattice field $f:\mathbb{Z}^D\to\mathbb{R}$ and site $x$, the Euler-Lagrange density of the bond action $S=\sum_{(y,k)} J_{\log}(f(y+e_k)-f(y))$ is $(\mathrm{EL}\,f)(x)=\sum_{k=1}^{D}\bigl[\sinh\bigl(f(x)-f(x-e_k)\bigr)-\sinh\bigl(f(x+e_k)-f(x)\bigr)\bigr]$, using $J_{\log}'=\sinh$.
background
Module CubicReggeProof gives a direct cubic-lattice proof that RS J-cost Regge data converge to linearized Einstein equations, replacing the general Cheeger-Müller-Schrader axiom. The lattice is ℤ^D (not arbitrary simplicial mesh); the cost is the forced J with $J(e^\varepsilon)=\cosh\varepsilon-1$, so bond costs are $J_{\log}$ of log-ratio jumps.
A lattice field is a real assignment on sites of ℤ^D (log-ratio perturbations). Axis shifts $x\mapsto x\pm e_k$ are the elementary neighbor maps. The action is a sum of $J_{\log}$ over oriented bonds; varying with respect to the value at $x$ and using $J_{\log}'=\sinh$ produces exactly the displayed sum over the $2D$ incident bonds.
This sits in Tier 2 of the module strategy: EL linearization to the lattice Laplacian (via $\sinh'(0)=1$), before the continuum limit $\Delta_{\mathrm{lat}}/a^2\to\nabla^2$.
proof idea
Definitional, not a tactic proof. The body is the closed-form variational derivative: sum over $k\in\mathrm{Fin},D$ of $\sinh(f(x)-f(x-e_k))-\sinh(f(x+e_k)-f(x))$, with neighbor sites via the continuum-limit shift maps. No lemmas are applied; the formula is the content of the def.
why it matters
Names the discrete EL operator that Tier 2 linearizes to $-\Delta_{\mathrm{lat}}$. Downstream, flat constant fields are shown to satisfy EL exactly (every sinh argument vanishes). The same operator appears in the proved convergence chain (linearized EL equals minus lattice Laplacian) and in the cubic Regge convergence certificate that retires the old regge-to-EH and Ricci-convergence axioms for weak-field RS gravity.
Framework link: J is the T5 unique cost; on the cubic lattice forced by discreteness, this EL is the variational bridge from recognition bonds to continuum linearized gravity (module target: O(a²) match to linearized EFE). It does not itself force D=3; D is a parameter here, fixed elsewhere by T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.