faceEdgeAD
plain-language theorem explainer
Names the left y-edge of the unit witness square on the 5×5×5 periodic Freudenthal torus: base corner A=(0,0,0), displacement axis 1 (A→D). Downstream shear and inner-product lemmas cite it as one of the four supported edges of the rectangle shear pattern. Pure structure constructor; no proof content.
Claim. Let $E_5$ be the set of directed edges of the $5\times5\times5$ periodic Freudenthal 3-torus. Define the left $y$-edge of the unit face square by base vertex $(0,0,0)$ and displacement index $1$, i.e. the edge $A\to D$ with $A=(0,0,0)$ and $D=(0,1,0)$.
background
Lane 3 of the Seven-Gaps gravity track studies the edge (tensor) sector on the concrete $N=5$ periodic Freudenthal 3-torus. The vertex-conformal ansatz maps a scalar per vertex to log-strain $(\xi_u+\xi_v)/2$ on each edge; the module shows that image is a proper subspace of the full edge-perturbation space (rank at most $125$ versus $875$ edges) and exhibits an explicit shear complement.
The localized witness is the unit coordinate square with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$. Edges are packaged as PeriodicEdge 5 5 5: a base vertex plus a displacement axis. The sibling faceVertexA is exactly the origin corner. Displacement index $1$ selects the $y$-direction, so this object is the left vertical side $A\to D$ of that square.
proof idea
Definition only: a one-line structure value { base := faceVertexA, disp := 1 } at type PeriodicEdge5 (abbrev for PeriodicEdge 5 5 5). No tactics, no lemmas applied.
why it matters
One of the four named edges that support the explicit rectangle shear rectangleShearFace5 (strain $+1$ on the two opposite $x$-edges, $-1$ on the two opposite $y$-edges, $0$ elsewhere). That witness is the concrete non-conformal edge perturbation used to separate the shear complement from the conformal ansatz on the $N=5$ torus.
Immediate consumers: endpoint identity faceEdgeAD_endpoints; finset distinctness lemmas (faceEdgeAB_not_mem_rest, faceEdgeDC_not_mem_rest, faceEdgeBC_not_mem_rest); pointwise evaluation rectangleShearFace5_apply_AD; and the 875-term inner-product collapse periodicEdgeInnerProduct5_rectangleShearFace5_left, which reduces to the four supported edges including this one. Sits inside the proved (zero-sorry) dimension-gap story of the edge-tensor sector, not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.