canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds
plain-language theorem explainer
On any nonzero periodic Freudenthal lattice, every typed edge has total dihedral angle sum exactly 2π when angles are the canonical local Freudenthal values. Discrete-gravity and Regge analysts cite this as the certified flat-point angle-sum identity before deficit or Hessian work. The proof is a one-line lift from the local slot-triple angle-sum certificate.
Claim. For all positive integers $N_x,N_y,N_z$ and every periodic edge $e$ of the $N_x\times N_y\times N_z$ Freudenthal torus, the sum over all periodic cell/tetrahedron pairs of the canonical typed edge-angle contribution of $e$ equals $2\pi$.
background
This module packages the exact obligations that turn an encoded periodic Freudenthal torus into an instance of the physical six-tet cubic Dirichlet model. It does not give the Dirichlet equality for free; it certifies the geometric side conditions the model needs.
The predicate proved here is the direct typed-cell version of the canonical periodic angle-sum target: for every periodic edge, sum the canonical typed edge-angle contributions over all periodic tetrahedra and demand equality with $2\pi$. Working with typed pairs (cell, localTet) removes the Fin tetrahedron encoder from later incidence arguments.
In Regge calculus the deficit on an edge is $2\pi$ minus that angle sum. Vanishing deficit at the flat assignment is therefore exactly this identity. Upstream scaffolding supplies the local slot-triple form of the same sum; the present statement is the direct typed packaging used by the deficit and symbol-preflight layers.
proof idea
One-line term proof. Apply the reduction lemma that builds the direct typed edge angle-sum target from a local slot-triple angle-sum target, feeding it the already-proved certificate canonicalPeriodicLocalSlotTripleAngleSumTarget_holds at the same lattice sizes $N_x,N_y,N_z$. No new geometric computation occurs here.
why it matters
This is the certified flat-point angle-sum link in the periodic Freudenthal chain that feeds the physical six-tet cubic Dirichlet instance. Downstream, canonicalPeriodicTypedEdgeAngleSumTarget_holds re-packages it with the Fin-encoded typed target, and the Regge TT symbol preflight uses it twice: edgeAngleContributionOfField_flat identifies flat-field contributions with the canonical typed contributions, and deficitOfField_flatEdgeField concludes that every deficit vanishes at the flat edge field by reusing this sum ("the geometry is not re-derived here").
In the gravity stack this is the discrete flatness certificate before Hessian, Dirichlet-action, and continuum-limit arguments on the cubic lattice. It sits under the D=3 spatial forcing (T8) and the eight-tick/octave discrete geometry that the Freudenthal triangulation realizes, without itself deriving those landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.