laplacian_pairing_comm
plain-language theorem explainer
The discrete Laplacian pairing on a finite weighted ledger graph is symmetric in its two real vertex fields. Anyone proving Dirichlet-energy identities or self-adjointness steps in the simplicial continuum bridge would cite it. The argument is a three-step rewrite that transports symmetry from the polar bilinear form through the known pairing identification.
Claim. Let $G$ be a finite weighted ledger graph on $n$ vertices and let $\varepsilon,\eta:\{0,\ldots,n-1\}\to\mathbb{R}$ be real fields on the vertices. Then the Laplacian pairing is symmetric: $\langle\eta,\Delta_G\varepsilon\rangle=\langle\varepsilon,\Delta_G\eta\rangle$.
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 hypotheses.
A weighted ledger graph supplies a nonnegative, symmetric edge weight on $\mathrm{Fin},n$. The discrete Laplacian pairing is the finite sum that pairs one vertex field against the discrete Laplacian of another. The edge polar form (bilinearization of the quadratic Dirichlet action) is identified with that pairing by an upstream lemma: the edge polar form equals $\langle\eta,\Delta\varepsilon\rangle$.
A sibling result already shows the polar form itself is symmetric in its two fields. The present statement is the corresponding self-adjointness claim written directly in pairing language.
proof idea
Three rewrites, no new algebra. First reverse the identification of the polar form with the pairing on $(\varepsilon,\eta)$, so the goal becomes symmetry of the bilinear form. Apply the already-proved commutativity of the polar form. Reapply the same identification to land back on the swapped pairing. The whole proof is transport of symmetry along the bilinear-equals-pairing bridge.
why it matters
Self-adjointness of the discrete Laplacian is the algebraic reason the Dirichlet energy is a genuine quadratic form rather than an oriented pairing. The module treats that energy as the quadratic $J$-cost on the graph; symmetry is required before one can speak of a well-defined energy landscape on ledger configurations.
No downstream consumers are wired yet in the graph, but the immediate sibling equates Dirichlet energy with the Laplacian quadratic pairing, so this lemma is the natural symmetry step those energy identities rely on. It stays inside the pure finite-graph layer of the continuum bridge and does not touch the forcing chain (T5--T8) or RS unit normalizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.