periodicExternalVertexOfIndex5
plain-language theorem explainer
Decodes a flat natural index into a vertex on the 5×5×5 periodic torus under the Track 1.D payload ordering n = (x·5 + y)·5 + z. Lattice and shear-sector code that must match external payload generators cites this map. The body is pure base-5 digit unpack with omega bounds proofs on each Fin 5 component.
Claim. Map $n \in \mathbb{N}$ to the vertex $(x,y,z)$ on the $5\times 5\times 5$ periodic lattice by $x = \lfloor n/25 \rfloor \bmod 5$, $y = \lfloor n/5 \rfloor \bmod 5$, $z = n \bmod 5$, inverting the Track 1.D encoding $n = (x\cdot 5 + y)\cdot 5 + z$.
background
Track 1.D opens the tensor/shear sector of weak-field gravity. The older Track 1.B conformal ansatz puts one scalar potential at each vertex and averages endpoints to get edge strains; that 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.
PeriodicVertex5 is the abbreviation Vertex 5 5 5: a point of the 5-periodic cubic lattice in each coordinate. External payload generators enumerate those vertices by the mixed-radix order $n = (x\cdot 5 + y)\cdot 5 + z$. The present decoder is the inverse of that enumeration, so Lean-side lattice constructions stay bit-compatible with the generators.
proof idea
Definition by arithmetic, not a proof. The three coordinates are extracted as successive base-5 digits: integer division by 25 then mod 5 for $x$, division by 5 then mod 5 for $y$, and mod 5 for $z$. Each component is wrapped as a Fin 5 whose bound obligation is discharged by omega.
why it matters
Gives a computable, Lean-native vertex decoder that matches the numerical order of the Track 1.D payload generators. The immediate consumer is periodicExternalEdgeOfEncodedIdx5, which builds edges by base := periodicExternalVertexOfIndex5 (idx / 7) and disp := idx % 7. That edge decoder is the companion to the canonical PeriodicTorus5.edgeEquiv, whose present implementation routes through opaque Fintype.equivFin order; the external encoder/decoder pair keeps shear-sector scaffolding aligned with external payloads while the conformal-versus-shear separation (rectangle obstruction, independent edge strains) is developed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.