periodicRelativeColumnOfRow5_encoded_endpoint_fst_eq_iff
plain-language theorem explainer
On the encoded 5×5×5 periodic Freudenthal torus, the first endpoint of a row-relative edge column decodes to vertex index v exactly when the global first endpoint of that column decodes to the base-translate of v. Anyone wiring conformal generator columns between row frames and the global frame cites this. The proof is a two-sided transport across the vertex encoding equivalence, reducing to the unencoded endpoint lemma.
Claim. Let $E$ be the edge set of the encoded $5\times 5\times 5$ periodic Freudenthal torus, and let $v$ be a vertex index in $\mathrm{Fin}\,n_V$. For edges $\mathrm{row},\mathrm{col}\in E$, the decoded first endpoint of the row-relative column of $\mathrm{col}$ equals $v$ if and only if the decoded first endpoint of $\mathrm{col}$ equals the encoded translate of $v$ by the base of $\mathrm{row}$.
background
Track 1.D builds the tensor/shear sector missing from the Track 1.B conformal ansatz. The conformal ansatz puts one scalar at each vertex and averages endpoint values onto edges; that slice cannot carry pure shear or transverse-traceless gravitational-wave modes. This module therefore separates independent edge perturbations from vertex-conformal ones and works on a concrete discrete geometry.
The geometry is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus (PeriodicTorus5), with edges PeriodicEdge5. Vertices are handled in two presentations: an internal geometric vertex type and an external index in $\mathrm{Fin},n_V$, related by the encoding equivalence periodicVertexEquiv5. Row-relative columns re-express an edge in a frame fixed by a chosen row edge; periodicTranslateEncodedVertexIdx5 is the corresponding base translation on encoded indices.
The unencoded sibling lemma periodicRelativeColumnOfRow5_endpoint_fst_eq_iff already equates first-endpoint membership in the relative frame with a global translate. The present statement is the same identity after decoding both sides to external indices.
proof idea
Tactic proof by constructor on the biconditional.
Forward: assume the decoded relative first endpoint equals $v$. Apply injectivity of periodicVertexEquiv5, then simpa with the definition of the encoded translate, feeding the unencoded lemma periodicRelativeColumnOfRow5_endpoint_fst_eq_iff at the encoded image of $v$, after pushing the hypothesis through congrArg periodicVertexEquiv5.
Reverse: assume the decoded global first endpoint equals the encoded translate of $v$. Lift that equality by congrArg periodicVertexEquiv5 to a global geometric translate identity, apply the reverse direction of the same unencoded endpoint lemma, and decode back with congrArg periodicVertexEquiv5.symm.
No new geometry is proved; the work is pure transport across the vertex encoding.
why it matters
This lemma is the encoded first-endpoint bridge used by periodicConformalGenerator5_relativeColumn_eq_shift, which states that a row-frame translate of one conformal generator column equals the globally shifted conformal generator column. That identity is part of the Track 1.D scaffold separating conformal (vertex-scalar) edge variations from genuine shear/tensor edge perturbations on the discrete torus.
In the broader Recognition gravity program, the conformal ansatz alone cannot represent TT gravitational-wave modes; the tensor/shear track must show how independent edge strains sit outside the vertex-conformal slice. Endpoint bookkeeping in relative versus global frames is elementary but mandatory before generator matrices and zero-mode analysis can be compared across frames on the $5\times 5\times 5$ Freudenthal lattice.
It does not itself produce a shear mode or a continuum TT projector; it closes a discrete coordinate identity those later statements need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.