freudenthalLocalDihedralAngle_eq
plain-language theorem explainer
On the canonical Freudenthal tetrahedron the six local dihedral angles evaluate exactly to π/4, π/2, π/3, π/2, π/2, π/4. Anyone checking the six-tet cubic Dirichlet angle-sum identities cites this. The proof is a six-way case split that rewrites each angle through the known cofactor cosines and applies arccos inversion.
Claim. For each edge slot $f \in \{0,\ldots,5\}$ of the canonical one-cube Freudenthal tetrahedron, the local dihedral angle equals $\pi/4$, $\pi/2$, $\pi/3$, $\pi/2$, $\pi/2$, $\pi/4$ respectively.
background
The module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
A local dihedral angle is obtained by feeding squared edge lengths into the Cayley–Menger cofactor cosine and taking $\arccos$. Concretely, dihedralAngle3Sq is $\arccos$ of the cofactor cosine on a six-tuple of squared edges, and the local Freudenthal angle is that functional evaluated on the canonical one-cube Freudenthal squared-edge data.
The immediate prior result supplies the six exact cosines: $\sqrt{2}/2$, $0$, $1/2$, $0$, $0$, $\sqrt{2}/2$. The present statement lifts those cosines to the corresponding angles in $[0,\pi]$.
proof idea
Case-split on the six edge slots. In each case unfold the local angle definition to $\arccos$ of the cofactor cosine, rewrite the cosine by the exact cosine theorem, then invert: for the $\pi/4$ and $\pi/3$ slots use $\arccos(\cos\theta)=\theta$ with the standard positivity bounds; for the three right-angle slots use $\arccos(0)=\pi/2$.
why it matters
Feeds directly into the three local Freudenthal angle-identity target, whose doc-comment states that those identities "close exactly." That target is one of the packaged obligations linking the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. Exact $\pi/4$, $\pi/2$, $\pi/3$ values are the classical dihedral spectrum of the Freudenthal cube triangulation; locking them in Lean removes a floating geometric hypothesis from the Regge-to-Dirichlet correspondence on the cubic lattice. Within the broader gravity stack this sits under the periodic Freudenthal and Regge cubic-lattice limit imports, not under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.