FreudenthalLocalDispAngleTemplateTarget
plain-language theorem explainer
Defines the residual local angle obligation after periodic cell-count collapse: each of the seven positive Freudenthal displacement classes has local angle-sum template exactly 2π. Gravity and Regge-lattice workers cite it as the pure angular half of the base/displacement-filtered zero-deficit target. It is a bare Prop alias, not a proved statement; discharge goes through the three distinct axis/face/body angle identities.
Claim. For every positive Freudenthal displacement class $d \in \{0,\ldots,6\}$, the local displacement angle-sum template of $d$ equals $2\pi$.
background
The module packages exact theorem obligations that instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not give the physical Dirichlet equality for free; it isolates the geometric identities still needed after the encoded periodic scaffold is in place.
After the periodic cell-count collapse, the remaining zero-deficit content is angular. The seven positive displacement classes on the cubic lattice (axis, face-diagonal, body-diagonal orbits) each carry a local Freudenthal angle-sum template. Axis classes share one identity, face-diagonal classes a second, and the body-diagonal class a third; the seven-fold quantification is therefore redundant once those three identities are known.
In the Regge/Freudenthal setting, a hinge or local slot triple is deficit-free when its angle sum is exactly $2\pi$. This definition is precisely that local $2\pi$ condition, written once per displacement class, and is the whole angular content of the base/displacement-filtered zero-deficit target.
proof idea
Definitional: the body is the universal quantification ∀ d : Fin 7, freudenthalLocalDispAngleSumTemplate d = 2 * Real.pi. No tactics or lemmas are applied at the definition site. Downstream, the seven-fold statement is recovered from the three distinct local identities by fin_cases on d and simplification against the axis, face, and body cases of the template.
why it matters
This Prop is the angular interface between the local Freudenthal geometry and the periodic zero-deficit target used by the physical six-tet cubic Dirichlet instance. The theorem freudenthalLocalDispAngleTemplateTarget_of_threeAngleIdentities reduces it to the three distinct axis/face/body identities; freudenthalLocalDispAngleTemplateTarget then asserts the seven identities for the canonical tetrahedron. From there, canonicalPeriodicBaseDispFilteredLocalSlotTripleAngleSumTarget_of_localDispAngleTemplates lifts the local templates to the base/displacement-filtered periodic zero-deficit target on any nonzero lattice periods $(N_x,N_y,N_z)$.
In the broader gravity stack this sits under the Regge cubic-lattice limit and the Freudenthal length-chain endpoint certificates: once angles sum to $2\pi$ classwise, the filtered local slot triples carry zero deficit, which is the geometric half of matching the physical Dirichlet action on the periodic torus. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is lattice geometry feeding the continuum Dirichlet model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.