canonicalDualWeight
plain-language theorem explainer
Incidence-defined hinge weight between two vertices of a finite 3D Regge triangulation: sum over global edges of the edge length when the edge joins the pair, else zero. Anyone assembling the graph-Dirichlet form of the Regge Hessian cites this weight. The body is a one-line sum of the per-edge pair contributions.
Claim. For a finite 3D Regge triangulation $K$ with incidence-consistent squared edge lengths, and vertices $i,j$, the canonical dual weight is $w_{ij}=\sum_e \ell_e\,\mathbf{1}_{\{e\text{ joins }i,j\}}$, where $\ell_e=\sqrt{q_e}$ is the length of global edge $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 Regge-Hessian interface.
A Triangulation3D carries abstract incidence (vertex/edge/tet counts, edge endpoints, tet vertex maps) plus a nondegenerate squared-edge tuple on every tetrahedron. IncidenceConsistent strengthens that data: local tet edge slots match global endpoints up to orientation, a global squared-edge function is supplied, and a local closed-form Schläfli identity is available so global Schläfli needs no caller-supplied package.
The per-edge building block returns $\sqrt{q_e}$ when global edge $e$ has endpoints $(i,j)$ or $(j,i)$, and zero otherwise. The dual weight simply totals those contributions over all edges, yielding the unordered vertex-pair hinge weight used by the Dirichlet energy and Hessian.
proof idea
Pure definition: unfold as the finite sum over Fin K.nE of the per-edge pair weight. No tactics, no lemmas. Nonnegativity and symmetry are proved separately by summing the corresponding per-edge facts.
why it matters
This weight is the incidence kernel of the concrete Regge Hessian package. It feeds the canonical Dirichlet energy (half-sum of $w_{ij}(\xi_i-\xi_j)^2$), its expanded quadratic form, the equality of that energy with the edge-stencil form (under sum-commute and reindex hypotheses), the off-diagonal Hessian entries (negative the weight), and the nonnegativity/symmetry lemmas.
Downstream it appears in the T5-to-nonlinear-Regge J-cost bridge certificate in the unified forcing chain: the discrete curvature action whose second variation is this weighted graph Laplacian is the geometric side of matching T5's unique cost $J(x)=\cosh(\log x)-1$ to a nonlinear Regge action. Without a concrete, incidence-defined dual weight, that bridge has no discrete operator to certify against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.