laplacian_action_as_prod_sum
plain-language theorem explainer
The theorem rewrites the discrete Laplacian action on any weighted ledger graph as a single sum over the Cartesian product of vertices. Discrete gravity researchers cite it when converting double sums into product sums for linearization arguments. The proof is a term-mode wrapper that unfolds the definition and applies a Finset product-sum identity.
Claim. Let $n$ be a natural number, $G$ a weighted ledger graph on $n$ vertices with edge weights $w_{ij}$, and let $ε$ be a real-valued log-potential on those vertices. Then the Laplacian action satisfies $Δ_G ε = (1/2) ∑_{(i,j) ∈ [n]×[n]} w_{ij} (ε_i − ε_j)^2$.
background
The module CubicDeficitDischarge discharges the ReggeDeficitLinearizationHypothesis for the RS-canonical cubic lattice presentation. It supplies a quadratic-in-ε truncation of the piecewise-flat Regge deficit together with a hinge list, so that the leading-order identity (regge_sum) = κ · (laplacian_action) holds exactly. The Laplacian action itself is the quadratic J-cost on the graph, defined in ContinuumBridge as (1/2) times the double sum over vertices of weight times squared potential difference. This theorem merely rewrites that double sum as an explicit sum over the product Finset (Fin n) ×ˢ (Fin n).
proof idea
The term proof unfolds laplacian_action, applies congr 1, rewrites the universe as the Cartesian product via Finset.univ_product_univ, and concludes with the symmetric form of Finset.sum_product' applied to the function (i,j) ↦ G.weight i j * (ε i − ε j)^2.
why it matters
The lemma is invoked inside cubic_linearization_discharge, the main theorem that discharges ReggeDeficitLinearizationHypothesis unconditionally for any weighted ledger graph. It completes Phase A of the four-phase program that promotes the draft paper's Theorem 5.1 (field-curvature identity) from a pattern-matching argument to a Lean theorem. In the Recognition Science setting it supplies the exact linearization step needed before higher-order cubic corrections are handled in Phase D via the existing CubicReggeProof infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.