CanonicalPeriodicDispFilteredLocalSlotTripleAngleSumTarget
plain-language theorem explainer
A Prop requiring that, on the periodic Freudenthal torus of size Nx×Ny×Nz, every typed edge has local dihedral angles summing to 2π when only displacement-matched tetrahedral slots are counted. Regge/discrete-gravity workers cite it as the flatness obligation for the physical six-tet cubic Dirichlet model. It is pure definitional packaging of a quantified equality; no proof body.
Claim. For $N_x,N_y,N_z\ge 1$, every typed periodic edge $e$ on the $N_x\times N_y\times N_z$ Freudenthal torus satisfies $$\sum_{\mathrm{cell},\mathrm{tet}}\sum_{\substack{f\in\{0,\ldots,5\}\\ \mathrm{disp}(e)=\mathrm{cubeDisp}(\mathrm{slotEdge}(\mathrm{tet},f))}} \mathbf{1}_{e=\mathrm{localEdge}(\mathrm{cell},\mathrm{tet},f)}\,\theta_f = 2\pi,$$ where $\theta_f$ is the canonical local Freudenthal dihedral angle at slot $f$.
background
The module packages exact obligations that turn an encoded periodic Freudenthal torus into an instance of the physical six-tet cubic Dirichlet model. It does not give the Dirichlet equality for free; it names the geometric flatness and correspondence hypotheses still required.
A periodic edge carries a base vertex and a positive displacement class among the 19 one-cube Freudenthal edge types (axis and face-diagonal directions). Each of the six tetrahedra in a cube has six local edge slots; localEdgeOf translates a (cell, tet, slot) triple to a typed periodic edge via the cube edge base and displacement tables. The filter keeps only slots whose cube displacement matches the edge under study, so the triple sum never mixes incompatible direction classes.
The target value $2\pi$ is the continuum flatness condition for dihedral angles around an interior edge in Regge calculus: deficit zero means the discrete metric is locally Euclidean, which is the geometric input that lets nonlinear Regge aggregates tend to a Dirichlet energy.
proof idea
Definitional Prop only: the body is the quantified equality itself (universal over periodic edges, double sum over cells/tets and displacement-filtered local slots, indicator times the canonical local dihedral angle, right-hand side $2\pi$). No tactics, no lemmas applied at this declaration.
why it matters
This is the displacement-filtered flatness hypothesis used by the full nonlinear Regge finite-aggregate limit theorem: that result takes an explicit Freudenthal coordinate realization plus local stencil correspondence and this target, and concludes that the spacing-scaled Regge energy tends to the Dirichlet energy. Downstream, a base-and-displacement filtered target implies this one (within a displacement class, full edge equality reduces to the base-offset equation), and this target implies the raw unfiltered local-slot triple-sum target (mismatched displacements cannot equal the typed edge). A separate theorem asserts the target holds for the canonical Freudenthal local angles. In the gravity stack it is one of the exact obligations that close the periodic six-tet cubic path from discrete Regge data to continuum Dirichlet form, consistent with the $D=3$ spatial setting of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.