periodicRelativeVertex5
plain-language theorem explainer
Relative vertex coordinates on the discrete 5×5×5 torus: rewrite a vertex so a chosen base point sits at the origin, via componentwise modular subtraction. Shear-sector and gauge-index constructions cite it when re-basing edges into a local frame. The body is a three-coordinate application of the N=5 modular difference.
Claim. For vertices $b,v$ on the $5\times 5\times 5$ periodic lattice, the relative vertex of $v$ with frame origin $b$ is the triple of modular differences $(v_x-b_x,\,v_y-b_y,\,v_z-b_z)$ in $\mathbb{Z}/5\mathbb{Z}$.
background
This module opens Track 1.D (tensor/shear sector). Track 1.B's conformal ansatz assigns one scalar potential per vertex and induces edge-length changes by averaging endpoints; that scalar slice cannot represent pure shear, so it misses transverse-traceless weak-field modes. The file separates independent edge perturbations from vertex-conformal ones and records the elementary rectangle obstruction.
A periodic vertex here is a point of the product lattice $\mathrm{Vertex},5,5,5$, i.e. three coordinates in $\mathrm{Fin},5$. Coordinate subtraction on that circle is the modular map $(v+(5-b))\bmod 5$. The relative-vertex constructor applies that map in each spatial slot so that $b$ becomes the new origin.
proof idea
Pure definition, not a proof. Unpack the nested pair structure of a three-coordinate vertex and apply the N=5 modular difference to each $\mathrm{Fin},5$ component. No lemmas are invoked beyond that coordinate subtraction.
why it matters
Local-frame bookkeeping for the discrete torus used in the shear track. Downstream it builds relative column edges from a row base, proves that relative endpoints match endpoint-wise re-basing, and supplies the origin and translate-inverse identities (re-basing at the origin is the identity; translating then re-basing recovers the original relative vertex).
Those identities feed encoded vertex-index and longitudinal-gauge-index translation equivalences, so gauge and shear data can be moved into a row-centered frame without changing combinatorial type. That is the discrete setup needed before comparing independent edge shear to vertex-conformal strain on the periodic complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.