CanonicalPeriodicLocalSlotTripleAngleSumTarget
plain-language theorem explainer
Defines the flatness obligation for a periodic Freudenthal torus: around every typed periodic edge, the sum of local Freudenthal dihedral angles from matching cell/tet/slot triples equals 2π. Gravity and Regge-limit arguments cite it as the explicit angle-sum hypothesis feeding the Dirichlet continuum limit. It is a pure Prop abbreviation (triple sum with zero on non-matches), not a proved statement.
Claim. For positive integers $N_x,N_y,N_z$, the following holds: for every typed edge $e$ on the periodic Freudenthal torus of size $(N_x,N_y,N_z)$, $$\sum_{(\mathrm{cell},\tau)}\sum_{f=0}^{5}\mathbf{1}_{e=\mathrm{localEdge}(\mathrm{cell},\tau,f)}\,\theta_f = 2\pi,$$ where $\theta_f$ is the canonical local Freudenthal dihedral angle at slot $f$, and the indicator is $1$ only when the translated local edge equals $e$.
background
The module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not give the continuum Dirichlet equality for free; it names the discrete flatness and stencil hypotheses that later limit theorems consume.
A Freudenthal cube triangulation splits each unit cube into six tetrahedra. Each tet has six local edge slots; localEdgeOf sends a base cell, tet index, and slot to a typed periodic edge (base vertex plus displacement class on the torus). The local dihedral angles $\theta_f$ are the fixed geometric angles of that triangulation.
In Regge calculus, continuum flatness at an interior edge is the deficit-angle condition: the sum of dihedral angles around the edge equals $2\pi$. This definition states that condition by ranging over all cell/tet pairs and all six slots, contributing $\theta_f$ only when the slot realizes the given edge and zero otherwise.
proof idea
No proof: this is a Prop-valued definition. The body is a universal quantifier over typed periodic edges whose right-hand side is the constant $2\pi$, and whose left-hand side is a double sum (over periodic tets and Fin 6 slots) of a piecewise term that returns the local Freudenthal dihedral angle on a match and zero otherwise. Downstream lemmas discharge or transport the predicate; the definition itself only names the target.
why it matters
This is the explicit triple-sum flatness hypothesis used throughout the physical six-tet cubic Dirichlet instance. The theorem canonicalPeriodicLocalSlotTripleAngleSumTarget_holds asserts it for the canonical Freudenthal angles (via the displacement-filtered form). The transport lemma canonicalPeriodicDirectTypedEdgeAngleSumTarget_of_localSlotTriple shows it implies the direct typed cell/tet angle-sum target.
Most importantly, the full nonlinear Regge finite-aggregate limit
...tendsto_dirichlet_of_freudenthalRealization_localSlotTripleAngleSum
takes this predicate as the remaining flatness input and concludes Dirichlet-energy convergence of the variable-weighted Regge probe. In the Recognition gravity stack that is the bridge from discrete six-tet geometry on the periodic torus to the continuum Dirichlet action that the physical model targets. It sits downstream of the periodic Freudenthal scaffold and upstream of the Regge-to-Dirichlet continuum step; it does not itself invoke the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.