faceEdgeAB_not_mem_rest
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, the bottom +x edge of the unit coordinate square is distinct from the other three edges of that square. Anyone collapsing support of the rectangle shear witness to four edges needs this separation. The proof is a one-line decidability check on finite edge equality.
Claim. Let $e_{AB}$ be the bottom $+x$ edge of the unit face with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$ on the $5\times 5\times 5$ periodic Freudenthal 3-torus, and let $e_{DC}$, $e_{BC}$, $e_{AD}$ be the top $+x$, right $+y$, and left $+y$ edges of the same face. Then $e_{AB}\notin\{e_{DC},e_{BC},e_{AD}\}$ as elements of the finite set of periodic edges.
background
Lane 3 of the Seven-Gaps gravity track studies the edge (tensor) sector on the concrete $N=5$ periodic Freudenthal 3-torus 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 this conformal slice is inside the full edge-perturbation space (dimension 875 versus conformal rank at most 125) and exhibits an explicit shear complement.
The unit coordinate square with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$ carries four oriented edges: bottom $+x$ ($A\to B$), top $+x$ ($D\to C$), right $+y$ ($B\to C$), and left $+y$ ($A\to D$). These are the support of the localized rectangle shear witness, which places strain $+1$ on the two $x$-edges and $-1$ on the two $y$-edges. Periodic edges are pairs (base vertex, displacement class) on the $5\times 5\times 5$ lattice.
proof idea
One-line wrapper: decide. Membership of a concrete periodic edge in a three-element Finset of periodic edges is a decidable proposition (finite equality of base vertices and displacement classes), so the kernel discharges the goal by computation with no lemmas.
why it matters
Feeds periodicEdgeInnerProduct5_rectangleShearFace5_left, which collapses the 875-term edge inner product of the rectangle shear against an arbitrary edge perturbation down to the four supported face edges. Pairwise separation of those edges is the bookkeeping needed so the sum does not double-count or cancel spuriously when the support finset is assembled.
In the broader Lane 3 story this is scaffolding for the explicit non-conformal shear witness: once the four edges are distinct, the shear pattern $(+1,+1,-1,-1)$ is well-defined as a typed edge perturbation and can be shown outside the conformal range. That witness underwrites the proper-subspace claim that conformal edge strains are a strict subspace of all edge perturbations on the $N=5$ torus, a concrete dimension-gap fact in the gravity track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.