periodicRelativeVertex5_origin_eq_self
plain-language theorem explainer
On the concrete 5×5×5 periodic torus, relative-frame coordinates of any vertex taken about the origin equal the vertex itself. Builders of shear-sector edge displacements from a global origin frame cite this identity. The proof destructures the triple of Fin coordinates and simplifies the modular subtraction against (0,0,0).
Claim. For every vertex $v$ on the $5\times 5\times 5$ periodic torus, the relative vertex of $v$ with respect to the origin $(0,0,0)$ equals $v$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. The conformal ansatz of Track 1.B assigns one scalar potential per vertex and cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and works on a concrete periodic lattice.
PeriodicVertex5 is the type of vertices of the $5\times 5\times 5$ torus (Vertex 5 5 5). The origin vertex is the zero triple $(0,0,0)$. Relative vertices are obtained by coordinate-wise modular subtraction (periodicSubFin5) of a chosen frame origin from a global vertex. The identity here is the special case when that origin is zero.
proof idea
Term-mode proof by cases on the vertex triple. Destructure $v$ as $\langle x,y,z\rangle$, then apply componentwise extensionality and simplify the definitions of relative vertex, modular subtraction on Fin 5, and the origin. Each coordinate reduces to $x-0=x$ (and likewise for $y,z$) in modular arithmetic, so the relative triple equals $v$.
why it matters
This is a frame-normalization lemma inside the shear-sector scaffold. Downstream, periodicRelativeColumnOfOriginDisp5 uses it to show that a relative column built from an origin-based row edge recovers the original column edge unchanged. Without origin-invariance of the relative map, displacement bookkeeping on the periodic torus would carry a spurious base offset.
In the broader Recognition gravity track the lemma is elementary infrastructure, not a forcing-chain step: it supports clean relative-frame statements for non-conformal edge strains that the conformal ansatz cannot see. It does not itself produce TT modes or close any of the seven gravity gaps; it only keeps the $N=5$ lattice arithmetic honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.