incidenceEdgeSlotPartition_sum_match_conformal
plain-language theorem explainer
Equates the global sum of conformal hinge lengths times incidence-partitioned weights with the fully local sum of conformal edge lengths times those weights. Anyone building the conformal Schläfli expansion near the flat potential cites this reindexing identity. The proof is a three-step finite-sum calc: distribute the product, commute the double sum, then apply the per-tetrahedron partition lemma.
Claim. Let $K$ be an incidence-consistent 3D triangulation with an incidence edge-slot partition, $\xi$ a vertex potential, and $w_{\tau,f}$ real weights on the six local edges of each tetrahedron $\tau$. Then $$\sum_e \ell_e^{\mathrm{conf}}(\xi)\,\Bigl(\sum_{\tau}\,w_{\tau,f(e,\tau)}\Bigr)=\sum_{\tau}\sum_{f=0}^{5}\sqrt{\ell_{\tau,f}^{2,\mathrm{conf}}(\xi)}\,w_{\tau,f},$$ where the inner sum runs only over tetrahedra incident to edge $e$ (via the edge-in-tet incidence map), $\ell_e^{\mathrm{conf}}$ is the conformal hinge length of global edge $e$, and $\ell_{\tau,f}^{2,\mathrm{conf}}$ is the local squared edge length under the vertex-conformal ansatz.
background
This module isolates the hard second-variation calculation for the nonlinear Regge action: the second directional derivative at the flat potential must match the canonical incidence Hessian. Once that chain-rule endpoint is in hand, the existing second-variation input package follows at once.
Under the vertex-conformal ansatz, each local squared edge in tetrahedron $\tau$ scales by $\exp(\xi_u+\xi_v)$ for its endpoints, written $\ell_{\tau,f}^{2,\mathrm{conf}}$. The 3D Regge hinge measure is edge length; its conformal version is $\ell_e^{\mathrm{conf}}=\sqrt{\ell_e^2},\exp((\xi_u+\xi_v)/2)$. The incidence map edgeInTet sends a global edge and tetrahedron to the local slot $f\in{0,\ldots,5}$ when the edge belongs to that tet, else none.
An incidence edge-slot partition packages the global-to-local bookkeeping so that sums over edges of hinge data can be rewritten as sums over tetrahedra and local slots. The sibling per-tet identity already matches one tetrahedron's contribution; this theorem lifts that match to the full double sum.
proof idea
Three-step calc on finite sums. First, for each global edge, pull the conformal hinge factor through the inner tet-sum via Finset.mul_sum, turning the product-of-sum into a double sum. Second, commute the edge and tet summations with Finset.sum_comm. Third, for each fixed tetrahedron, invoke the already-proved per-tet identity incidenceEdgeSlotPartition_edge_sum_for_tet_conformal, which replaces the edge-sum of hinge measure times matched weights by the local sum $\sum_f\sqrt{\ell_{\tau,f}^{2,\mathrm{conf}}},w_{\tau,f}$. No analytic estimates: pure reindexing under the incidence partition.
why it matters
Direct input to conformalSchlaefliNearZeroExpansion_of_angleDiff_and_partition, which assembles the conformal Schläfli near-zero expansion from angle-line differentiability plus the partition. That expansion is a link in the nonlinear directional Hessian chain: second derivative of the Regge action at the flat potential must equal the canonical incidence Hessian.
In the broader Recognition geometry stack this is bookkeeping, not new physics: it ensures global hinge sums and local conformal edge sums agree so the second-variation target can be stated purely in local tet data. It does not itself force $D=3$ or the eight-tick structure; those sit upstream in the forcing chain. It closes a pure reindexing gap so the remaining hard work is the analytic expansion of dihedral angles, not incidence algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.