faceVertexB
plain-language theorem explainer
Names the lattice point (1,0,0) on the 5×5×5 periodic Freudenthal 3-torus as the second corner of the unit coordinate witness square. Readers assembling the rectangle shear or uniform-x strain cite it when wiring the four face edges. The body is a one-line constant assignment into the periodic vertex type.
Claim. On the $5\times 5\times 5$ periodic Freudenthal 3-torus, the second corner of the unit coordinate witness square is the vertex $(1,0,0)$.
background
Lane 3 of the Seven-Gaps gravity development studies the edge (tensor) sector on the concrete $N=5$ periodic Freudenthal 3-torus. The vertex-conformal 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 that conformal slice sits inside the full edge-perturbation space and exhibits an explicit shear complement.
Vertices of the $N=5$ torus are triples in $\mathbb{Z}/5\mathbb{Z}^3$, abbreviated as the periodic vertex type. The witness square used throughout the file has corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$. This declaration fixes the second of those four corners.
Upstream, the periodic vertex abbreviation is just the standard $5\times 5\times 5$ vertex type from the tensor-shear sector; the rectangle obstruction there already shows that a nontrivial rectangle strain ($h\neq v$) admits no vertex-conformal potential.
proof idea
Definitional constant: the value is the triple $(1,0,0)$ at the periodic vertex type. No tactics, no lemmas, no computation.
why it matters
The four corners of the witness square are the scaffolding for the explicit shear face that proves the conformal ansatz is a proper subspace of edge perturbations. Downstream, the right $y$-edge is based at this vertex, and both endpoint identities for the $A\to B$ and $B\to C$ edges resolve to pairs involving it (by decide).
Those edges feed the inner-product identity that the face shear is orthogonal to the entire conformal slice (endpoint averages telescope around the square) and the typed non-conformality of the uniform $x$-strain (which instantiates $h=1$, $v=0$ on the square and invokes the rectangle obstruction). In the broader RS gravity lane this is local discrete geometry supporting the dimension gap $125<875$ between conformal rank and edge space on the $N=5$ torus, not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.