IncidenceEdgeSlotBookkeeping
plain-language theorem explainer
Packages the exact reindexing identity that equates a weighted sum of local tetrahedral edge-slot contributions to the same weights summed through global edges with matching flat lengths. Anyone proving first variation of the nonlinear Regge action, or building Freudenthal cube/torus bookkeeping, cites this certificate. It is a structure with a single Prop field; concrete instances come from incidence partitions.
Claim. For a 3D triangulation $K$ that is incidence-consistent, an incidence edge-slot bookkeeping certificate is a proof that for every local weight $w_{\tau,f}$ on tetrahedron-edge slots, $\sum_e \ell_e \sum_{\tau}\!\sum_{f:\,e\in\tau} w_{\tau,f} = \sum_{\tau}\sum_{f=1}^{6} \sqrt{s_{\tau,f}}\, w_{\tau,f}$, where $\ell_e$ is the global flat edge length and $s_{\tau,f}$ is the squared local edge length of slot $f$ in tetrahedron $\tau$.
background
The module targets the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus vanishing deficit; analytic work needs clean interchange between global edge sums and local tetrahedral edge-slot sums.
A triangulation $K$ carries $n_T$ tetrahedra and $n_E$ global edges. Each tetrahedron has six edge slots. Incidence consistency supplies, for each local slot, at least one global edge that hits it. Flat edge lengths on global edges must match the square roots of the local squared edge lengths wherever incidence holds.
Existence alone does not justify exact reindexing of finite sums: one also needs uniqueness and no double-counting of slots. This structure records that full bookkeeping identity as a named hypothesis package for downstream derivative and Schläfli arguments.
proof idea
Definitional structure, not a proved theorem. The sole field is the universal equality sum_match over arbitrary real weights on local slots. Concrete inhabitants are built by incidenceEdgeSlotBookkeeping_of_partition from an incidence edge-slot partition (bijection between global edges and the slots they cover), which rewrites the double sum by partitioning the local index set. Freudenthal cube, two-cube strip, and periodic torus modules supply such partitions and wrap them into instances of this structure.
why it matters
This is the incidence bookkeeping gate for the Regge first-variation pipeline. It feeds conformalSchlaefliIncidenceBookkeeping_of_edgeSlotBookkeeping, which turns the certificate plus a local dihedral directional-derivative package into conformal Schläfli incidence bookkeeping, and reggeActionFirstVariationInput_of_edgeSlotBookkeeping, which assembles the full named input for the vanishing-first-variation theorem at a flat configuration.
Concrete geometry modules (Freudenthal six-tet cube, two-cube strip, encoded periodic Freudenthal torus) produce instances, so the abstract identity is discharged on the standard RS 3D meshes. In the broader framework this sits under $D=3$ spatial geometry (forcing chain T8) and the eight-tick/octave discrete structure that motivates the triangulation setting; it does not itself touch $J$-cost or the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.