periodicAddFin5
plain-language theorem explainer
Modular addition of two coordinates in Fin 5, i.e. addition modulo 5 on the discrete circle of length 5. Anyone building translations or relative frames on the concrete N=5 periodic torus cites this. The body is the standard Fin constructor: sum of values mod 5, with omega discharging the residual bound.
Claim. For base coordinates $b,v\in\{0,1,2,3,4\}$, define $b\oplus_5 v:=(b+v)\bmod 5$, returned as an element of $\mathrm{Fin}\,5$.
background
Track 1.D opens the tensor/shear sector of the weak-field metric. The conformal (vertex-scalar) ansatz cannot carry pure shear or transverse-traceless modes, so the module separates independent edge perturbations from vertex-conformal ones and works on a concrete periodic lattice.
The geometry is the N=5 periodic torus (imported from PeriodicFreudenthalTorus). Vertices are triples of Fin 5 coordinates (PeriodicVertex5). Coordinate arithmetic on each axis is ordinary modular addition on the five-point circle; this definition is that one-dimensional sum.
Sibling constructors (periodicTranslateVertex5, relative-frame maps) apply the same operation componentwise so that lattice translations stay inside the typed torus.
proof idea
Pure definition, not a proof. Unpack the two Fin 5 values, add their underlying naturals, reduce modulo 5, and repackage as Fin 5. The proof obligation $0\le(b+v)\bmod 5<5$ is discharged by omega. No lemmas are invoked.
why it matters
This is the atomic group law used by periodicTranslateVertex5, which translates a typed N=5 vertex by adding base and displacement on each coordinate. Downstream inverse identities (periodicTranslateVertex5_relative_eq_self and periodicRelativeVertex5_translate_eq_self) rely on that translation being invertible on the torus; both reduce to the fact that modular addition on Fin 5 is a group operation.
In the shear-sector scaffold the translation/relative-frame pair lets one move edge and hinge data without leaving the periodic cell, which is prerequisite bookkeeping before comparing conformal versus independent edge perturbations on rectangles and before any Regge TT analysis on the same lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.