periodicRelativeColumnOfRow5_endpoint_snd_eq_iff
plain-language theorem explainer
Second-endpoint equality for a column edge written in a row-relative frame on the $5\times5\times5$ periodic Freudenthal torus is equivalent to second-endpoint equality after translating the candidate vertex by the row base in the global frame. Lattice gauge and shear bookkeeping cite this bridge between frames. The proof is a short biconditional from the relative-column endpoint translation identity plus injectivity of vertex translation.
Claim. Let $row$ and $col$ be edges of the $5\times5\times5$ periodic Freudenthal torus and let $v$ be a vertex. Write $C$ for the column of $col$ expressed in the frame relative to $row$. Then the second endpoint of $C$ equals $v$ if and only if the second endpoint of $col$ equals the translate of $v$ by the base vertex of $row$.
background
Track 1.D builds the tensor/shear sector of the weak-field metric on the encoded $5\times5\times5$ periodic Freudenthal torus. The conformal (vertex-scalar) ansatz of Track 1.B cannot represent pure shear, so independent edge perturbations must be separated from vertex-conformal ones; this module supplies the elementary rectangle obstruction and the periodic bookkeeping that follows.
Edges and vertices are the specialized abbreviations PeriodicEdge 5 5 5 and Vertex 5 5 5. A row-relative column rewrites one edge in the translational frame fixed by another edge's base. Vertex translation by a base is the lattice automorphism used to move between that relative frame and the global frame; the second endpoint is the far vertex of an oriented edge.
The upstream identity that the relative column's endpoints, once translated by the row base, recover the original column's endpoints is the geometric input. Injectivity of that translation then converts one-sided equalities into a clean biconditional.
proof idea
Invoke the relative-column endpoint identity: translating both endpoints of the row-relative column by the row base recovers the endpoints of the original column. Project to the second factor to obtain an equality relating the translated second endpoint of the relative column to the second endpoint of the column.
For the forward direction, substitute the assumed relative-frame equality into that projected identity. For the reverse direction, chain the projected identity with the assumed global equality and cancel the translation by its injectivity. The argument is pure term/tactic bookkeeping on products and a lattice automorphism; no analysis or curvature enters.
why it matters
Frame changes for edge endpoints are the elementary step before gauge generators and encoded indices can be moved between relative and global pictures. Downstream, the encoded second-endpoint variant reuses this biconditional after applying the vertex equivalence, and the longitudinal gauge-generator shift theorem uses the same relative-column language to prove that a row-frame translate of a generator column is exactly the globally shifted generator.
In the Recognition gravity track this sits inside the tensor/shear scaffold that aims beyond the conformal ansatz toward transverse-traceless modes on the eight-tick, $D=3$ lattice geometry. It does not yet produce a TT zero mode; it only keeps endpoint bookkeeping coherent so later shear and gauge lemmas can cite a single frame-change fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.