CanonicalPeriodicBaseDispFilteredLocalSlotTripleAngleSumTarget
plain-language theorem explainer
Base-and-displacement filtered triple-sum target: around every periodic edge on an Nx×Ny×Nz Freudenthal torus, local dihedral angles over matching (cell, tet, slot) incidences sum to 2π. Discrete-gravity workers cite it as the flatness obligation for the six-tet cubic Dirichlet model. Pure Prop packaging: displacement match is a finite local-slot filter; incidence reduces to a base-vertex offset equation.
Claim. For positive integers $N_x,N_y,N_z$, every periodic edge $e$ on the Freudenthal torus of size $N_x\times N_y\times N_z$ satisfies: the sum over all periodic tetrahedra and over local edge slots $f\in\{0,\ldots,5\}$ whose cube-edge displacement equals that of $e$, of the local Freudenthal dihedral angle at $f$ when the edge base equals the cell origin shifted by the cube-edge base vertex (else $0$), equals $2\pi$.
background
The module packages exact theorem obligations that instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not give the physical Dirichlet equality for free; it isolates the flatness and correspondence conditions still required.
A periodic Freudenthal torus tiles $\mathbb{Z}/N_x\times\mathbb{Z}/N_y\times\mathbb{Z}/N_z$ by unit cubes, each cut into six tetrahedra. Edges carry a base vertex and one of seven displacement classes (three axes, four face diagonals). For each tetrahedron type and local slot $f\in\mathrm{Fin},6$, a fixed table picks a one-cube edge representative; from that representative one reads a displacement class and a base cube-corner, and a bit-shift map moves the cell origin by that corner.
The target is zero angular deficit: dihedral angles around each edge must sum to a full turn. Filtering by displacement class leaves a finite local-slot table; incidence then collapses to the single base-offset equation. As the doc-comment puts it, this is "the finite table left after the periodic-cell base-offset equation has been isolated."
proof idea
Definition of a proposition, not a proved theorem. The body quantifies over every periodic edge and equates a filtered double sum to $2\pi$. The outer sum runs over all periodic (cell, tet) pairs. The inner Finset retains only those local slots $f$ for which the cube-edge displacement of the local-edge table entry matches the edge displacement. Each retained summand is the local dihedral angle at $f$ if the edge base equals the cell origin bit-shifted by the cube-edge base vertex, else zero.
No tactics fire at the definition site. Downstream discharge rewrites the filtered triple sum into seven local displacement-class angle-template identities, then applies those templates.
why it matters
This Prop is the remaining flatness input for full nonlinear Regge finite-aggregate convergence to Dirichlet energy on the explicit Freudenthal coordinate realization. Downstream, the holds theorem asserts it for the canonical local angles, obtained from the seven local displacement-class templates. A further implication lifts it to the coarser displacement-filtered target, because within a fixed displacement class full edge equality reduces to the base-offset equation.
In the Recognition Science gravity stack this is a gate on the discrete-to-continuum bridge: Regge action on the six-tet cubic lattice must recover continuum Dirichlet energy. Ambient forcing (T7 eight-tick octave, T8 $D=3$) explains why a cubic 3-space lattice is the scaffold; the declaration itself is only the local angle-sum flatness obligation on that scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.