encodedOriginEdgeOfDisp5_equiv
plain-language theorem explainer
On the canonical 5 imes5 imes5 periodic Freudenthal torus, the encoded origin-edge index of a displacement is the edge-equivalence inverse of the geometric origin-row edge. Anyone matching generator-facing TT Hessian/Lichnerowicz residual formulas to the encoded edge lattice cites this bridge. The proof is a one-line simp that unfolds the encoded edge as the inverse image under the torus edge equivalence.
Claim. For every displacement index $d\in\{0,\ldots,6\}$, if $e^{\mathrm{enc}}(d)$ is the encoded origin-edge representative of $d$ on the canonical $5\times5\times5$ periodic Freudenthal torus and $\Phi$ is that torus's edge equivalence, then $\Phi(e^{\mathrm{enc}}(d))$ equals the geometric origin-row periodic edge with base at the origin vertex and displacement $d$.
background
Track 1.D builds the tensor/shear sector beyond the Track 1.B conformal ansatz. The conformal slice assigns one scalar potential per vertex and cannot represent pure shear, so it misses transverse-traceless gravitational-wave 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.
Edges on that torus admit two presentations. The geometric side is a periodic edge: an origin-base vertex together with a displacement in a seven-element index set (the discrete edge directions used by the Track 1.D generators). The encoded side is a raw edge index in the torus complex. The torus supplies an edge equivalence $\Phi$ identifying the two presentations.
The encoded origin-edge map is defined as the inverse image under $\Phi$ of the geometric origin-row edge. The geometric origin-row edge itself is the pair (origin vertex, displacement). This lemma records that $\Phi$ undoes that encoding.
proof idea
One-line wrapper. The encoded origin-edge is defined by
$e^{\mathrm{enc}}(d):=\Phi^{-1}(\text{origin-row edge of }d)$.
Unfolding that definition with simp immediately yields $\Phi(e^{\mathrm{enc}}(d))$ equal to the geometric origin-row edge. No extra lemmas are required beyond the definition and the fact that $\Phi$ is an equivalence.
why it matters
Generator-facing residual certificates for the TT Hessian versus lattice Lichnerowicz operator need a stable dictionary between encoded edge indices and geometric origin-row edges. This equivalence is that dictionary for the origin column.
It is consumed by the coefficient-only origin-column formula data structures for the TT Hessian/Lichnerowicz residual (absolute and relative-frame variants). Those structures store the two edge-operator kernels and seven residual-generator coefficient rows, then prove origin-row scalar formulas directly against the generator map. Without the encoded/geometric match, those origin-column entry formulas cannot be stated on the encoded lattice.
In the broader Recognition gravity track this is scaffolding glue inside the shear sector, not a forcing-chain landmark: it does not touch T5–T8, the RCL, or the mass ladder. It does close a concrete identification needed before discrete TT residual identities can be certified on the $5^3$ torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.