faceEdgeBC_not_mem_rest
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, the unit-square face edge BC is distinct from the face edge AD. Anyone collapsing the rectangle-shear inner product to its four supported edges cites this. The proof is a one-line decidable check of edge inequality in the finite type PeriodicEdge5.
Claim. Writing $BC$ and $AD$ for the two opposite edges of the unit coordinate square face on the $5\times 5\times 5$ periodic edge set, one has $BC \notin \{AD\}$ as elements of that finite edge type.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector of Regge data beyond the vertex-conformal ansatz. On any finite 3D triangulation the conformal map sends a scalar per vertex to the log-strain $(\xi_u+\xi_v)/2$ on each edge; on the concrete $N=5$ periodic 3-torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal image is a proper subspace of the full edge-perturbation space.
An explicit shear witness rectangleShearFace5 places strain $+1$ on the two $x$-edges and $-1$ on the two $y$-edges of the unit square with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$. Those four edges are named $AB$, $DC$, $BC$, and $AD$ (the last is the left $y$-edge $A\to D$). The present fact records that the opposite pair $BC$ and $AD$ are unequal as PeriodicEdge5 values.
proof idea
One-line wrapper: decide. Equality of PeriodicEdge5 (alias PeriodicEdge 5 5 5) is decidable, and membership of a singleton Finset reduces to that equality, so the kernel discharges the goal by computation on the concrete base vertex and displacement data of the two edges.
why it matters
Feeds the support lemma periodicEdgeInnerProduct5_rectangleShearFace5_left, whose doc-comment states that "the 875-term inner product against the face shear collapses to its four supported edges." That collapse needs a finset of exactly those four edges and therefore needs pairwise distinctness facts such as $BC\neq AD$.
In the broader RS gravity picture this is bookkeeping inside the proof that the conformal ansatz is a proper subspace of edge perturbations on the Freudenthal 3-torus (the dimension gap $125<875$), and that an explicit localized shear is a concrete non-conformal witness. It does not itself touch the forcing chain T0–T8; it is infrastructure for the tensor-sector complement to the conformal slice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.