IncidenceEdgeSlotPartition
plain-language theorem explainer
An incidence edge-slot partition for an incidence-consistent 3D triangulation assigns each tetrahedron and each of its six local edge slots a unique global edge representative. The incidence map hits that local slot if and only if the global edge is exactly that representative. Anyone building Regge first-variation or Hessian bookkeeping cites this package. It is pure structure data: two fields encode the unique-representative property that turns global edge sums into local six-edge sums.
Claim. For an incidence-consistent triangulation $K$ in three dimensions, an incidence edge-slot partition is a map sending each tetrahedron $\tau$ and each local edge slot $f\in\{0,\ldots,5\}$ to a global edge index such that, for every global edge $e$, tetrahedron $\tau$, and slot $f$, the incidence relation "$e$ meets $\tau$ in slot $f$" holds if and only if $e$ equals that representative of $(\tau,f)$.
background
The module targets the vanishing of the first variation of the full nonlinear Regge action at a flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; until the closed-form local Schläfli identities are fully expanded into derivatives, the module records exact analytic statements and the named bookkeeping inputs they need.
A 3D triangulation $K$ carries $n_T$ tetrahedra and $n_E$ global edges. Each tetrahedron has six local edge slots. Incidence consistency means local squared edge lengths agree with the global edge-length assignment wherever an edge meets a tetrahedron. The incidence map edgeInTet returns, for a global edge and a tetrahedron, either none or the local slot index at which they meet.
An incidence edge-slot partition is the concrete dual view: every local slot $(\tau,f)$ is represented by exactly one global edge, and the incidence map hits that slot precisely on that representative. Companion lemmas then convert a weighted sum over all global edges (with weights zero off the tetrahedron) into an ordinary six-term sum over local slots, with global lengths replaced by square roots of local squared edges.
proof idea
Pure structure definition: two fields. The first is the representative map from tetrahedron and local slot to global edge index. The second is the biconditional that the incidence map returns slot $f$ on tetrahedron $\tau$ exactly when the global edge equals that representative.
Three short companion theorems ride on the structure. The first is a one-line application of the biconditional at the representative itself. The second unfolds the global edge-length definition and rewrites via incidence consistency at the representative. The third is a four-step sum calculation: expand the match into an indicator sum, commute the double sum, collapse the inner sum to the unique representative via Finset.sum_eq_single and the biconditional, then replace global length by the local square-root formula.
why it matters
This structure is the intended concrete incidence class for edge-slot bookkeeping in the Regge first-variation pipeline. Downstream, incidenceEdgeSlotBookkeeping_of_partition builds the abstract bookkeeping interface from any such partition, and reggeActionFirstVariationInput_of_edgeSlotPartition packages that into the named input for the first-variation theorem at a flat configuration.
Concrete triangulations supply instances: the Freudenthal cube, the two-cube strip, and encoded periodic Freudenthal tori each construct an edge-slot partition. The nonlinear Hessian module reuses the same partition to match conformal edge sums and to obtain the near-zero Schläfli expansion from angle-line differentiability.
In the broader Recognition geometry stack this sits under the $D=3$ spatial forcing (T8) and the discrete Regge calculus that realises curvature on the eight-tick lattice. It does not itself prove first-variation vanishing; it supplies the unique-representative bookkeeping that lets Schläfli cancellation be written as a clean local sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.