faceVertexC
plain-language theorem explainer
Names the third corner of the unit witness square on the 5×5×5 periodic Freudenthal torus as the lattice point (1,1,0). Anyone citing the rectangle shear or uniform-x-strain non-conformality proofs needs this label. The body is a one-line constant definition of type PeriodicVertex5.
Claim. On the $5\times 5\times 5$ periodic vertex lattice, the witness-square corner $C$ is the point $(1,1,0)$.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector on the concrete $N=5$ periodic Freudenthal 3-torus. The vertex-conformal ansatz assigns one scalar potential per vertex and induces the log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. The full edge-perturbation space is much larger (875 edges versus at most 125 conformal degrees of freedom), so an explicit shear complement is needed.
The standard witness is the unit coordinate square with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$. Strains $+1$ on the two $x$-edges and $-1$ on the two $y$-edges give a pure rectangle shear. PeriodicVertex5 is simply the type of vertices of the $5\times5\times5$ torus (Vertex 5 5 5).
proof idea
Pure definition: the constant triple $(1,1,0)$ is declared to inhabit PeriodicVertex5. No proof obligations.
why it matters
Supplies the third corner label used by the endpoint identities faceEdgeBC_endpoints and faceEdgeDC_endpoints, which identify the edges $BC$ and $DC$ of the witness square. Those identities feed the telescoping argument that the face shear is orthogonal to every conformal edge perturbation (rectangleShearFace5_inner_conformal_eq_zero: endpoint averages cancel around the square). The same corners appear when the uniform $x$-strain is shown non-conformal by reducing to the rectangle obstruction $h\neq v$ from TensorShearSector. Together these close the concrete shear-complement half of the dimension-gap story on the $N=5$ torus (conformal rank $\le 125<875$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.