periodicRelativeColumnOfRow5_endpoint_fst_eq_iff
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, the first endpoint of a column edge written in a row-edge frame equals a vertex v exactly when the column's global first endpoint equals the translate of v by the row base. Gauge and shear bookkeeping on the discrete torus cite this equivalence. The proof projects the relative-column endpoint identity and closes both directions by injectivity of vertex translation.
Claim. For periodic edges $\mathrm{row},\mathrm{col}$ and vertex $v$ on the $5\times5\times5$ torus, the first endpoint of the column rewritten in the row frame equals $v$ if and only if the first endpoint of $\mathrm{col}$ equals the translate of $v$ by the base vertex of $\mathrm{row}$.
background
Track 1.D separates independent edge (tensor/shear) perturbations from the Track 1.B vertex-conformal ansatz, which cannot represent pure shear or transverse-traceless modes. The ambient geometry is the concrete $N=5$ periodic Freudenthal torus: vertices are triples in $(\mathbb{Z}/5)^3$, and edges carry a base vertex plus a displacement.
A column edge written in a row frame keeps the column displacement but replaces its base by the relative base of the column with respect to the row. Vertex translation adds a fixed base vertex componentwise (mod 5). The upstream identity periodicTranslateVertex5_relativeColumn_endpoints relates the endpoints of the relative column to the global column endpoints after that translation; translation by a fixed base is injective on the torus.
proof idea
Apply the relative-column endpoint identity to row and col, then take the first factor to obtain
$\mathrm{translate}(\mathrm{row.base},,(\mathrm{rel,col}).\mathrm{endpoints}_1)=\mathrm{col.endpoints}_1$.
For the forward implication, substitute the assumed equality of the relative first endpoint with $v$ into that identity. For the converse, compose the identity with the assumed global equality and cancel the translation using injectivity of periodicTranslateVertex5 at row.base.
why it matters
This is elementary frame bookkeeping for the tensor/shear scaffold: it lets endpoint tests written in a row-relative chart be rewritten as global translated equalities. Downstream, the encoded-index variant periodicRelativeColumnOfRow5_encoded_endpoint_fst_eq_iff lifts the same fact through the vertex encoding equivalence, and periodicLongitudinalGaugeGenerator5_relativeColumn_eq_shift uses the relative-column calculus to show that a row-frame translate of a longitudinal gauge generator column is exactly the globally shifted generator.
In the broader Recognition gravity track, such identities keep discrete shear and longitudinal gauge generators consistent under torus translations while the conformal ansatz is already known to obstruct pure rectangle shear. The result is local to the $N=5$ scaffold; it does not itself produce continuum TT modes or close the full weak-field metric sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.