faceEdgeBC_endpoints
plain-language theorem explainer
On the unit coordinate square of the N=5 periodic torus, the right y-edge from B to C has endpoints exactly the corners (1,0,0) and (1,1,0). Anyone wiring conformal endpoint averages or rectangle-obstruction arguments on that face cites this identity. The proof is a one-line decide on the concrete edge and vertex constructors.
Claim. The directed edge of the witness square with base corner $(1,0,0)$ and displacement class $+y$ has endpoints $((1,0,0),(1,1,0))$.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector on the $5\times 5\times 5$ periodic Freudenthal 3-torus, beyond the vertex-conformal ansatz. That ansatz puts one scalar per vertex and induces the log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. The module builds an explicit unit square with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$ and names its four directed edges.
The right $y$-edge is the periodic edge whose base is $B$ and whose displacement class is $1$ (the $+y$ generator). Endpoints of a periodic edge are the ordered pair (base, base$+$disp). This lemma simply records that pair for the $B\to C$ edge, so later rewrites can replace abstract endpoint projections by the named corners.
proof idea
One-line computational proof: decide unfolds the definitions of the edge record (base $B$, disp $+y$), the endpoint projection, and the three named vertices, then closes the resulting ground equality on PeriodicVertex5 triples.
why it matters
Parent results need the four face-edge endpoint identities to convert conformal membership into explicit averages $(\varphi_u+\varphi_v)/2$ on the square. Downstream, the inner-product vanishing theorem uses this rewrite so the four averages telescope to zero, proving the rectangle shear is orthogonal to the whole conformal slice. The uniform $x$-strain non-conformality proof likewise instantiates endpoint averages on the same square and feeds the TensorShearSector rectangle obstruction ($h\neq v$).
In the broader RS gravity lane this is scaffolding for the concrete shear witness that the conformal image is a proper subspace of edge perturbations (rank $\le 125<875$ on the $N=5$ torus). It does not itself touch T0–T8 or the RCL; it is local combinatorial bookkeeping that makes the shear complement checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.