freudenthalLocalPairAngle
plain-language theorem explainer
Assigns to each local Freudenthal (tetrahedron, edge-slot) pair the dihedral angle of its edge-slot. Gravity and discrete-Regge calculations cite it when collapsing periodic six-tet angle sums onto displacement classes. The body is a one-line projection onto the slot component.
Claim. For a local pair $(t,s)$ with tetrahedron index $t\in\{0,\ldots,5\}$ and edge-slot $s\in\{0,\ldots,5\}$, the Freudenthal local angle is the real dihedral angle attached to slot $s$.
background
The module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not claim the physical Dirichlet equality for free; it isolates the finite local data left after the periodic-cell base-offset equation is solved.
A local pair is an element of $\mathrm{Fin},6\times\mathrm{Fin},6$: one of six tetrahedra in the cubic Freudenthal decomposition together with one of six edge-slots on that tet. Positive displacement classes (axis, face-diagonal, body-diagonal) group these pairs; a companion template records how many copies of each slot angle enter each class.
The angle itself is the local dihedral angle of the chosen edge-slot. Downstream sums over displacement fibers or filters replace full periodic cell/tet/slot triple sums by these local angles once the unique periodic cell solving the base-offset equation is supplied.
proof idea
Definitional one-liner: project the pair to its second factor (the edge-slot) and apply the already-defined local dihedral-angle map on slots. No tactics, no lemmas beyond that projection.
why it matters
This is the angle atom in the local-pair calculus that feeds three in-module sum identities: the exact fiber sum equating the displacement-fiber angle total to the symbolic template; the filter form of the same identity; and the collapse of the base/displacement-filtered periodic cell/tet/slot triple sum onto the one-cube local-pair displacement fiber sum (via uniqueness of the periodic cell solving the base-offset equation).
In the broader Recognition gravity stack those identities are the bridge from the encoded periodic Freudenthal torus scaffold to the physical finite-difference Dirichlet target on the six-tet cubic lattice. They sit downstream of the Regge/cubic-lattice limit and length-chain endpoint certificates imported by the module, and they keep the discrete angle bookkeeping exact before any continuum or continuum-limit claim is asserted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.