stationarity_iff_laplacian_zero
plain-language theorem explainer
Stationarity of the Laplacian action on a weighted simplicial ledger graph is equivalent to the discrete Laplacian vanishing at every vertex. Researchers bridging discrete J-cost models to Regge calculus and the Einstein equations would cite this identification when closing the discrete-to-continuum gap. The proof is a one-line wrapper that applies the hypothesis directly via the definition of the discrete Laplacian.
Claim. For a weighted ledger graph $G$ and field perturbation $ε$, if the discrete Laplacian vanishes at every vertex then the weighted sum of field differences also vanishes: if $∀ i, (Δε)_i = 0$ then $∀ i, ∑_j w_{ij}(ε_i - ε_j) = 0$.
background
The ContinuumBridge module proves that J-cost stationarity on a simplicial ledger yields the Regge equations and hence the Einstein field equations in the continuum limit. WeightedLedgerGraph is the structure carrying a symmetric nonnegative weight matrix on $n$ vertices; the discrete_laplacian at vertex $i$ is defined exactly as $∑j w{ij}(ε_i - ε_j)$. In log coordinates the J-cost coupling expands quadratically as $(ε_i - ε_j)^2/2 + O((ε_i - ε_j)^4)$, reproducing the Laplacian action form.
proof idea
The proof is a one-line wrapper: introduce the hypothesis that the discrete Laplacian vanishes at each $i$, then apply the hypothesis directly to obtain the weighted sum, which is the definition of discrete_laplacian.
why it matters
This supplies the step3_laplacian_structure instantiation inside jcost_to_efe_chain, which assembles the full derivation from J-cost to the Einstein field equations. It realizes the module's central claim that the quadratic structure of J-cost makes its stationarity condition identical to the discrete Regge equations, consistent with the Recognition Science forcing chain and the identification of J-cost with the Regge action up to the factor $κ = 8φ^5$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.