freudenthalLocalDispAngleSumTemplate
plain-language theorem explainer
Defines the symbolic angle-sum template on the seven positive cubic displacement classes for the local Freudenthal six-tet geometry. Axis classes get twice the sum of dihedral slots 0, 3, 5; face-diagonal classes get twice slots 1 and 4; the body diagonal gets six times slot 2. Gravity and Regge-calculus workers cite it when collapsing periodic cell/tet/slot sums to a finite list of local identities. The body is a pure case split on Fin 7.
Claim. For each positive displacement class $d \in \{0,\ldots,6\}$, the local angle-sum template $T(d)$ is: $T(d)=2\theta_0+2\theta_3+2\theta_5$ if $d\in\{0,1,2\}$ (axis classes); $T(d)=2\theta_1+2\theta_4$ if $d\in\{3,4,5\}$ (face-diagonal classes); $T(d)=6\theta_2$ if $d=6$ (body-diagonal class), where $\theta_f$ is the local Freudenthal dihedral angle at tetrahedral edge slot $f$ on the canonical one-cube squared-edge tuple.
background
The module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not freely assert the physical Dirichlet equality; it isolates the remaining theorem-shaped targets.
The building block is the local Freudenthal dihedral angle $\theta_f$ at tetrahedral edge slot $f\in\mathrm{Fin},6$, evaluated via the squared-edge dihedral formula on the canonical one-cube Freudenthal triangulation. Positive lattice displacements fall into seven classes (three axis, three face-diagonal, one body-diagonal). Around a typed periodic edge of a fixed class, only certain local pairs (cell, tet, slot) contribute.
This definition records, class by class, the exact linear combination of those local dihedrals that the filtered pair sum is expected to equal. Downstream work then only needs $T(d)=2\pi$ for each class.
proof idea
Pure definition by cases on $\mathrm{Fin},7$. Each branch is an explicit real linear combination of the six local dihedral values $\theta_f=\mathrm{freudenthalLocalDihedralAngle},f$. No lemmas are applied; the coefficients (two copies of slots 0,3,5 for axis classes; two of 1 and 4 for face diagonals; six of slot 2 for the body diagonal) are hard-coded from the local-pair fiber geometry.
why it matters
This template is the collapse target for the base/displacement-filtered periodic cell/tet/slot angle sum: that filtered sum equals $T(d)$ exactly, so the remaining zero-deficit work is only the seven identities $T(d)=2\pi$. Those seven reduce to three distinct local Freudenthal angle identities (axis, face, body), which form the whole $2\pi$ content of the filtered zero-deficit target after periodic cell-count collapse.
It therefore sits on the path from the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model, packaging the local-angle bookkeeping that Regge-style hinge sums need before continuum or Dirichlet limits. Framework-wise it is geometry/Regge scaffolding inside the gravity domain, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.