faceEdgeDC_not_mem_rest
plain-language theorem explainer
On the unit coordinate square of the 5×5×5 periodic Freudenthal torus, the top x-edge D→C is distinct from both y-edges B→C and A→D. Anyone collapsing the rectangle-shear inner product to its four supported edges needs this membership fact. The proof is a one-line decidability check on the concrete edge encodings.
Claim. Let $E_{DC}$ be the top $x$-edge $D\to C$ of the unit face on the $5\times 5\times 5$ periodic edge set, and let $E_{BC}$, $E_{AD}$ be the two $y$-edges of that face. Then $E_{DC}\notin\{E_{BC},E_{AD}\}$ as a finite-set membership statement.
background
Lane 3 of the Seven-Gaps gravity track studies the edge (tensor) sector of a $5\times 5\times 5$ periodic Freudenthal 3-torus beyond the vertex-conformal ansatz. The conformal ansatz assigns one scalar per vertex and induces log-strain $(\xi_u+\xi_v)/2$ on each edge; the full edge-perturbation space is much larger (875 edges vs at most 125 conformal degrees of freedom).
The explicit shear witness is the unit coordinate square with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$. Its four boundary edges are the two $x$-edges (bottom $A\to B$, top $D\to C$) and the two $y$-edges (right $B\to C$, left $A\to D$), each encoded as a base vertex plus a displacement class in ${0,1,2}$ on PeriodicEdge 5 5 5.
The present fact is a pure combinatorial non-membership among those three named edges: the top $x$-edge is not either $y$-edge.
proof idea
One-line wrapper: decide. Equality and Finset membership on the concrete inductive encoding of periodic edges (base vertex in $(\mathbb{Z}/5)^3$ plus a displacement class) are decidable, so Lean closes the goal by computation with no lemmas.
why it matters
Feeds the support-collapse theorem periodicEdgeInnerProduct5_rectangleShearFace5_left, whose doc-comment states that the 875-term inner product of the face shear against an arbitrary edge perturbation reduces to the four supported edges: $\eta(AB)+\eta(DC)-\eta(BC)-\eta(AD)$. The non-membership facts keep the Finset of "rest" edges free of double-counting when the sum is split into the shear support and its complement.
In the broader RS gravity lane this is scaffolding for the concrete non-conformal shear witness on the $N=5$ torus: the rectangle shear puts $+1$ on the two $x$-edges and $-1$ on the two $y$-edges, proving the conformal image is a proper subspace of the edge-perturbation space (rank $\le 125<875$). It does not itself touch T0–T8 or the RCL; it is local linear-algebra bookkeeping inside the edge-tensor sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.