faceEdgeDC_endpoints
plain-language theorem explainer
On the unit coordinate square of the N=5 periodic torus, the top x-edge (base at D with +x displacement) has ordered endpoints exactly (D, C). Gravity and Regge-calculus arguments that expand conformal endpoint averages on the witness square cite this identity. The proof is a one-line kernel decision from the concrete vertex and edge definitions.
Claim. For the top $x$-edge of the unit witness square on the $N=5$ periodic 3-torus (base corner $(0,1,0)$, displacement class $+x$), the ordered endpoint pair equals $\bigl((0,1,0),\,(1,1,0)\bigr)$.
background
Lane 3 of the Seven-Gaps gravity development studies the edge (tensor) sector of a $5\times5\times5$ periodic Freudenthal 3-torus 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 and exhibits explicit shear witnesses.
The witness square has corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$. The top $x$-edge is the periodic edge with base $D$ and displacement class $0$ (the $+x$ class). Its endpoints are the ordered pair of the base vertex and the vertex obtained by applying that displacement. Sibling edge and vertex abbreviations fix the four sides of the square used by the rectangle shear and the uniform $x$-strain.
proof idea
One-line proof by decide. After unfolding the definitions of the top $x$-edge (base $D$, disp $0$) and of the two corner vertices $D=(0,1,0)$ and $C=(1,1,0)$, both sides of the equality are closed ground terms in a decidable type, so the kernel closes the goal.
why it matters
This is bookkeeping that unlocks the two main non-conformality and orthogonality arguments on the witness square. Downstream, rectangleShearFace5_inner_conformal_eq_zero rewrites the conformal endpoint average on the top $x$-edge via this identity, so the four averages around the square telescope to zero and the face shear is orthogonal to the entire conformal slice. The same rewrite appears in xUniformStrain5_not_conformal_typed, which instantiates conformal averages on the square, obtains horizontal strain $1$ and vertical strain $0$, and invokes the rectangle obstruction from TensorShearSector.
In the broader Recognition gravity lane, these facts support the dimension-gap claim that the conformal image (rank at most $n_V=125$) is a proper subspace of the edge space ($n_E=875$) and that concrete shear modes sit outside the conformal ansatz. The declaration itself is not a forcing-chain step (T0–T8); it is local geometry for the edge-tensor sector on the discrete 3-torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.