freudenthalLocalPairDispFiber_angle_sum
plain-language theorem explainer
For each of the seven positive displacement classes on the Freudenthal lattice, the sum of local dihedral angles over the explicit (tetrahedron, edge-slot) fiber equals a fixed symbolic template. Gravity workers instantiating the six-tet cubic Dirichlet model cite this for local angle bookkeeping. Proof is exhaustive case split on the seven classes, then simplification and ring normalization.
Claim. For every positive displacement class $d \in \{0,\ldots,6\}$, $$\sum_{p \in F(d)} \theta(p) = T(d),$$ where $F(d)$ is the explicit local Freudenthal fiber of (tetrahedron, edge-slot) pairs for class $d$, $\theta(p)$ is the local dihedral angle of the edge-slot of $p$, and $T(d)$ is the symbolic angle-sum template for that 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 assert the physical Dirichlet equality for free; it supplies the local identities the model target demands.
Positive edge displacements on the cubic lattice fall into seven classes (three axis, three face-diagonal, one body-diagonal). For each class $d$, an explicit finite set $F(d)$ of local pairs (tetrahedron index in the six-tet cell, edge-slot) is listed by hand. The local angle of a pair is the Freudenthal dihedral angle of its edge-slot. The template $T(d)$ encodes the expected multiplicity: axis classes get two copies each of slots $0,3,5$; face-diagonals two each of $1,4$; the body-diagonal six copies of slot $2$.
The fiber and template are pure combinatorial data; this theorem asserts they match under summation.
proof idea
Case-split on the seven values of $d$. In each branch, unfold the fiber set, the pair-angle map, and the template definition, then normalize the resulting rational combination of dihedral-angle symbols by ring arithmetic. No external lemmas are required beyond the three local definitions; the identity is a finite, fully expanded equality check.
why it matters
The immediate consumer is the filter form of the same identity: the sum of local angles over all pairs whose computed displacement equals $d$ equals $T(d)$. That theorem rewrites through fiber-equals-filter and applies this result. Together they discharge the local-angle side of the bookkeeping that links the periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet target.
In the broader gravity stack this sits under the Regge/cubic-lattice limit path: correct local dihedral multiplicities are a prerequisite for matching the Dirichlet action on the encoded torus. The module header is explicit that the physical Dirichlet equality is not free; this is one of the exact obligations that must hold before that equality can be claimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.