pairing_eq_left_weighted_sum
plain-language theorem explainer
On a finite weighted ledger graph, the Laplacian pairing of two vertex fields expands as a double sum of edge weights times the hop difference of one field, times the other field at the source vertex. Proofs that equate the edge polar form to the pairing cite this expansion. The argument unfolds the pairing, distributes the outer factor through the inner sum, and reorders real multiplications.
Claim. Let $G$ be a weighted ledger graph on $n$ vertices with edge weights $w_{ij}$, and let $\varepsilon,\eta:\{0,\ldots,n-1\}\to\mathbb{R}$. Write $(\Delta\varepsilon)_i=\sum_j w_{ij}(\varepsilon_i-\varepsilon_j)$ for the discrete Laplacian. Then the pairing equals the left-weighted double sum: $\langle\eta,\Delta\varepsilon\rangle=\sum_i\sum_j w_{ij}(\varepsilon_i-\varepsilon_j)\eta_i$.
background
This module isolates the finite weighted-graph Dirichlet action used by the simplicial ledger continuum bridge. Imports are Mathlib-only; the action, Laplacian, and pairing identities carry no physical normalization and no continuum endpoint assumptions.
A weighted ledger graph on $n$ vertices is a symmetric nonnegative weight map $w$. The discrete Laplacian of a vertex field $\varepsilon$ is $(\Delta\varepsilon)i=\sum_j w{ij}(\varepsilon_i-\varepsilon_j)$. The Laplacian pairing is the finite product $\langle\eta,\Delta\varepsilon\rangle=\sum_i\eta_i(\Delta\varepsilon)_i$. Upstream, the same Laplacian appears in the continuum-bridge module as the discrete skeleton of the quadratic graph action (the discrete J-cost).
The present identity is pure finite-sum algebra: it only expands that pairing into an explicit double sum with $\eta$ factored on the left.
proof idea
Unfold the pairing and the discrete Laplacian to get $\sum_i\eta_i\sum_j w_{ij}(\varepsilon_i-\varepsilon_j)$. A calc block first applies Finset.mul_sum (via Finset.sum_congr) to pull $\eta_i$ inside the inner sum, yielding $\sum_i\sum_j\eta_i\cdot(w_{ij}(\varepsilon_i-\varepsilon_j))$. A second double sum_congr with ring reorders the real factors to $w_{ij}(\varepsilon_i-\varepsilon_j)\eta_i$. No graph axioms are used.
why it matters
The sole downstream consumer is laplacian_bilinear_eq_pairing, whose doc-comment states that the edge polar form is exactly the Laplacian pairing $\langle\eta,\Delta\varepsilon\rangle$. That theorem opens the module's "Exact Dirichlet identities" section and is the bridge from the bilinear edge form to the Laplacian pairing used throughout the simplicial ledger.
In the Recognition framework the discrete Laplacian action is the quadratic J-cost on the ledger graph. Keeping the pairing expansion purely combinatorial (Mathlib sums only) lets later continuum-bridge steps attach physical normalization without smuggling continuum hypotheses into the finite identities. The result is private scaffolding inside the Dirichlet-action file, not a public API theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.