canonicalPeriodicTypedEdgeAngleContribution
plain-language theorem explainer
Per cell/tetrahedron contribution to the dihedral angle sum around a typed edge on the periodic Freudenthal torus. Returns the local Freudenthal dihedral angle when the edge occupies a slot in that tetrahedron, and zero otherwise. Regge and gravity proofs cite it as the summand in the flat (zero-deficit) angle-sum identity. Defined by a match on the optional edge-slot lookup.
Claim. Fix positive integers $N_x,N_y,N_z$. For a typed periodic edge $e$ and a periodic cell/tetrahedron pair $(\mathrm{cell},\tau)$, the contribution equals the local Freudenthal dihedral angle $\theta_F(f)$ if $e$ occupies a local slot $f$ in that pair, and equals $0$ if $e$ is not incident to the pair.
background
The module packages 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 ties the encoded periodic scaffold to the model target.
A typed periodic edge lives on the $N_x\times N_y\times N_z$ Freudenthal torus. A periodic cell/tetrahedron pair indexes one tetrahedron in the six-tet cubic decomposition of a lattice cell. The optional slot lookup asks whether that edge appears in a local face/slot of the tetrahedron; if so, the contribution is the corresponding local Freudenthal dihedral angle, else zero.
In Regge calculus the curvature deficit at an edge is $2\pi$ minus the sum of dihedral angles of incident tetrahedra. The flat (zero-deficit) case therefore requires that sum to equal $2\pi$. This definition is the typed per-pair summand used to state that identity without anonymous finite edge encoders.
proof idea
Definition by case analysis, not a theorem. Match the optional slot of the typed edge inside the given cell/tetrahedron pair. On some f, return the local Freudenthal dihedral angle at slot $f$. On none, return $0$. No lemmas are applied; the body is the lookup-and-evaluate rule that later angle-sum targets sum over.
why it matters
This is the typed summand for the canonical periodic Freudenthal zero-deficit angle-sum chain. Downstream, the direct typed target asserts that summing these contributions over all cell/tetrahedron pairs yields $2\pi$ for every typed edge. Incident-filtered and local-slot-triple targets reduce to that direct form by showing nonincident pairs contribute zero.
Analysis lemmas identify the flat edge-field contribution with this definition, then reuse the certified angle-sum chain to prove every deficit vanishes at the flat assignment. That flat-point fact is preflight for Regge TT-symbol work on the periodic lattice.
In the broader Recognition gravity stack this sits inside the six-tet cubic Dirichlet instance: packaging the geometric obligations that connect the periodic Freudenthal scaffold to the physical finite-difference Dirichlet model, rather than asserting continuum gravity identities outright.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.