canonicalPeriodicBaseDispFilteredLocalSlotTripleSum_eq_angleTemplate
plain-language theorem explainer
On a periodic Freudenthal torus, the base-and-displacement filtered sum of local dihedral angles over cells, tets, and edge slots equals the symbolic local angle-sum template for that edge's displacement class. Gravity and discrete-Regge workers cite it to collapse the periodic triple sum to a finite template before proving zero deficit. The proof rewrites to a local pair-displacement filter identity, then applies the corresponding template evaluation.
Claim. For positive lattice sizes $N_x,N_y,N_z$ and any periodic edge $e$ on the Freudenthal torus, the double sum over periodic tetrahedra and over the six local edge slots whose cube-edge displacement matches $e$'s displacement, of the local dihedral angle when the base vertex also matches (else zero), equals the Freudenthal local displacement angle-sum template evaluated at $e$'s displacement class.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not give the physical Dirichlet equality for free; it reduces it to checkable geometric identities.
A periodic edge carries a base vertex and a displacement class on the torus. Each cube is triangulated into six tets; localEdgeOf assigns each local tet edge slot a global cube-edge representative, and addVertexBits shifts a cell origin by an 8-bit vertex offset. The filtered triple sum keeps only those (cell, tet, slot) contributions whose displacement and base match the typed edge, inserting the local dihedral angle or zero.
Upstream, the hinge deficit is $2\pi$ minus the sum of dihedral angles. After cell-count collapse on the torus, zero deficit for the base/displacement filter reduces to showing that filtered angle sum equals a displacement-class template, then that each template equals $2\pi$.
proof idea
Term-mode, two steps. First rewrite the left-hand triple sum via the intermediate identity that equates the base/displacement-filtered periodic cell-tet-slot sum to a local pair-displacement filtered angle sum for the edge. Then apply the evaluation lemma that that local pair-displacement filter sum equals the symbolic Freudenthal local displacement angle-sum template at edge.disp. No further casework on lattice sizes or edge types appears here.
why it matters
This is the bridge from the periodic filtered triple sum to the finite family of local angle templates. Downstream, the zero-deficit target for the base/displacement-filtered periodic sum is obtained by rewriting with this equality and invoking the seven local displacement-class template identities (the remaining $2\pi$ content). The module doc frames that package as what is needed to instantiate the physical six-tet cubic Dirichlet model on the periodic Freudenthal torus, tying discrete Regge-style hinge geometry to the continuum Dirichlet action limit used in the gravity sector. Closing the three explicit template-to-$2\pi$ identities finishes the filtered zero-deficit obligation after cell-count collapse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.