CanonicalPeriodicDirectTypedEdgeAngleSumTarget
plain-language theorem explainer
Packages the flatness obligation that every positive-displacement periodic edge on an Nx×Ny×Nz Freudenthal torus has total typed dihedral-angle contribution exactly 2π. Gravity and Regge-calculus workers cite it as the encoder-free angle-sum hypothesis feeding the nonlinear Regge-to-Dirichlet continuum limit. It is a Prop definition, not a proved equality.
Claim. For positive integers $N_x,N_y,N_z$, the direct typed edge angle-sum target holds when, for every positive-displacement periodic edge $e$ on the $N_x\times N_y\times N_z$ Freudenthal torus, $\sum_{(\mathrm{cell},t)}\theta(e;\mathrm{cell},t)=2\pi$, where the sum runs over all periodic cell/tetrahedron pairs and $\theta$ is the local Freudenthal dihedral angle of the matched edge slot (or zero if the pair is nonincident).
background
The module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not give the Dirichlet equality for free; it packages the exact obligations needed to instantiate that model on a periodic torus.
A periodic edge is a base vertex plus one of seven positive cube displacements. A periodic tetrahedron is a cubic cell vertex paired with one of the six Freudenthal tets inside that cell. The contribution of one cell/tet pair to an edge is the local Freudenthal dihedral angle of the matched edge slot when the computable slot lookup succeeds, and zero otherwise.
The classical Regge flatness condition asks that the sum of dihedral angles around every interior edge equal $2\pi$ (zero deficit). This definition states that condition directly over typed pairs $(\mathrm{cell},\mathrm{localTet})$, without routing through a Fin tetrahedron encoder.
proof idea
Definitional packaging only: the body is the universal quantification over periodic edges of equality between the finite sum of canonicalPeriodicTypedEdgeAngleContribution and $2\pi$. No tactics or lemmas are applied at this declaration. Downstream theorems discharge it by reducing to a local-slot-triple sum or to an incident-filtered sum (nonincident pairs contribute zero).
why it matters
This is the encoder-free flatness hypothesis used by the full nonlinear Regge continuum-limit theorem ..._tendsto_dirichlet_of_freudenthalRealization_directTypedAngleSum, which takes the direct typed angle-sum target as remaining input and concludes Dirichlet-energy convergence of the weighted finite Regge aggregate.
Sibling bridges show it is equivalent (under the module's incidence lemmas) to the incident-filtered target and to the local-slot-triple target, and that it implies the older typed-edge target with the Fin tetrahedron encoder. The proved theorem canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds asserts the Prop for canonical Freudenthal local angles via the local-slot-triple route.
In the Recognition gravity stack this is the geometric flatness gate between discrete six-tet Regge action on the periodic Freudenthal lattice and the continuum Dirichlet energy that the physical model targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.