freudenthalLocalDispAngleTemplateTarget
plain-language theorem explainer
On the canonical Freudenthal tetrahedron, each of the seven positive displacement-class angle-sum templates equals 2π. Gravity workers wiring the periodic six-tet cubic Dirichlet model to a zero-deficit target cite this local identity pack. The proof is a one-line reduction of the seven classes to three shared angle identities already proved.
Claim. For every displacement class $d \in \{0,\ldots,6\}$, the local Freudenthal angle-sum template attached to $d$ equals $2\pi$.
background
The module packages exact theorem obligations that 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 assembles the local geometric identities the model demands.
After the periodic cell-count collapse, the remaining local content is a family of angle-sum templates indexed by the seven positive displacement classes of the cubic lattice (three axis, three face-diagonal, one body-diagonal). The target proposition asserts that each template sums to a full turn: $\mathrm{template}(d)=2\pi$. Axis classes share one underlying identity, face-diagonals a second, and the body diagonal a third, so the seven statements are not independent.
These local $2\pi$ identities are precisely the angle content of the base/displacement-filtered zero-deficit target used downstream when the periodic Freudenthal scaffold is matched to the physical Dirichlet action.
proof idea
Term-mode one-liner. Apply the reduction lemma that derives the seven-class template target from the three distinct local Freudenthal angle identities (axis, face-diagonal, body-diagonal). Feed that lemma the already-established three-angle identity target. No further casework or arithmetic appears at this site.
why it matters
This is the local $2\pi$ pack that closes the angle side of the base/displacement-filtered zero-deficit obligation on the canonical Freudenthal cell. The sole recorded consumer is the theorem that the canonical periodic base/displacement-filtered local slot triple angle-sum target holds for any positive lattice periods $N_x,N_y,N_z$: that result applies the filtered-target constructor to this theorem.
In the broader gravity stack the identity sits between the periodic Freudenthal torus geometry and the physical six-tet cubic Dirichlet model, feeding Regge-style hinge and length-chain endpoints. It does not itself force $D=3$ or the eight-tick octave; those enter earlier in the forcing chain. What it supplies is the concrete local angle closure needed so the Dirichlet instance is not left as scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.