CanonicalPeriodicLocalEdgeOfFilteredEdgeAngleSumTarget
plain-language theorem explainer
For every typed edge on a periodic Nx×Ny×Nz Freudenthal torus, the sum of angle contributions from tetrahedra selected by the local-edge-of witness equals 2π. Regge and discrete-gravity workers cite it as the finite-star flatness obligation. It is a Prop packaging that geometric target, not a proved identity; proofs that need zero edge defect take it as a hypothesis.
Claim. For positive integers $N_x,N_y,N_z$, the proposition asserts: for every periodic edge $e$ on the $N_x\times N_y\times N_z$ Freudenthal torus, $$\sum_{T:\,\mathrm{localEdgeOf}(e,T)} \theta(e,T) = 2\pi,$$ where the sum runs over periodic tetrahedra $T$ related to $e$ by the local-edge-of witness and $\theta(e,T)$ is the typed edge angle contribution of that pair.
background
The module connects the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not give the physical Dirichlet equality for free; it packages the exact geometric obligations still required to instantiate that model on the torus.
A periodic edge is an edge class on the $N_x\times N_y\times N_z$ lattice torus; a periodic tet is a cell in the six-tet cubic Freudenthal decomposition, lifted periodically. The local-edge-of witness filters those cells whose translated local Freudenthal edge matches a given typed periodic edge. The angle contribution is the dihedral term attached to that edge-cell pair in the discrete Regge action.
The named target is the classical discrete-flatness condition: around every edge the incident angles sum to a full turn. The doc-comment calls this the purely geometric finite-star form of the incident angle-sum target; remaining work is to classify which translated local edges equal a given typed periodic edge.
proof idea
Definitional packaging only. The body is a universal quantifier over periodic edges together with a filtered Finset sum of typed angle contributions set equal to $2\pi$. No tactics and no lemmas are applied; the Prop is the obligation itself. Downstream results either assume it or transport it to an equivalent filter (slot-witness form) by relating the two incidence predicates.
why it matters
Two same-module parents consume it. The slot-witness implication theorem states that this local-edge-of filtered target implies the slot-witness filtered angle-sum target, so bookkeeping that indexes by slots can inherit the geometric hypothesis. The large continuum-limit theorem takes it as the remaining flatness input: under local stencil correspondence and this filtered angle sum, the variable-weighted finite Regge aggregate (spacing-scaled, divided by spacing norm squared) tends to the Dirichlet energy of the explicit Freudenthal realization.
In the Recognition gravity path this sits between the periodic Freudenthal scaffold and the physical six-tet cubic Dirichlet model. The $2\pi$ sum is zero edge defect, which lets the nonlinear Regge action reduce to pure gradient energy rather than a curvature source. It is an interface obligation, not a closed forcing-chain step (T0-T8); closing it is geometric classification of the finite star, not a new physical constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.