freudenthalLocalDihedralAngle
plain-language theorem explainer
Local dihedral angle at each of the six edge slots of a Freudenthal tetrahedron in the unit cube, read off the canonical squared-edge lengths (unit steps, face diagonals, body diagonal). Discrete-gravity and Regge workers cite it as the fixed geometric weight in every periodic cell/tet contribution to a typed edge angle sum. The body is a one-line composition of the squared-edge dihedral map with the Freudenthal edge table.
Claim. For each tetrahedral edge slot $f \in \{0,\ldots,5\}$, the local Freudenthal dihedral angle is $\theta(f)=\arccos\bigl(\cos_{\mathrm{dih}}(a_{\mathrm{F}},f)\bigr)$, where $a_{\mathrm{F}}$ is the canonical squared-edge $6$-tuple of a Freudenthal tetrahedron in the unit cube (squared lengths $1,2,3,1,2,\ldots$: three unit steps, two face diagonals, one body diagonal).
background
The module packages the 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; it wires the encoded periodic scaffold to the model target.
A Freudenthal tetrahedron in the unit cube has a fixed squared-edge $6$-tuple: three edges of squared length $1$ (axis steps), two of squared length $2$ (face diagonals), and one of squared length $3$ (body diagonal). The upstream map `dihedral angle from squared edges' returns $\arccos$ of the cosine built from that Cayley–Menger edge data at a chosen slot $e\in\mathrm{Fin},6$.
In the Regge picture, curvature lives at hinges (edges). The local dihedral angle is the geometric ingredient of each cell/tetrahedron pair's contribution to the angle sum around a typed periodic edge.
proof idea
Pure definition, not a proof. It applies the squared-edge dihedral-angle map to the canonical Freudenthal squared-edge table and evaluates at the slot index $f$. No tactics, no lemmas beyond that composition: the angle is $\arccos$ of the dihedral cosine of those fixed edge lengths at $f$.
why it matters
This is the constant geometric weight inside every filtered cell/tet/slot sum that builds the periodic typed-edge angle-sum targets. Downstream, the base/displacement-filtered triple sum is identified with the symbolic Freudenthal local-angle template for the edge's displacement class, after which the remaining zero-deficit work is three explicit template identities to $2\pi$.
It feeds the flat-field preflight that the per-tetrahedron angle contribution equals the certified typed-edge contribution of the periodic angle-sum chain, and the implication from the local-slot triple-sum target to the direct typed cell/tet angle-sum target. In the broader RS gravity stack this is scaffolding for the physical Dirichlet instance on the six-tet cubic lattice, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.