periodicRelativeColumnOfOriginDisp5
plain-language theorem explainer
On the encoded 5×5×5 periodic Freudenthal torus, framing any column edge against an origin-row edge leaves that column edge unchanged: the relative-column map is the identity when the reference row sits at the lattice origin. Gravity/Regge analysts building relative-frame TT Hessian residual certificates cite this identity. The proof is a short simp that unfolds the relative-column and origin-edge constructors and applies the origin-relative vertex identity.
Claim. Let $d_r,d_c\in\{0,\ldots,6\}$ and let $b$ be a vertex of the $5\times5\times5$ periodic torus. Write $e_{\mathrm{orig}}(d_r)$ for the edge based at the lattice origin with displacement $d_r$, and write $e=(b,d_c)$ for the edge based at $b$ with displacement $d_c$. Then the relative-frame column of $e$ with respect to the origin-row $e_{\mathrm{orig}}(d_r)$ equals $e$ itself.
background
Track 1.D builds the tensor/shear sector of the weak-field Regge metric on the canonical encoded $5\times5\times5$ periodic Freudenthal torus. The conformal (vertex-potential) ansatz of Track 1.B cannot represent pure shear, so independent edge perturbations must be treated separately from vertex-conformal ones; this module sets up that separation and the elementary rectangle obstruction.
A PeriodicVertex5 is a vertex of the $5\times5\times5$ torus; a PeriodicEdge5 is a periodic edge, recorded as a base vertex plus a displacement in Fin 7 (the seven Freudenthal edge directions). Origin-edges are those whose base is the lattice origin. Relative-frame constructions re-express a column edge in the coordinate chart fixed by a chosen row edge; when that row is an origin-edge, the chart is the absolute chart.
The key upstream fact is that relative displacement of a vertex against the origin returns the vertex itself (periodicRelativeVertex5_origin_eq_self). The relative-column and origin-edge maps are pure constructors on this data.
proof idea
One-line tactic proof. Unfold periodicRelativeColumnOfRow5 and periodicOriginEdgeOfDisp5, then apply periodicRelativeVertex5_origin_eq_self. After unfolding, both sides are the same PeriodicEdge5 record { base := colBase, disp := colDisp }, so simp closes the goal.
why it matters
Feeds the structure EncodedTTHessianLichnerowiczCoeffRelativeOriginColumnFormulaData5, which packages origin-column formula data for a relative-frame translated residual certificate: the part of the relative certificate that agrees with the existing origin-row generator map, without asserting the absolute translated formula for every row.
In the tensor/shear track this identity is the bookkeeping step that lets residual TT Hessian / Lichnerowicz coefficients on origin columns be copied into the relative-frame certificate without extra conjugation. It sits downstream of the conformal-vs-shear split (rectangle obstruction) and upstream of encoded residual certificates used to compare the discrete Regge Hessian kernel against the lattice Lichnerowicz operator on the $5\times5\times5$ torus. No forcing-chain landmark (T5–T8) is touched; the result is pure discrete-geometry scaffolding for the gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.