periodicExternalVertexIndex5
plain-language theorem explainer
Encodes a vertex of the 5×5×5 periodic torus as a single natural number via mixed-radix packing of its three coordinates. Downstream Track 1.D edge and TT-generator matrices use this external order so Lean indices match the Python payload numbering. The body is a pure arithmetic definition, not a proof.
Claim. For a vertex $v=(x,y,z)$ on the $5\times 5\times 5$ periodic lattice, the external index is $((x\cdot 5+y)\cdot 5+z)\in\mathbb{N}$. This is the encoder inverse to the external vertex decoder on in-range payload indices.
background
Track 1.D builds the tensor/shear sector missing from the Track 1.B conformal ansatz. Conformal edge strains average endpoint scalar potentials and cannot realize pure shear, so they miss transverse-traceless weak-field modes. This module separates independent edge perturbations from vertex-conformal ones and sets up external index conventions for numerical generators.
PeriodicVertex5 is the concrete vertex type of the $N=5$ periodic Freudenthal torus (Vertex 5 5 5). The external encoder packs the three coordinates in base 5 so Lean-side matrix rows and columns line up with the Track 1.D Python payloads. Spatial dimension $D=3$ (forced at T8) is why three coordinates appear; the factor 5 is the chosen lattice period, not a physical constant.
proof idea
Definitional, not a theorem. Expand the nested product structure of a Vertex 5 5 5 triple and evaluate the mixed-radix formula $(x\cdot 5+y)\cdot 5+z$. No lemmas are invoked; the term is pure Nat arithmetic matching the external decoder order documented beside the edge encoder.
why it matters
Gives the shared external vertex numbering used by the edge encoder (edge_index = vertex_index * 7 + disp), the external edge head index, and both the dense and sparse TT normal-equation generator matrices for the $N=5$ torus. Those generators feed the Python payload comparison that checks conformal columns versus longitudinal shear columns in the weak-field TT sector.
Without a stable Lean-native index (as opposed to opaque Fintype.equivFin order), the scaffold cannot certify that matrix entries and sparse dots agree with the external numerics. This is infrastructure for the tensor/shear track, not a forcing-chain step; it sits downstream of the $D=3$ geometry and the rectangle obstruction that pure conformal strains cannot produce shear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.