faceEdgeAB
plain-language theorem explainer
Names the bottom +x edge of the unit face square on the 5×5×5 periodic Freudenthal 3-torus: base vertex (0,0,0), displacement class 0. Downstream shear and inner-product lemmas cite it as one of the four supported edges of the rectangle shear witness. The body is a one-line structure literal.
Claim. Let $e_{AB}$ be the edge of the $5\times 5\times 5$ periodic Freudenthal 3-torus with base vertex $(0,0,0)$ and displacement class $0$ (the $+x$ direction). Equivalently, $e_{AB}$ is the bottom $x$-edge $A\to B$ of the unit coordinate square with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$.
background
Lane 3 of the Seven-Gaps gravity track studies the edge (tensor) sector of a finite 3D Regge complex 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; the module measures how small this conformal slice is inside the full edge-perturbation space on the concrete $N=5$ periodic torus.
Edges are pairs (base, disp) in the type PeriodicEdge 5 5 5: a base vertex in $(\mathbb{Z}/5)^3$ and a displacement class selecting one of the three axis directions. The sibling definition of corner $A$ fixes the origin $(0,0,0)$ of the witness square. Spatial dimension $D=3$ (forced by T8) underlies the three-axis Freudenthal lattice.
The four edges of that unit face square are the only nonzero support of the explicit shear witness used to exhibit a non-conformal edge perturbation.
proof idea
One-line structure literal: set base to the origin corner $(0,0,0)$ and disp to $0$ (the $+x$ displacement class). No lemmas or tactics; the type is the abbreviation PeriodicEdge 5 5 5.
why it matters
This edge is the first support of rectangleShearFace5, the localized shear pattern that puts strain $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges of the unit face, and $0$ elsewhere. Downstream facts include the endpoint identity $e_{AB}\mapsto(A,B)$, exclusion from the other three face edges, the four pointwise evaluations of the shear, and the collapse of the 875-term edge inner product against the shear to those four edges.
Together those facts feed the typed and encoded non-conformality theorems for the rectangle shear, which close the concrete dimension-gap story on the $N=5$ torus: conformal rank $\le 125 < 875=$ edge-space dimension. That gap is the Lane-3 witness that the edge/tensor sector properly exceeds the conformal ansatz in Recognition gravity (D=3, eight-tick lattice geometry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.