CanonicalPeriodicIncidentFilteredEdgeAngleSumTarget
plain-language theorem explainer
For every positive-displacement edge on a periodic Freudenthal torus of size Nx×Ny×Nz, the sum of typed dihedral angle contributions over the finite star of incident six-tet cells equals 2π. Regge-calculus and discrete-gravity workers cite this as the flatness obligation stated on the incident filter alone. It is a Prop-valued definition packaging that geometric target, not a proved theorem. Downstream lemmas transport it to the unfiltered typed sum and into the full Regge-to-Dirichlet limit.
Claim. For all integers $N_x,N_y,N_z\ge 1$ and every positive-displacement periodic edge $e$ on the $N_x\times N_y\times N_z$ Freudenthal torus, if one sums the typed edge-angle contribution of $e$ over all periodic tetrahedra incident to $e$, the sum equals $2\pi$.
background
The module connects the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not assert the physical Dirichlet equality for free; it packages the exact theorem obligations needed to instantiate that model on the torus.
A periodic edge is a base vertex together with one of the seven positive cube displacements. A periodic tetrahedron is a pair (cell vertex, index in the six Freudenthal tets of the cube). The translated local-edge map sends each local tet edge slot to a global periodic edge via the cube triangulation table.
The incident filter keeps only those cell/tet pairs for which the typed edge is geometrically incident. In flat Regge calculus the link of an interior edge closes to a full $2\pi$, so the filtered star sum is the natural finite-star flatness target. Nonincident typed pairs contribute zero, which is why the filter is lossless for the angle sum.
proof idea
Definition of a proposition, not a proof. The body universally quantifies over periodic edges and equates the Finset sum of typed edge-angle contributions, restricted to the incident-filtered universe of periodic tetrahedra, with $2\pi$.
No lemmas are applied here. Downstream, the slot-witness filtered target implies this Prop by refining the filter, and this Prop implies the direct (unfiltered) typed angle-sum target because nonincident pairs contribute zero. The full Regge-to-Dirichlet limit theorem consumes it as a named flatness hypothesis.
why it matters
Three same-module parents depend on it. The implication from incident-filtered to direct typed angle-sum target takes it as hypothesis, using that nonincident typed pairs contribute zero. The slot-witness filtered target implies it, so geometric classification of translated local Freudenthal edges can be staged through successively weaker filters. The full nonlinear Regge finite-aggregate theorem (variable-weighted probe, spacing-scaled, Dirichlet-energy form) takes this filtered flatness input together with a local edge-stencil correspondence and the explicit Freudenthal coordinate realization.
In the Recognition gravity stack this is the discrete flatness condition that lets the six-tet cubic Regge action converge to continuum Dirichlet energy on the periodic lattice, closing the scaffold between the encoded Freudenthal torus and the physical Dirichlet model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.