canonicalPeriodicDispFilteredLocalSlotSum_eq_baseFiltered
plain-language theorem explainer
On a periodic Freudenthal torus, after restricting local tet edge slots to a fixed displacement class, the indicator that a typed edge equals the cell-local edge is interchangeable with the indicator that only the base vertex matches the cube-edge base offset. Gravity/Regge lattice workers cite this when collapsing full edge equality to a base-offset check inside angle sums. The proof is Finset.sum_congr plus a local iff from typed-edge reconstruction lemmas, case-split on the base equation.
Claim. Fix nonzero lattice periods $N_x,N_y,N_z$, a periodic edge $e$, and a periodic cell-tet pair. Summing the local Freudenthal dihedral angle over the six tet edge slots whose cube-edge displacement matches $e$'s displacement, the contribution is nonzero only when $e$ equals the cell-local edge; that sum equals the analogous sum whose nonzero guard is only that $e$'s base vertex equals the cell origin plus the cube-edge base of that slot.
background
This module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not freely assert the physical Dirichlet equality; it supplies the finite combinatorial identities needed to reach that target.
A periodic edge carries a base vertex on the $N_x\times N_y\times N_z$ torus and a displacement class among the 19 one-cube Freudenthal edge types (axis and face/space diagonals). cubeEdgeDisp and cubeEdgeBase read those data off the local representative; addVertexBits shifts a cell origin by a local cube corner in $\mathrm{Fin},8$. Each of the six tet edge slots maps, via the cube triangulation's local edge table, to one of those 19 representatives.
The sums here are over slots filtered to a single displacement class. Within that class the remaining geometric content is whether the typed edge coincides with the cell-local edge, or merely whether bases match. Dihedral weights are the fixed local Freudenthal angles on those slots.
proof idea
Classical Finset.sum_congr over the common displacement filter. For each surviving slot $f$, extract the displacement match from filter membership. Build the iff: full typed-edge equality implies base equality by canonicalPeriodicTypedEdge_base_eq_of_localEdgeOf; conversely, base equality plus the already-known displacement match rebuilds the edge via canonicalPeriodicTypedEdge_eq_localEdgeOf_iff_base_and_disp. The local edge's own base unfolds by simp on localEdgeOf. Case-split on the base equation: both sides of the summand become the same angle (or both zero) after simp.
why it matters
Feeds canonicalPeriodicDispFilteredLocalSlotTripleAngleSumTarget_of_baseDispFiltered, whose doc states that the base-and-displacement filtered target implies the displacement-filtered target because, within a displacement class, full edge equality is equivalent to the base-offset equation. That step is how the module reduces incident-star angle-sum obligations on the periodic torus to checks that only track base offsets inside each displacement class.
In the broader gravity stack this is scaffolding for the physical six-tet cubic Dirichlet instance on the Freudenthal lattice: Regge-type edge actions and finite-difference Dirichlet targets need clean passage between typed edges and (base, disp) coordinates. The companion doc on the incident-filter form notes that nonincident typed pairs contribute zero, so later geometric work can stay on the finite incident star of each edge. No T0–T8 forcing step is claimed here; the result is pure lattice combinatorics supporting the Dirichlet/Regge side of RS gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.