encodedOriginEdgeOfDisp5
plain-language theorem explainer
Maps a displacement index in Fin 7 to the encoded edge index of the origin-row representative on the canonical 5×5×5 periodic Freudenthal torus. Downstream TT Hessian/Lichnerowicz residual certificates cite it as the origin-column edge key. The body is a one-line inverse of the torus edge encoding equivalence applied to the geometric origin edge.
Claim. For each displacement $d \in \{0,\ldots,6\}$, the encoded origin-edge index is the preimage, under the edge encoding equivalence of the canonical $5\times5\times5$ periodic Freudenthal torus, of the geometric edge whose base is the origin vertex and whose displacement is $d$.
background
Track 1.D separates independent edge-length perturbations from the vertex-conformal ansatz of Track 1.B, so that pure shear and transverse-traceless modes can be represented. The working lattice is the canonical encoded $5\times5\times5$ periodic Freudenthal torus (PeriodicTorus5), whose edges are indexed both geometrically (base vertex plus one of seven displacements) and by a flat encoded Fin index.
The geometric origin-row representative periodicOriginEdgeOfDisp5 d is the edge with base at the origin vertex and displacement $d$. The torus supplies an equivalence edgeEquiv between encoded edge indices and those geometric edges. This definition simply names the encoded index of that origin-row edge, which residual-certificate generators use as a stable column key.
proof idea
Pure definitional wrapper: apply the inverse of PeriodicTorus5.edgeEquiv to periodicOriginEdgeOfDisp5 disp. No tactics, no lemmas beyond the equivalence already attached to the encoded torus.
why it matters
Gives the generator-facing origin-column edge key used throughout the encoded TT Hessian/Lichnerowicz residual stack. Immediate consumer is the round-trip lemma encodedOriginEdgeOfDisp5_equiv. Structures that store origin-column residual tables and coefficient formulas (EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5, EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5, the relative-frame variant, and residual row/table formula data) all index through this encoding so finite residual calculations can be stated against encoded operators rather than geometric edges.
In the Track 1.D program this is scaffolding glue, not a physics claim: it lets shear-sector residual certificates talk about the same origin-row edges the conformal obstruction lemmas already use, on the fixed $5^3$ torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.