FreudenthalLocalThreeAngleIdentityTarget
plain-language theorem explainer
Packages the three local dihedral-angle sum identities on the canonical Freudenthal cube triangulation that underwrite the seven positive displacement classes. Axis slots share one full-turn identity, face-diagonal slots another, and the body-diagonal slot a third. Gravity and Regge workers cite this Prop as the obligation that the seven-class angle template reduces to. Pure definition: a conjunction of three real equalities, no proof content.
Claim. The proposition that the six local Freudenthal dihedral angles $\theta_f$ (one per tetrahedral edge slot $f\in\{0,\ldots,5\}$ on the canonical one-cube squared-edge tuple) satisfy $2\theta_0+2\theta_3+2\theta_5=2\pi$, $2\theta_1+2\theta_4=2\pi$, and $6\theta_2=2\pi$.
background
The module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not grant the physical Dirichlet equality for free; it packages the exact theorem obligations needed to instantiate that model on a periodic Freudenthal torus.
The local dihedral angle $\theta_f$ is the 3D squared-edge dihedral angle of slot $f$ evaluated on the canonical one-cube Freudenthal squared-edge tuple. The six slots fall into three geometric families: axis, face-diagonal, and body-diagonal. Around a typed periodic edge these families close with multiplicities 2+2+2, 2+2, and 6 respectively, each summing to a full turn $2\pi$.
Those three closures are the geometric content of the seven positive displacement-class angle templates used later in the Dirichlet/Regge comparison.
proof idea
Definition only: the body is the conjunction of the three real equalities written above, with each $\theta_f$ expanded as freudenthalLocalDihedralAngle f. No tactics, no lemmas applied. Downstream theorems unfold this Prop and discharge the three conjuncts from the explicit closed-form values of the six local angles.
why it matters
This Prop is the bottleneck obligation for the local angle side of the physical six-tet cubic Dirichlet instance. The companion theorem freudenthalLocalThreeAngleIdentityTarget asserts that the three identities close exactly, by substituting the closed-form local dihedral values. From that hypothesis, freudenthalLocalDispAngleTemplateTarget_of_threeAngleIdentities reduces all seven displacement-class angle-template identities to these three distinct local closures (axis classes share the first, face-diagonal the second, body-diagonal the third).
In the broader RS gravity chain this is scaffolding for matching the periodic Freudenthal Regge action to a physical finite-difference Dirichlet form on the cubic lattice, not a forcing-chain (T0–T8) step. It sits downstream of the Freudenthal length-chain and Regge cubic-lattice limit imports, and upstream of the encoded-periodic Dirichlet target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.