laplacian_action_prod_form
plain-language theorem explainer
The identity rewrites the Laplacian action on a finite weighted ledger graph with log-potentials as half the double sum over vertex pairs of the edge weight times the squared potential difference. Workers on the nonlinear J-cost to Regge bridge cite this when isolating the quadratic term inside the exact action decomposition. The proof is a one-line wrapper that unfolds the Laplacian definition and closes by congruence.
Claim. Let $G$ be a weighted ledger graph on $n$ vertices and let $ε$ be a log-potential. The Laplacian action satisfies $laplacian_action(G, ε) = (1/2) ∑_{i,j} G.weight(i,j) (ε_i - ε_j)^2$.
background
The module develops the nonlinear J-cost action on simplicial ledgers to address Beltracchi §6: the quadratic (weak-field) approximation of J-cost must be separated from higher-order terms so that strong-field regimes remain accessible. The exact J-cost action is defined as ∑{i,j} w{ij} (cosh(ε_i - ε_j) - 1), which equals the Laplacian action plus a quartic remainder. The Laplacian action itself is the quadratic truncation of that expression. Upstream results supply the constants (G from Constants) and the functional-equation reparametrization used to express the cosh form.
proof idea
The proof is a one-line wrapper. It unfolds the definition of laplacian_action and applies congr 1 to equate the expanded form to the explicit double-sum quadratic expression.
why it matters
This supplies the quadratic term required by the downstream decomposition theorem exact_decomposition, which states exactJCostAction = laplacian_action + quarticRemainder with the remainder non-negative. The result therefore supports the claim that the J-cost side of the bridge holds unconditionally for any ε, not merely small ε, thereby closing the weak-field gap noted in the module doc-comment. It sits inside the Recognition Science forcing chain after the J-uniqueness and phi-fixed-point steps and before the eight-tick octave and D=3 geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.