faceEdgeDC
plain-language theorem explainer
Names the top x-edge of the unit face on the 5×5×5 periodic Freudenthal torus: base corner D = (0,1,0), displacement class 0 (+x), so D→C. Gravity authors cite it when building the localized rectangle shear witness and when collapsing edge inner products to four supported edges. It is a one-line structure literal, not a proved claim.
Claim. On the $5\times 5\times 5$ periodic Freudenthal 3-torus, let $D=(0,1,0)$. The top $x$-edge of the unit coordinate square is the directed periodic edge with base $D$ and displacement class $0$ (the $+x$ class), i.e. the edge $D\to C$ with $C=(1,1,0)$.
background
Lane 3 of the Seven-Gaps gravity track studies the edge (tensor) sector beyond the vertex-conformal ansatz. That ansatz assigns one scalar per vertex and induces log-strain $(\xi_u+\xi_v)/2$ on each edge. On the concrete $N=5$ periodic torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal image is a proper subspace of the full edge-perturbation space.
Edges are encoded as a base vertex plus a displacement class in ${0,1,2}$ for the three axis directions. The sibling corner $D$ is fixed as $(0,1,0)$. Displacement $0$ is the $+x$ class (same convention as the bottom edge $A\to B$). Together with the three companion face edges, this edge bounds the unit square with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$ used as the localized shear support.
proof idea
Definition by structure literal: the periodic-edge record is filled with base equal to the already-defined corner $D=(0,1,0)$ and displacement field $0$. No tactics, no lemmas, no computation beyond the record constructor. Downstream endpoint and distinctness facts are discharged later by decide on the finite torus.
why it matters
This edge is one of the four supports of rectangleShearFace5, the explicit shear witness that places strain $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges (zero elsewhere). That witness is the concrete complement to the conformal slice: it is proved non-conformal in both typed and encoded coordinates, and the 875-term edge inner product against it collapses to the four face edges.
Parent uses include the endpoint identity for this edge, the finset non-membership lemmas that keep the four supports distinct, the pointwise evaluations of the shear pattern, and the inner-product reduction. In the broader RS gravity story this supplies the hands-on non-conformal edge mode that makes the dimension gap $125<875$ visible rather than purely rank-theoretic, tying the tensor sector to the Freudenthal 3-torus geometry behind $D=3$ and the eight-tick discrete setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.