periodicOriginVertex5
plain-language theorem explainer
The origin vertex on the concrete 5×5×5 periodic torus is the coordinate triple (0,0,0). Anyone building edge displacements or relative frames on that lattice cites this constant. The body is a one-line definitional assignment, not a proof.
Claim. On the concrete periodic torus with periods $5$, $5$, and $5$, the origin vertex is the lattice point $(0,0,0)$.
background
Track 1.D separates independent edge (tensor/shear) perturbations from the older vertex-conformal scalar ansatz. The conformal slice cannot realize pure shear, so it cannot cover transverse-traceless weak-field modes; this module supplies the elementary rectangle obstruction and the concrete periodic geometry used later.
PeriodicVertex5 is the abbreviation for vertices of the product lattice Vertex 5 5 5, i.e. integer coordinates modulo 5 in each spatial direction. The module imports the periodic Freudenthal torus geometry and Regge first-variation tooling that underwrite that lattice.
The origin is the canonical base point against which displacements and relative coordinates are measured on that finite torus.
proof idea
Definitional constant: the value is the triple (0, 0, 0) of type PeriodicVertex5. No lemmas or tactics are involved.
why it matters
This constant is the base vertex for origin-row edge representatives (periodicOriginEdgeOfDisp5 builds a periodic edge with base := periodicOriginVertex5) and for the relative-frame identity that translating by the origin is the identity map on vertices (periodicRelativeVertex5_origin_eq_self).
In the tensor/shear scaffold it fixes the coordinate origin so that edge displacements and shear strains can be written without an arbitrary base choice. It does not itself touch T0–T8 or the RCL; it is infrastructure for the gravity-side Regge/TT sector that must eventually sit on the forced D = 3, eight-tick geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.