freudenthalLocalThreeAngleIdentityTarget
plain-language theorem explainer
The three local dihedral-angle sum identities for the canonical Freudenthal tetrahedron hold exactly: axis, face-diagonal, and body-diagonal classes each close to a full turn. Gravity and Regge-calculus workers cite it when collapsing seven displacement-class angle templates to three geometric identities. The proof substitutes the six exact local angles and finishes by ring arithmetic.
Claim. The three local Freudenthal angle identities hold: $2\theta_0 + 2\theta_3 + 2\theta_5 = 2\pi$ (axis classes), $2\theta_1 + 2\theta_4 = 2\pi$ (face-diagonal classes), and $6\theta_2 = 2\pi$ (body-diagonal class), where $\theta_f$ is the local dihedral angle of face slot $f\in\{0,\ldots,5\}$ on the canonical Freudenthal tetrahedron.
background
This 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 records the geometric identities the scaffold must satisfy.
The local dihedral angles of the canonical Freudenthal tetrahedron are known exactly: $\theta_0=\pi/4$, $\theta_1=\pi/2$, $\theta_2=\pi/3$, $\theta_3=\pi/2$, $\theta_4=\pi/2$, $\theta_5=\pi/4$. The three-angle target groups the six face slots by the seven positive displacement classes of the cubic lattice: axis classes share the first identity, face-diagonal classes the second, and the single body-diagonal class the third.
Upstream, freudenthalLocalDihedralAngle_eq supplies those six closed values. The identities are the geometric content behind the angle-template layer of the Regge/Dirichlet correspondence on the encoded periodic Freudenthal torus.
proof idea
Unfold the target proposition into its three conjuncts. Instantiate the exact local-angle lemma at each of the six face indices $f=0,\ldots,5$, obtaining $\pi/4$, $\pi/2$, $\pi/3$, $\pi/2$, $\pi/2$, $\pi/4$ respectively. For each conjunct, rewrite the angle symbols by those values and discharge the resulting numerical identity with ring:
- axis: $2(\pi/4)+2(\pi/2)+2(\pi/4)=2\pi$;
- face-diagonal: $2(\pi/2)+2(\pi/2)=2\pi$;
- body-diagonal: $6(\pi/3)=2\pi$.
No geometric argument beyond the already-proved angle table is required.
why it matters
This closes the three local Freudenthal angle identities that underlie all seven positive displacement-class angle templates. Downstream, freudenthalLocalDispAngleTemplateTarget is obtained in one step by applying the reduction lemma that says the seven templates follow from these three identities.
In the broader gravity stack, those templates feed the physical six-tet cubic Dirichlet instance on the periodic Freudenthal torus, which is the concrete lattice model linking the encoded torus scaffold to the Dirichlet/Regge action targets. The identities are pure solid-geometry facts about the Freudenthal tetrahedron (dihedral angles $\pi/4$, $\pi/2$, $\pi/3$), so they sit below the dynamical claims and remove a block of scaffolding from the angle-template track of the master theorem hierarchy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.