faceVertexD
plain-language theorem explainer
Names the corner D = (0,1,0) of the unit witness square on the 5×5×5 periodic Freudenthal 3-torus. Anyone citing the rectangle shear face or its edge endpoints uses this constant. The body is a one-line triple literal of type PeriodicVertex5.
Claim. On the $5\times 5\times 5$ periodic 3-torus, fix the vertex $D=(0,1,0)$ as the fourth corner of the unit coordinate square with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$.
background
Lane 3 of the Seven-Gaps gravity development studies the edge (tensor) sector beyond the vertex-conformal ansatz. That ansatz assigns one scalar potential per vertex and induces the log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. The ambient complex is the $N=5$ periodic Freudenthal 3-torus, with vertex type PeriodicVertex5 (i.e. Vertex 5 5 5) and 125 vertices, 875 edges.
The concrete shear witness is the unit face with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$. Strain $+1$ is placed on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges; all other edges carry zero. The four named corners pin those edges and their endpoint identities in later lemmas.
Upstream, PeriodicVertex5 is just the product vertex type of the $5$-torus. The other depends-on symbols (A, B from gap and birth-count modules) are ambient constants of the broader RS stack and do not enter the body of this definition.
proof idea
Definitional constant: the value is the literal triple $(0,1,0)$ at type PeriodicVertex5. No proof obligations.
why it matters
This corner is the base of the top $x$-edge faceEdgeDC and one endpoint of the left $y$-edge faceEdgeAD. Downstream endpoint theorems (faceEdgeAD_endpoints, faceEdgeDC_endpoints) decide those pairs by reduction to the four named corners.
Those edges feed the rectangle shear pattern rectangleShearFace5, whose inner product against every conformal edge perturbation vanishes by telescoping of endpoint averages around the square (rectangleShearFace5_inner_conformal_eq_zero). The same corners appear when the uniform $x$-strain is shown non-conformal by instantiating the four conformal averages and invoking the rectangle obstruction $h\neq v$ from TensorShearSector.
In the Seven-Gaps program this is scaffolding geometry for the dimension gap: conformal image rank $\le 125 < 875$, with an explicit shear complement. It does not itself touch T0–T8 or the RCL; it is local discrete geometry for the gravity edge sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.