periodicVertexEquiv5
plain-language theorem explainer
Canonical bijection between finite indices Fin(n_V) and typed vertices of the concrete 5×5×5 periodic Freudenthal torus. Gravity and shear-sector proofs cite it whenever edge endpoints or conformal generators must move between encoded Fin coordinates and typed Vertex data. The body is a one-line specialization of the general finite-index encoder at side lengths 5,5,5.
Claim. There is a canonical equivalence $\mathrm{Fin}(n_V)\simeq V_{5,5,5}$ between the finite index set of cardinality equal to the vertex count of the $5\times 5\times 5$ periodic torus and the typed vertex set of that torus.
background
Track 1.D separates independent edge (tensor/shear) perturbations from the older Track 1.B vertex-conformal ansatz. The conformal slice assigns one scalar per vertex and averages endpoints; it cannot represent pure shear or TT gravitational-wave modes. This module builds the concrete $N=5$ geometry on which that separation is checked.
PeriodicTorus5 is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus. PeriodicVertex5 is the typed vertex type Vertex 5 5 5. The vertex-count slot n_V is the cardinality of that finite type. Upstream, vertexFinEquiv Nx Ny Nz supplies the general encoder: every periodic vertex is indexed by a Fin of the right cardinality via the symmetric Fintype equivalence.
The present abbreviation freezes those side lengths at five and names the resulting equivalence for the rest of the shear-sector file.
proof idea
One-line wrapper: instantiate the general periodic-vertex encoder vertexFinEquiv at Nx = Ny = Nz = 5. No extra algebraic work; the equivalence is exactly the inverse of Fintype.equivFin on Vertex 5 5 5.
why it matters
This is the naming glue that lets every Track 1.D calculation speak both typed and encoded languages. Downstream, conformal generator pointwise formulas write endpoint support via periodicVertexEquiv5.symm on edge endpoints; the generator map averages coefficients at those two encoded indices; relative-column endpoint equalities transport through the same map; and the encoded torus edge-vertex map is shown to agree with typed endpoints after this transport.
In the EdgeTensorSector parent, the typed endpoint form of a conformal log-subspace perturbation exists as a potential on PeriodicVertex5, which is the codomain of this equivalence. Without a fixed $N=5$ vertex dictionary, the rectangle obstruction and the shear-versus-conformal split cannot be stated in Fin-indexed linear algebra. It does not itself touch T0–T8 or the RCL; it is infrastructure for the weak-field tensor sector on the discrete torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.