faceEdgeAD_endpoints
plain-language theorem explainer
On the unit face of the 5-torus cube, the labeled edge AD has ordered endpoints exactly the vertices A and D. Anyone rewriting conformal log-strain as endpoint averages on that face cites this identity. The proof is a pure finite decision on the concrete edge and vertex constructors.
Claim. For the distinguished edge $AD$ of the unit coordinate square on the $5\times 5\times 5$ periodic Freudenthal 3-torus, the ordered endpoint pair equals $(A,D)$, where $A$ and $D$ are the correspondingly labeled face vertices.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector of Regge-type log-strain on the actual $N=5$ periodic Freudenthal 3-torus. The vertex-conformal ansatz assigns one scalar potential per vertex and induces the symmetric average $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. That image is a proper linear subspace of the full edge-perturbation space (rank at most $n_V=125$ inside dimension $n_E=875$).
To exhibit a concrete shear complement, the file fixes one unit coordinate square with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$ and names its four boundary edges and four vertices. Edge objects carry an endpoints field recording the ordered pair of incident vertices. The present fact pins that field for the edge running from $A$ to $D$.
Downstream arguments rewrite any conformal edge value as the average of the two endpoint potentials; those rewrites need the endpoint pairs of $AB$, $BC$, $CD$, and $AD$ as definitional equalities.
proof idea
One-line tactic proof: decide. Both sides are closed terms built from the finite, fully constructive torus geometry (named face vertices and the named face edge), so propositional equality of the ordered pairs is decided by the kernel with no lemmas and no case splits.
why it matters
This is bookkeeping that unlocks the shear-versus-conformal calculations on the witness square. The orthogonality theorem rectangleShearFace5_inner_conformal_eq_zero rewrites each of the four face edges via endpoint averages and telescopes
$(\varphi_A+\varphi_B)+(\varphi_D+\varphi_C)-(\varphi_B+\varphi_C)-(\varphi_A+\varphi_D)=0$;
the $AD$ rewrite is exactly this identity. The same endpoint facts appear 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 RS gravity lane, these identities support the claim that the conformal ansatz is a proper subspace of edge perturbations on a genuine 3D triangulation, so tensor/shear modes exist beyond pure vertex potentials. They do not themselves touch the forcing chain T0–T8; they sit in the discrete geometric layer that makes the seven-gaps edge-sector dimension gap explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.