canonicalEdgeStencilSumComm
plain-language theorem explainer
Exact finite-sum commutation for the canonical edge-pair weight on an incidence-consistent 3D Regge triangulation: the edge sum may sit inside or outside the double vertex sum against squared potential differences. Anyone equating the canonical Regge Hessian quadratic form to a graph Dirichlet (edge-stencil) energy cites this. The proof is pure Finset bookkeeping: distribute the product, then apply sum_comm twice.
Claim. Let $K$ be a finite 3D Regge triangulation with incidence-consistent global squared edge lengths, and let $w_{ij}(e)$ be the canonical edge-pair weight ($\sqrt{\ell_e^2}$ if edge $e$ joins vertices $i$ and $j$, else $0$). For every vertex potential $\xi$, $$\sum_i\sum_j\Bigl(\sum_e w_{ij}(e)\Bigr)(\xi_i-\xi_j)^2=\sum_e\sum_i\sum_j w_{ij}(e)(\xi_i-\xi_j)^2.$$
background
The module isolates the final analytic Hessian step for a finite 3D Regge triangulation: a concrete action package under the conformal ansatz is turned into the existing Regge Hessian data interface.
A Triangulation3D carries finite vertex, edge, and tetrahedron counts plus abstract incidence (edgeVerts, tetVerts). IncidenceConsistent strengthens that with a global squared-edge map and local-to-global edge agreement (plus the closed-form Schläfli data needed for a global Schläfli identity). The canonical edge-pair weight is nonzero only when a global edge meets the unordered vertex pair $(i,j)$, in which case it equals the square root of that global squared length.
The target proposition is purely bookkeeping: it equates the form with the edge sum folded into a pair weight against the fully expanded triple sum. Downstream identities need the expanded order so a per-edge double-count can fire.
proof idea
Fix an arbitrary vertex potential $\xi$. Rewrite the left-hand side by distributing multiplication over the finite edge sum (Finset.sum_mul), producing a triple sum $\sum_i\sum_j\sum_e w_{ij}(e)(\xi_i-\xi_j)^2$.
A first Finset.sum_comm swaps the $j$ and $e$ summations inside each fixed-$i$ block. A second Finset.sum_comm then moves the outer $i$ sum past $e$, yielding $\sum_e\sum_i\sum_j$. The calc chain is only these two commutations; no geometric content is used beyond the types of the finite index sets.
why it matters
This lemma is the sum-order gate before per-edge double-count identities that turn the canonical Regge Hessian quadratic form into a graph Dirichlet energy. Downstream, hessianQuadratic_canonical_eq_freudenthalStencil derives (never postulates) that the frozen quadratic form of the canonical periodic Freudenthal triangulation equals the seven-class stencil energy $\sum_x\sum_d c_d(u(x+d)-u(x))^2$. Separately, periodicEdgeStencilTarget_of_noSelfLoop discharges the periodic edge-stencil Dirichlet target via a sum-comm-and-reindex argument that consumes this commutation.
In the broader RS geometry stack this is scaffolding closure for the concrete Hessian path (Regge action under conformal ansatz to second variation to stencil form), not a forcing-chain landmark. It does not touch T5–T8, RCL, or the mass ladder; it is local discrete-geometry bookkeeping that makes the Freudenthal stencil comparison fully derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.