PeriodicVertex5
plain-language theorem explainer
Type alias for the vertex set of the 5×5×5 periodic cubic Freudenthal torus: triples in Fin 5 × Fin 5 × Fin 5. Gravity and SevenGaps edge-tensor code cites it as the domain for vertex potentials, face corners of the witness square, and endpoint averaging of conformal edge strains. The body is a one-line specialization of the generic periodic Vertex type.
Claim. Write $\mathrm{PeriodicVertex}_5$ for the set of vertices of the $5\times 5\times 5$ periodic cubic lattice, i.e. $(\mathbb{Z}/5\mathbb{Z})^3$ (equivalently $\mathrm{Fin}\,5 \times \mathrm{Fin}\,5 \times \mathrm{Fin}\,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 at each vertex and induces edge-length changes by averaging the two endpoints; that scalar slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction for the conformal ansatz.
Upstream, periodic cubic vertices are the product type $\mathrm{Fin},N_x \times \mathrm{Fin},N_y \times \mathrm{Fin},N_z$. Specializing all three periods to 5 yields the concrete lattice used for the N=5 periodic Freudenthal edge surface and for typed edge/vertex counts in the SevenGaps edge-tensor development.
proof idea
Definitional abbreviation only: expand to the upstream Vertex constructor at periods $(5,5,5)$. No proof obligations.
why it matters
Pins the discrete geometry for the concrete N=5 periodic edge surface that carries the tensor/shear scaffold. Downstream, the four corners of the witness square (face vertices A–D) are elements of this type; the typed edge equivalence identifies edges with base-vertex × displacement pairs; and the conformal log-subspace endpoint form quantifies over potentials $\varphi : \mathrm{PeriodicVertex}_5 \to \mathbb{R}$ realizing edge strains by endpoint averages. Without a fixed finite torus, those SevenGaps statements cannot be stated as closed Lean objects. It is scaffolding infrastructure for separating shear from the conformal slice, not a dynamical claim about gravity or the forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.