periodicRelativeColumnOfRow5_encoded_endpoint_snd_eq_iff
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, the decoded second endpoint of a row-relative edge equals a vertex index v exactly when the decoded second endpoint of the original edge equals the global translate of v by the row base. Anyone tracking conformal generator columns under row-frame changes cites this. The proof is a two-sided transport across the vertex encoding equivalence, reducing to the unencoded endpoint lemma via injectivity.
Claim. Let $row$ and $col$ be edges of the canonical $5\times5\times5$ periodic Freudenthal torus, and let $v$ be a vertex index. Decoding the second endpoint of the row-relative column of $col$ yields $v$ if and only if decoding the second endpoint of $col$ yields the encoded translate of $v$ by the base of $row$.
background
Track 1.D builds the tensor/shear sector beyond the Track 1.B conformal ansatz. The conformal ansatz puts one scalar at each vertex and varies edge lengths by averaging endpoint potentials; that slice cannot carry pure shear or transverse-traceless modes. This module separates independent edge perturbations from vertex-conformal ones and works on a fixed discrete geometry: the canonical encoded $5\times5\times5$ periodic Freudenthal torus (PeriodicTorus5), with edges PeriodicEdge5.
Vertices are handled in two presentations linked by an equivalence periodicVertexEquiv5: an external encoded index (the numerical order used by payload generators) and the internal torus vertex type. Row-relative columns re-express an edge in the frame of a chosen row edge; global translation shifts encoded indices by a base vertex. The unencoded companion lemma already equates second-endpoint membership in the relative frame with a global vertex translate; the present statement is the same fact after decoding both sides to encoded indices.
proof idea
Bidirectional constructor. Forward: assume the decoded relative second endpoint is $v$. Apply injectivity of periodicVertexEquiv5, then rewrite through periodicTranslateEncodedVertexIdx5 and feed the encoded assumption into the unencoded lemma periodicRelativeColumnOfRow5_endpoint_snd_eq_iff (first direction) after conjugating by the equivalence. Reverse: from the encoded global equality, conjugate to obtain a global vertex equality for the unencoded endpoints, apply the second direction of the same unencoded lemma, and decode back with symm. All steps are simpa/congrArg transport; no new geometry is proved here.
why it matters
This is a bookkeeping bridge inside the tensor/shear scaffold: conformal generator columns must transform cleanly when one switches from a row-relative frame to a global shift. The sole downstream consumer is periodicConformalGenerator5_relativeColumn_eq_shift, whose doc-comment states that a row-frame translate of one conformal generator column is exactly the globally shifted conformal generator column. That identity needs endpoint indices to match under encoding, which is precisely this iff.
In the broader Recognition gravity track, the point is to isolate shear degrees of freedom that the pure conformal (vertex-scalar) ansatz cannot reach, on the discrete Regge/Freudenthal geometry imported from the periodic torus and first-variation modules. The result does not itself produce TT modes or a continuum limit; it clears an index-level obstruction so generator columns can be compared across frames.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.