CanonicalPeriodicTypedEdgeAngleSumTarget
plain-language theorem explainer
For every typed periodic edge on an Nx×Ny×Nz Freudenthal torus, the sum of canonical local angle contributions over all tetrahedra equals 2π. Regge and discrete-gravity workers cite this as the typed-edge flatness (zero-deficit) obligation. It is a Prop definition: pure packaging of that universal equation, with no separate proof body.
Claim. For positive integers $N_x,N_y,N_z$, every periodic edge $e$ on the $N_x\times N_y\times N_z$ Freudenthal torus satisfies $\sum_{\tau}\theta_{\mathrm{can}}(e,\tau)=2\pi$, where the sum runs over all periodic tetrahedra via the finite-index tetrahedron encoding and $\theta_{\mathrm{can}}$ is the canonical typed edge-angle contribution at each incident tetrahedron.
background
This module packages the exact obligations needed to 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 inputs that still must be discharged.
A periodic Freudenthal torus is a cubic lattice with periodic identification in three axes, triangulated into Freudenthal tetrahedra. Edges are typed periodic edges; tetrahedra are the periodic tets of that complex. The canonical typed edge-angle contribution is the local dihedral (Freudenthal) angle that a given tet contributes at a given edge.
In Regge calculus, vanishing deficit means the sum of those angles around an edge is exactly $2\pi$. The present definition is the typed-edge form of that zero-deficit target: the anonymous finite edge encoder is removed so later proofs only classify incident cell/tet slots of each typed edge and evaluate the angles.
proof idea
Definitional packaging only. The body is the Prop $\forall e,;\sum_{\tau}\theta_{\mathrm{can}}(e,\mathrm{decode}(\tau))=2\pi$ over typed periodic edges and the finite tetrahedron index type. No tactics or lemmas are applied at this declaration; discharge happens downstream via the direct typed-cell form and the holds theorem for canonical Freudenthal angles.
why it matters
This is the flatness hypothesis that the full nonlinear Regge finite-aggregate theorem consumes: the Dirichlet-energy limit from the explicit Freudenthal coordinate realization is stated with remaining flatness input equal to this typed-edge angle-sum target.
It sits in a short implication chain. The direct typed-cell/tetrahedron angle-sum target implies this encoded form (reindexing over the tet finite encoder). This form in turn implies the canonical zero-deficit target on anonymous finite-index edges. A holds theorem asserts the target for canonical Freudenthal local angles by routing through the direct typed version.
In the Recognition gravity stack, that closes the geometric side of the six-tet cubic Dirichlet instance: once local stencil correspondence and this angle sum are in hand, the Regge aggregate can tend to the continuum Dirichlet energy on the periodic torus. It is scaffolding for the physical model, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.