CanonicalEdgePairWeightReindexTarget
plain-language theorem explainer
Defines the finite-sum reindexing identity that collapses a double sum over all vertex pairs, weighted by the canonical edge-pair kernel, onto twice the oriented contribution of a single global edge. Anyone equating the full Dirichlet energy to the edge-stencil form cites this Prop as the per-edge target. The body is a pure equality of sums; no proof is attached here.
Claim. For an incidence-consistent 3D triangulation $K$ and every vertex potential $\xi$ and global edge $e$, the double sum $\sum_{i,j} w_{ij}(e)\,(\xi_i-\xi_j)^2$ equals $2\sqrt{\ell_e^2}\,(\xi_{v_1(e)}-\xi_{v_2(e)})^2$, where $w_{ij}(e)$ is the canonical edge-pair weight and $\ell_e^2$ is the squared length of $e$.
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 ReggeHessianData interface.
The parent target CanonicalDirichletEqualsEdgeStencilTarget asserts equality of the full canonical Dirichlet energy with the edge-stencil Dirichlet energy. The present definition is the exact finite-sum reindexing identity underlying that equality: each global edge should contribute twice to the oriented vertex-pair sum, once per orientation.
Here $K$ is a Triangulation3D with incidence consistency $hK$, which supplies edge endpoints via edgeVerts and squared lengths via globalSqEdge. The weight canonicalEdgePairWeight is the kernel that picks out the contribution of edge $e$ to the pair $(i,j)$. VertexPotential assigns a real scalar to each vertex.
proof idea
No proof: this is a Prop-valued definition fixing the target equality. Downstream, canonicalEdgePairWeightReindex_of_noSelfLoop discharges it under a no-self-loop hypothesis by expanding the double sum, retaining only the two oriented endpoint pairs of $e$, and reading off the factor $2\sqrt{\ell_e^2}$. The companion theorem canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex then consumes the target (together with a sum-commutation hypothesis) to obtain the full Dirichlet-versus-stencil equality.
why it matters
Without this per-edge reindexing identity, the passage from the dense vertex-pair Dirichlet form to the sparse edge stencil cannot be stated cleanly. It is the intermediate Prop fed to canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex, which closes CanonicalDirichletEqualsEdgeStencilTarget, and it is the conclusion of canonicalEdgePairWeightReindex_of_noSelfLoop.
In the concrete Regge Hessian pipeline this is the combinatorial step that lets the second variation of the conformal Regge action reduce to a weighted graph Laplacian on the triangulation skeleton. That reduction is required before the Hessian can be matched to the ReggeHessianData interface used elsewhere in the geometry stack. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete geometry supporting the action calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.