CanonicalEdgeStencilSumCommTarget
plain-language theorem explainer
Names the finite-sum commutation identity that equates the double vertex sum of edge-aggregated pair weights times squared potential differences with the triple sum that loops edges outermost. Anyone proving that the canonical Dirichlet form equals the edge stencil cites this Prop as the bookkeeping hypothesis. The body is pure sum reordering over finite index types; no geometry enters yet.
Claim. For a finite 3D Regge triangulation $K$ with incidence-consistent squared edge lengths, the following holds for every vertex conformal potential $\xi$: $$\sum_{i,j}\Bigl(\sum_e w_{ij}(e)\Bigr)(\xi_i-\xi_j)^2 = \sum_e\sum_{i,j} w_{ij}(e)\,(\xi_i-\xi_j)^2,$$ where $w_{ij}(e)$ is the canonical edge-pair weight ($\sqrt{\ell_e^2}$ when $e$ joins $\{i,j\}$, else $0$).
background
The module isolates the final analytic Hessian step for a finite 3D Regge triangulation under the conformal ansatz, packaging the second variation into the existing Regge Hessian interface.
A Triangulation3D supplies finite vertex, edge, and tetrahedron counts together with incidence maps. Incidence consistency adds global squared edge lengths and local-to-global edge agreement. Vertex potentials are real functions on the finite vertex set. The canonical edge-pair weight for vertices $i,j$ and edge $e$ is $\sqrt{\ell_e^2}$ when the endpoints of $e$ are exactly ${i,j}$ (either orientation), and zero otherwise.
The identity asserted here is pure finite-sum bookkeeping: the factor $(\xi_i-\xi_j)^2$ does not depend on the edge index, so the edge sum may pass through the product and the three nested sums may be reordered.
proof idea
Definition only: the declaration is the Prop itself, not a proved theorem. Its body is the universal quantification over vertex potentials of equality between the vertex-outer double sum (with the edge sum collapsed into a pair weight) and the edge-outer triple sum. Downstream, canonicalEdgeStencilSumComm discharges this Prop by simp_rw [Finset.sum_mul] followed by a calc reordering of finite sums; no geometric lemmas are required.
why it matters
This target is the first bookkeeping gate before the per-edge double-count identity can be applied in the concrete Regge Hessian pipeline. The theorem canonicalEdgeStencilSumComm proves it outright. The conditional theorem canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex takes the target as hypothesis hSum (together with a reindex target) and concludes that the canonical Dirichlet quadratic form equals the edge stencil. That equality is the bridge from the conformal second-variation expansion of the Regge action to the discrete Dirichlet energy used in the Hessian interface. Within Recognition geometry this is scaffolding for the 3D Regge curvature package, not a forcing-chain landmark (T5–T8), but it is required for a fully expanded, incidence-consistent Hessian on finite triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.