faceEdgeAB_endpoints
plain-language theorem explainer
On the 5×5×5 periodic torus, the bottom x-edge of the unit witness square has endpoints exactly the corners (0,0,0) and (1,0,0). Anyone proving conformal endpoint averages or rectangle-obstruction non-conformality on that square cites this. The proof is a one-line `decide` on the concrete edge and vertex definitions.
Claim. The bottom $+x$ edge of the unit coordinate square on the $N=5$ periodic torus has endpoints equal to the ordered pair of corners $(0,0,0)$ and $(1,0,0)$.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector beyond the vertex-conformal ansatz. That ansatz assigns one scalar per vertex and induces the log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. The module measures how small this conformal slice sits inside the full edge-perturbation space on the concrete $5\times5\times5$ periodic Freudenthal 3-torus, and exhibits explicit shear witnesses.
The unit square with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$ is the localized witness face. The bottom $x$-edge is the periodic edge with base $A$ and displacement class $0$ (the $+x$ class). Endpoints of a periodic edge are the ordered pair (base, base translated by the displacement).
proof idea
One-line computational proof: decide unfolds the definitions of the bottom $x$-edge (base $A$, disp $0$), of the two corners $A$ and $B$, and of the endpoints projection, then closes by reflexivity on the resulting concrete Fin tuples.
why it matters
This identity is the first rewrite step when any conformal edge field is evaluated on the witness square. Downstream, rectangleShearFace5_inner_conformal_eq_zero uses it to show the face shear is orthogonal to the whole conformal slice: endpoint averages telescope to zero around the square. Likewise xUniformStrain5_not_conformal_typed instantiates the conformal average on this edge to obtain horizontal strain $1$ versus vertical strain $0$, then invokes the rectangle obstruction from TensorShearSector.
Those non-conformality and orthogonality facts feed the dimension-gap story on the $N=5$ torus (conformal rank $\le 125 < 875$ edge dimension) and the existence of concrete shear outside the conformal ansatz. In the broader RS gravity program this is scaffolding for the tensor sector beyond pure conformal strain, not a T0–T8 forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.