PeriodicEdge5
plain-language theorem explainer
Specializes the periodic Freudenthal edge type to the canonical 5×5×5 lattice used throughout Track 1.D. Gravity and stencil-coefficient authors cite it whenever they quantify over edges on that torus. The body is a one-line abbreviation of the three-parameter edge constructor at N = 5.
Claim. Write $\mathrm{PeriodicEdge}_5$ for the type of edges of the $5\times 5\times 5$ periodic Freudenthal torus, i.e. the specialization $\mathrm{PeriodicEdge}(5,5,5)$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. Track 1.B's conformal ansatz puts one scalar potential on each vertex and averages endpoints to vary edge lengths; that scalar slice cannot carry pure shear or transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations separately from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
The ambient discrete geometry is the periodic Freudenthal torus. Spatial dimension is forced to $D = 3$ (T8/T9). The concrete working lattice for coefficient certificates is the $5\times 5\times 5$ torus: vertices are triples in $(\mathbb{Z}/5\mathbb{Z})^3$, and edges are base-vertex plus displacement data. Upstream geometry imports supply the Regge first-variation hinge measure and the periodic torus constructors that this abbreviation pins to $N = 5$.
proof idea
Definitional abbreviation only: expand to PeriodicEdge 5 5 5. No proof obligations, tactics, or lemmas.
why it matters
Every axis-stencil and explicit-fiber identity in the $N = 5$ Freudenthal coefficient certificates is typed over this edge sort. Downstream it appears in endpoint-comparability on axis edges, the residual coefficient sum, soundness of the corrected three-axis stencil, and the global explicit-fiber LHS expansions (mixed pair sums and scaled pair expansions). Those results close the RHS half of explicit-fiber axis-stencil soundness and package the LHS for the tensor/shear track. Without a fixed $N = 5$ edge type, the discrete Regge variation sums that separate shear from conformal modes cannot be stated uniformly. Framework landmarks in play: $D = 3$ spatial dimensions and the discrete geometry underlying the gravity sector of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.