faceEdgeBC
plain-language theorem explainer
Names the right y-edge of the unit witness square on the 5×5×5 periodic Freudenthal torus: base corner B=(1,0,0) with displacement class 1 (+y), so B→C. Anyone building or citing the localized rectangle shear witness uses this edge label. The body is a one-line structure literal.
Claim. Let $E_5$ be the set of directed edges of the $5\times5\times5$ periodic 3-torus. Define the edge with base vertex $B=(1,0,0)$ and displacement class $1$ (the $+y$ lattice step). This is the right $y$-edge $B\to C$ 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 work studies the edge (tensor) sector on a finite 3D Regge complex beyond the vertex-conformal ansatz. That ansatz assigns one scalar per vertex and induces log-strain $(\xi_u+\xi_v)/2$ on each edge; the module measures how small that conformal image is inside the full edge-perturbation space on the concrete $N=5$ periodic torus ($125$ vertices, $875$ edges).
PeriodicEdge5 is the edge type of that torus (periodic edge data for periods $5,5,5$). Edges are recorded by a base vertex and a displacement class. The sibling faceVertexB is the corner $(1,0,0)$ of the unit face square used as the shear support. Displacement class $1$ is the $+y$ step, so this definition is the right vertical side $B\to C$ of that square.
Upstream dimension constants $D=3$ (T8/T9) fix the ambient spatial setting; the torus and edge encoding come from the Freudenthal/tensor-shear infrastructure imported by the module.
proof idea
Definition, not a proof. The value is the structure literal with base := faceVertexB (the point $(1,0,0)$) and disp := 1 (displacement class $+y$). No lemmas are applied; endpoints and distinctness facts about this edge are proved later by decide.
why it matters
This edge is one of the four supported edges of the explicit shear witness rectangleShearFace5, which places strain $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges (including this $B\to C$ edge) and $0$ elsewhere. Downstream, faceEdgeBC_endpoints pins its endpoints to $(B,C)$; faceEdgeBC_not_mem_rest and sibling distinctness lemmas keep the four face edges pairwise separate so the $875$-term inner product against the face shear collapses to four terms (periodicEdgeInnerProduct5_rectangleShearFace5_left). Those facts underwrite the typed and encoded non-conformality of the rectangle shear, closing the concrete gap that the conformal range (rank $\le 125$) is a proper subspace of the $875$-dimensional edge space on the $N=5$ torus. In the RS gravity lane this is the localized tensor/shear complement to the conformal ansatz on a $D=3$ lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.