faceVertexA
plain-language theorem explainer
Names the origin corner (0,0,0) on the 5×5×5 periodic torus as vertex A of the unit witness square. Downstream edge and shear constructions anchor on this point. The body is a one-line constant definition.
Claim. Let $A$ be the vertex $(0,0,0)$ in the $5\times 5\times 5$ periodic lattice (vertices of the Freudenthal 3-torus). This is corner $A$ of the unit coordinate square used as the localized shear witness.
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 is inside the full edge-perturbation space on the concrete $5\times 5\times 5$ periodic Freudenthal 3-torus ($n_V=125$, $n_E=875$).
PeriodicVertex5 is the type of vertices of that torus (abbrev for Vertex 5 5 5). The explicit shear witness is a rectangle pattern on the unit coordinate square with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$: strain $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges. This definition fixes the first of those four corners.
proof idea
Pure definitional constant: the triple $(0,0,0)$ as a value of type PeriodicVertex5. No proof obligations.
why it matters
Anchors the localized rectangle/shear witness that shows the conformal ansatz is a proper subspace of edge perturbations. Downstream, faceEdgeAB and faceEdgeAD take this vertex as base (displacements $+x$ and $+y$), and endpoint lemmas identify those edges with pairs involving $A$. The orthogonality identity rectangleShearFace5_inner_conformal_eq_zero evaluates conformal averages at $A$ (and the other three corners) so the square telescopes to zero. The uniform $x$-strain non-conformality proof likewise instantiates endpoint averages on edges from $A$ and invokes the rectangle obstruction ($h\neq v$ has no vertex potential). Together these close the concrete shear complement on the $N=5$ torus in the Seven-Gaps edge-tensor sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.