neighbor_cost
plain-language theorem explainer
Defines the total J-cost of nearest-neighbor field differences at a lattice site x in D dimensions. For each axis k it sums J_log of the forward and backward increments of a lattice field f. Continuum-limit and gravity modules cite it as the discrete action density whose quadratic regime yields the lattice Laplacian and, after continuum scaling, diffusion and Klein–Gordon structure.
Claim. For a lattice field $f:\mathbb{Z}^D\to\mathbb{R}$ and a site $x\in\mathbb{Z}^D$, the neighbor cost is $$C_{\mathrm{nn}}(f,x)=\sum_{k=1}^{D}\Bigl(J_{\log}\bigl(f(x+e_k)-f(x)\bigr)+J_{\log}\bigl(f(x-e_k)-f(x)\bigr)\Bigr),$$ where $e_k$ is the unit step along axis $k$ and $J_{\log}$ is the Recognition J-cost on log-ratio increments.
background
Module F-014 (Continuum Limit) shows how discrete J-cost dynamics on $\mathbb{Z}^D$ produce smooth second-order PDEs. RS is ledger-discrete; observed physics is continuum. The bridge is the small-perturbation expansion $J(\mathrm{e}^{t})=\cosh t-1=t^2/2+O(t^4)$, so quadratic costs generate a lattice Laplacian and then $\nabla^2$.
A lattice field is a map $f:\mathbb{Z}^D\to\mathbb{R}$ assigning a log-ratio perturbation to each site. Shifts $x\mapsto x\pm e_k$ move one step along axis $k$. 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)$.
$J_{\log}$ is the discrete recognition cost on increments (from DiscretenessForcing). Neighbor cost packages the full nearest-neighbor J-contribution at $x$ before any continuum or quadratic approximation.
proof idea
Pure definition: sum over axes $k\in\mathrm{Fin},D$ of $J_{\log}$ on the forward difference $f(x+e_k)-f(x)$ plus $J_{\log}$ on the backward difference $f(x-e_k)-f(x)$. No proof obligations; noncomputable only because real summation and $J_{\log}$ are. Downstream theorems (e.g. jcost_gives_laplacian_structure) expand each $J_{\log}$ via the quadratic leading term and compare to half the squared increments.
why it matters
This is the discrete action density that turns J-cost variational dynamics into diffusion. The in-module theorem jcost_gives_laplacian_structure states that for small neighbor differences the neighbor cost approximates $\frac12\sum_k\bigl[(\Delta_+f)^2+(\Delta_-f)^2\bigr]$, whose $f(x)$-gradient is the lattice Laplacian—so minimizing J yields Laplacian flow.
Downstream, Gravity.ContinuumManifoldEmergence.jcost_neighbor_is_laplacian and LatticeConvergence.jcost_neighbor_approximation_3D specialize the same link in $D=3$. CubicReggeProof.ProvedConvergenceChain lists it as Step 2 (neighbor cost $\approx\sum\varepsilon_k^2/2$) on the proved path from RS lattice to linearized Einstein equations; total_action_convergence reuses the same bound. In the F-014 chain this sits between T5 J-uniqueness / RCL and continuum $\nabla^2\to$ Klein–Gordon (mass from the $\phi$-ladder) and later curvature/EFE structure. Closes the discrete-to-continuum gap without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.