periodicSubFin5
plain-language theorem explainer
Modular coordinate subtraction on the concrete five-point circle Fin 5. Given a base index and a vertex index, it returns the vertex coordinate in the frame whose origin is the base. Downstream relative-frame maps on the N=5 periodic torus apply it componentwise. The body is a one-line modular arithmetic construction with an omega-proved bound.
Claim. For $b,v\in\{0,1,2,3,4\}$, the relative coordinate of $v$ with origin $b$ is $(v+(5-b))\bmod 5$, viewed as an element of $\mathrm{Fin}\,5$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric on a discrete geometry. The conformal (scalar) ansatz assigns one potential per vertex and cannot represent pure shear or transverse-traceless modes; this module separates independent edge perturbations from vertex-conformal ones.
The ambient lattice is the concrete periodic cubic torus with period $N=5$ in each spatial direction. Vertices are triples in $\mathrm{Fin},5\times\mathrm{Fin},5\times\mathrm{Fin},5$ (the Freudenthal-style periodic vertex type). Relative frames are needed so that edge and column data can be rewritten with a chosen lattice point as origin without leaving the torus.
This definition is the one-dimensional building block: subtraction of indices on the circle of length 5, implemented by adding the modular complement of the base.
proof idea
Definition, not a proof. The value is the subtype pair whose first component is $(v+(5-\mathrm{base}))\bmod 5$; the second component is the inequality proof that the residue lies in ${0,\ldots,4}$, discharged by omega. No lemmas are invoked.
why it matters
Relative coordinates on the $N=5$ torus are assembled componentwise from this map in periodicRelativeVertex5. That relative vertex map is the workhorse for the translation/re-basing identities (periodicRelativeVertex5_origin_eq_self, periodicRelativeVertex5_translate_eq_self, periodicTranslateVertex5_relative_eq_self) and for endpoint transport of relative columns (periodicRelativeColumnOfRow5_endpoints).
Those identities keep shear and edge-perturbation calculations origin-independent on the discrete torus, which is required before comparing pure shear modes to the conformal ansatz obstruction already proved in this file. The construction is local scaffolding for Track 1.D; it does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.