incidenceEdgeSlotBookkeeping_of_partition
plain-language theorem explainer
From an incidence edge-slot partition on a consistent 3D triangulation, one obtains the bookkeeping identity that reindexes weighted global-edge sums to pure local tetrahedral edge-slot sums with matching flat lengths. Anyone assembling first-variation input for the nonlinear Regge action on Freudenthal cubes, strips, or periodic tori cites this. The proof is a three-step sum rewrite: distribute lengths, commute sums, then apply the partition's per-tetrahedron edge sum.
Claim. Let $K$ be a 3D triangulation that is incidence-consistent, and let $P$ be an incidence edge-slot partition of $K$ (every local slot $(\tau,f)$ has a unique global edge representative). Then the bookkeeping identity holds: for every local weight $w$, $\sum_e \ell_e \sum_\tau w_{\tau,f(e,\tau)} = \sum_\tau \sum_{f=0}^{5} \sqrt{(K.\mathrm{tet}\,\tau).\mathrm{sqEdge}\,f}\, w_{\tau f}$, where $\ell_e$ is the global flat edge length.
background
This module targets the vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential, via Schläfli cancellation plus zero deficit. Until the closed-form local Schläfli identities are fully expanded into derivatives, the module records the exact analytic statement and the named geometric inputs it needs.
An incidence edge-slot partition supplies a map localEdgeOf sending each tetrahedron $\tau$ and local edge index $f\in{0,\ldots,5}$ to a unique global edge, with the incidence map edgeInTet hitting that slot if and only if the global edge is that representative. The bookkeeping structure is the certificate that weighted sums over global edges and tetrahedra equal direct sums over local slots with matching flat lengths: existence of a global edge per slot comes from incidence consistency, but exact reindexing also needs uniqueness, which the partition encodes.
Global edge lengths are the consistent lengths induced on the triangulation; local squared edge lengths come from each tetrahedron's metric data. Concrete incidence maps appear in the Freudenthal cube and two-cube strip constructions.
proof idea
The definition fills the single field sum_match of the bookkeeping structure. Fix an arbitrary local weight $w$. Start from the double sum over global edges $e$ and tetrahedra $\tau$ of $\ell_e$ times the matched slot weight. Distribute $\ell_e$ across the inner sum via Finset.mul_sum. Commute the two finite sums with Finset.sum_comm so the outer index is $\tau$. For each fixed $\tau$, invoke the partition lemma P.edge_sum_for_tet w τ, which collapses the sum over global edges (via the unique representative and the incidence iff) to a sum over the six local slots $f$, replacing $\ell_e$ by $\sqrt{(K.\mathrm{tet},\tau).\mathrm{sqEdge},f}$.
why it matters
First-variation input for the nonlinear Regge action needs the bookkeeping identity so that hinge and edge contributions can be rewritten purely in local tetrahedral coordinates. This constructor is the standard bridge from a concrete partition to that certificate.
Downstream, the Freudenthal six-tetrahedron cube, the two-cube strip, and the encoded periodic Freudenthal torus all obtain their edge-slot bookkeeping by applying this definition to their respective partitions. The same module then packages a partition plus flatness into full first-variation input via reggeActionFirstVariationInput_of_edgeSlotPartition.
In the broader Recognition geometry stack this sits under the $D=3$ spatial forcing (T8) and the discrete Regge calculus used to probe flat conformal backgrounds. It does not itself prove the variation vanishes; it only supplies the incidence reindexing those proofs require.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.