Vertex
plain-language theorem explainer
Periodic cubic vertices are triples of modular indices on a finite $N_x\times N_y\times N_z$ grid. Anyone building the periodic Freudenthal torus, discrete Regge data, or simplicial ledger edge lengths cites this type. It is a pure type abbreviation equating the vertex sort to a product of three finite ordinals, with no proof obligations.
Claim. For natural numbers $N_x,N_y,N_z$, a periodic cubic vertex is an element of $\mathrm{Fin}\,N_x \times \mathrm{Fin}\,N_y \times \mathrm{Fin}\,N_z$.
background
The Periodic Freudenthal Torus module supplies the scalable target shape for an arbitrary periodic Freudenthal tiling. It does not yet pin a concrete finite mesh; it defines typed periodic vertices, edges, and tetrahedra, and shows that any finite triangulation encoding this model carries the global incidence-edge-slot partition required by the nonlinear Regge first-variation theorem.
A vertex here is simply a lattice site on the three-torus: one modular coordinate along each spatial axis. Downstream constructions (bitwise cube displacements, bone incidence for Regge data, edge lengths from ledger potentials) all quantify over this product type. The only import is the non-periodic Freudenthal cube triangulation, which supplies the local combinatorial pattern being periodized.
proof idea
Pure definitional abbreviation: the vertex sort is identified with the Cartesian product of three Fin types. No tactics, no lemmas, no proof body.
why it matters
This is the carrier type for the entire periodic torus geometry stack. Local siblings (addBits, addVertexBits, injectivity lemmas) move sites by cube-corner bit patterns on this type. Downstream, ReggeData takes an abstract vertex sort whose concrete instance is often this product; the simplicial ledger reads edge lengths from potentials on these sites; cosmology's passive-mode decomposition counts vertex ground states against the forced $2^D=8$ octave. In the RS forcing chain the eight-tick period and $D=3$ (T7, T8) make a cubic three-torus the natural discrete spatial skeleton; this abbreviation is the typed handle for that skeleton while the remaining work (a finite encoder into Fin nV, Fin nE, Fin nT) stays isolated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.