periodicOriginEdgeOfDisp5
plain-language theorem explainer
Builds the origin-row representative of a periodic edge on the $5\times5\times5$ Freudenthal torus: base fixed at the origin vertex, displacement any of the seven lattice directions. Cited by the encoded-edge map and by relative-column identities in the tensor/shear sector. Pure structure constructor; no proof content.
Claim. For each displacement $d\in\{0,\ldots,6\}$, the origin-row periodic edge is the edge whose base vertex is the torus origin and whose displacement is $d$, on the canonical $5\times5\times5$ periodic Freudenthal torus.
background
Track 1.D opens the tensor/shear sector of weak-field gravity. The older conformal ansatz puts one scalar at each vertex and averages endpoints to get edge strains; that slice cannot carry pure shear, so it misses transverse-traceless gravitational-wave modes. This module therefore treats independent edge perturbations separately from vertex-conformal ones.
A PeriodicEdge5 is an edge of the canonical $5\times5\times5$ periodic Freudenthal torus: a base vertex together with a displacement in one of seven lattice directions (Fin 7). The origin vertex is the distinguished base used for row representatives. The definition simply packages that origin base with a chosen displacement.
proof idea
Definitional constructor only. It returns the structure record whose base field is the fixed origin vertex of the $5\times5\times5$ torus and whose displacement field is the input disp : Fin 7. No lemmas or tactics.
why it matters
Gives a canonical origin-row edge for each of the seven displacements, so later maps can talk about "the" edge of a given direction without choosing a base. Downstream, encodedOriginEdgeOfDisp5 sends it through the torus edge equivalence to a global edge index, and encodedOriginEdgeOfDisp5_equiv records the round-trip. The relative-column theorem periodicRelativeColumnOfOriginDisp5 uses it as the row edge when expressing a column edge in the row's coordinate frame. That bookkeeping is part of separating genuine shear (independent edge strains) from conformal vertex potentials on the Freudenthal lattice, the first step toward TT modes in the Regge/Recognition gravity track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.