flat_satisfies_el
plain-language theorem explainer
Constant (flat) lattice fields satisfy the Euler-Lagrange equation of the J-cost action exactly at every site. Convergence-chain and cubic-Regge certificate authors cite this as the vacuum solution step. The proof unfolds the EL sum and cancels by sinh(0)=0.
Claim. For any dimension $D\in\mathbb{N}$, constant $c\in\mathbb{R}$, and lattice site $x\in\mathbb{Z}^D$, if $f\equiv c$ then the Euler-Lagrange operator of the lattice $J$-cost action vanishes: $\mathrm{EL}[f](x)=0$. Explicitly, $\sum_{k=1}^{D}\bigl(\sinh(f(x)-f(x-e_k))-\sinh(f(x+e_k)-f(x))\bigr)=0$.
background
This module gives a direct cubic-lattice proof that J-cost Regge calculus on $\mathbb{Z}^D$ converges to the continuum variational principle (linearized Einstein equations), replacing the general Cheeger-Müller-Schrader axiom for the RS-specific case.
The lattice action is $S=\sum_{(y,k)} J_{\log}(f(y+e_k)-f(y))$, with $J_{\log}(\varepsilon)=\cosh(\varepsilon)-1$ (the T5 cost written in logarithmic coordinates). Differentiating in $f(x)$ and using $J_{\log}'=\sinh$ yields the Euler-Lagrange operator $\mathrm{EL}f=\sum_k\bigl(\sinh(f(x)-f(x-e_k))-\sinh(f(x+e_k)-f(x))\bigr)$.
Tier 2 of the module strategy linearizes this EL equation to the lattice Laplacian via $\sinh'(0)=\cosh(0)=1$. The present lemma is the exact vacuum check before that linearization: constant fields are exact critical points.
proof idea
Term-mode one-liner. Unfold the definition of the Euler-Lagrange sum; every bond difference on a constant field is zero, so each summand is $\sinh(0)-\sinh(0)$. simp with Real.sinh_zero finishes. No induction on $D$ and no approximation.
why it matters
Supplies the flat-solution field of the cubic Regge convergence certificate and step 4 of the proved convergence chain (both zero-axiom, zero-sorry assemblies in this module). Downstream, cubic_regge_convergence_cert packages it as flat_solution, and proved_convergence_chain records it as step4_flat_solution, sitting between EL-is-Laplacian and the $\sinh'(0)=1$ linearization coefficient.
In the RS gravity story this is the discrete vacuum: Minkowski (constant ledger field) is an exact critical point of the J-cost action on $\mathbb{Z}^D$, so the continuum limit can target linearized EFE about flat space without a residual lattice force. It is the exact Tier-2 anchor that lets the cubic case bypass general CMS comparison geometry. Dimension $D$ is parametric here; the framework later specializes to the T8 value $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.