sum_edges_slotMatch
plain-language theorem explainer
For any cell, tetrahedron, and edge-indexed family F, summing F only on edges that hit a local slot of that tet equals summing F over the six local edges of the tet. Gravity analysts cite it whenever a global Regge edge sum must be rewritten as a per-tet slot sum. The proof is a finite double-sum interchange: match cases expand to indicators, injectivity of localEdgeOf collapses each inner sum, then sum_comm finishes.
Claim. Fix a cell $c$ on the periodic $N\times N\times N$ Freudenthal torus, a tetrahedron index $\tau\in\{0,\ldots,5\}$, and any family $F$ of real values on edges times local slots. Then $\sum_e M(e)=\sum_{f=0}^{5} F(e_{c\tau f},f)$, where $M(e)=F(e,f)$ if the canonical slot lookup returns some $f$ for $(e,c,\tau)$ and $M(e)=0$ otherwise, and $e_{c\tau f}$ is the global edge occupying local slot $f$ of tet $\tau$ in cell $c$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol campaign: first and second variations of the plane-wave Regge action at flat, reduced by the tetrahedral Schläfli identity so that no second derivative of arccos survives.
The geometry is the periodic Freudenthal triangulation of the $N^3$ torus. Each cell carries six tetrahedra; each tet has six local edge slots. localEdgeOf picks the global periodic edge occupying a given slot. The partial map canonicalEdgeSlot? is the inverse lookup: given a global edge $e$, cell, and tet, it returns some f exactly when $e$ is that tet's local edge $f$, else none.
Upstream, canonicalEdgeSlot_eq_some_implies recovers $e=\mathrm{localEdgeOf}(c,\tau,f)$ from a successful lookup, and canonicalPeriodicLocalEdgeNoDup asserts that the six local edges of a fixed cell/tet are pairwise distinct. Together they make the incidence relation a partial involution between global edges and local slots, which is exactly what lets global edge sums regroup into tet-local slot sums.
proof idea
First record injectivity of $f\mapsto\mathrm{localEdgeOf}(c,\tau,f)$ from canonicalPeriodicLocalEdgeNoDup.
For each global edge $e$, expand the match on canonicalEdgeSlot? into a finite sum over slots of an indicator: if the lookup is none, every indicator is false (else canonicalEdgeSlot_eq_some_of_noDup would force a some); if it is some f0, the indicator sum collapses to the single term $F(e,f0)$ by sum_eq_single, using injectivity to kill other slots and canonicalEdgeSlot_eq_some_implies to identify $e$ with the local edge.
Global sum over $e$ of those expansions, apply Finset.sum_congr, then Finset.sum_comm to swap the $e$ and $f$ sums. For each fixed slot $f$, sum_ite_eq' picks out exactly the term at $e=\mathrm{localEdgeOf}(c,\tau,f)$, which is in the universe, yielding $\sum_f F(\mathrm{localEdgeOf}(c,\tau,f),f)$.
why it matters
This is the incidence involution named in the module doc as the first proved item of Gate A2: every regrouped Regge sum in the file rests on it. Downstream, sum_sqrt_deficitDeriv_eq_zero (the pathwise Schläfli kill) rewrites $\sum_e\sqrt{l_e},\delta'_e$ as a sum over tets of per-slot Schläfli contractions, and sum_edgeSqrtDeriv_deficitDeriv_flat does the same at flat for the mixed first-variation block $\sum_e L'_e(0),\delta'_e(0)$.
Without the bijection, the tetrahedral Schläfli identity (tetraSchlaefliSixEdgeClosedForm) cannot be applied tet-by-tet to delete the entire second group of $S'$, and Gate A2(a)–(b) (vanishing first variation at flat; second variation equal to $-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$ with no arccos second derivatives) would not close. In the broader RS gravity lane this is pure discrete differential geometry scaffolding for the continuum TT symbol, not a forcing-chain step, but it is the algebraic hinge that makes the Schläfli reduction mechanical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.