freudenthalLocalDispAngleTemplateTarget_of_threeAngleIdentities
plain-language theorem explainer
The seven displacement-class angle-sum identities on the canonical Freudenthal tetrahedron follow from three distinct local dihedral identities (axis, face-diagonal, body-diagonal). Gravity and Regge-lattice workers cite it when collapsing the 2π zero-deficit template after periodic cell-count reduction. The proof is a Fin-7 case split that rewrites each class sum by the matching identity.
Claim. If the three local Freudenthal dihedral identities hold, namely $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), then for every displacement class $d\in\{0,\ldots,6\}$ the corresponding local angle-sum template equals $2\pi$.
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 freely assert the physical Dirichlet equality; it records the theorem targets that close that instantiation.
After periodic cell-count collapse, the remaining local content of the base/displacement-filtered zero-deficit target is a family of seven angle-sum identities, one per positive displacement class: each template must equal $2\pi$. Those seven classes are not independent. Axis displacements share one linear combination of local dihedral angles, face-diagonal displacements share a second, and the body diagonal is a third pure multiple.
The hypothesis packages exactly those three identities in terms of the six local dihedral angles of the canonical Freudenthal tetrahedron. The conclusion is the full seven-class template target used downstream as the whole $2\pi$ content of the filtered zero-deficit condition.
proof idea
Term/tactic hybrid: introduce an arbitrary displacement index $d:\mathrm{Fin},7$, unpack the three-angle hypothesis into its axis, face, and body conjuncts, then fin_cases on $d$. Each of the seven goals simplifies by unfolding the displacement-class angle-sum template and rewriting with the matching conjunct (hAxis, hFace, or hBody). No external lemmas beyond definitional unfolding are required; the reduction is purely combinatorial grouping of the seven classes onto the three identities.
why it matters
Closes the bridge from the three geometric dihedral identities of the Freudenthal tet to the seven-class angle template demanded by the periodic zero-deficit target. The sole direct consumer is freudenthalLocalDispAngleTemplateTarget, which discharges the full template by feeding in the already-proved three-angle package.
In the broader gravity stack this sits inside the physical six-tet cubic Dirichlet instance: connecting the encoded periodic Freudenthal torus scaffold to the physical model obligations (finite-difference Dirichlet action, edge stencils, Hessian/Dirichlet structure). It is local angle bookkeeping after cell-count collapse, not a global curvature or continuum limit statement, but without it the displacement-filtered $2\pi$ content of the zero-deficit target remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.