rectangleShearFace5_apply_of_ne
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, the localized rectangle shear vanishes at every edge outside the four boundary edges of the unit coordinate square. Anyone computing supports, inner products, or non-conformality of this shear witness cites it. The proof is a one-line simp unfolding of the piecewise definition under the four inequality hypotheses.
Claim. Let $e$ be an edge of the $5\times 5\times 5$ periodic torus. If $e$ is none of the four edges of the unit face with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$ (the two opposite $+x$ edges and the two opposite $+y$ edges), then the rectangle shear edge-perturbation evaluates to $0$ at $e$.
background
Lane 3 of the Seven-Gaps gravity work 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 conformal image is a proper subspace of the full edge-perturbation space. On the concrete $N=5$ periodic 3-torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal rank is at most 125, strictly less than 875.
The explicit shear witness places strain $+1$ on the two opposite $x$-edges of the unit coordinate square and $-1$ on the two opposite $y$-edges, and $0$ elsewhere. The four supported edges are the bottom $x$-edge $A\to B$, the top $x$-edge $D\to C$, the right $y$-edge $B\to C$, and the left $y$-edge $A\to D$. The present lemma records the off-support vanishing that follows immediately from that piecewise definition.
proof idea
One-line wrapper: simp unfolds the definition of the rectangle shear (four nested equality tests returning $1$, $1$, $-1$, $-1$, else $0$) and rewrites with the four hypotheses $e\neq$ each supported edge, leaving the residual branch $0$.
why it matters
This off-support identity is the support lemma used by the downstream collapse of the 875-term edge inner product against the face shear: that product reduces exactly to the four supported evaluations $\eta(AB)+\eta(DC)-\eta(BC)-\eta(AD)$. Without the vanishing statement, the inner-product reduction would have to re-case on every edge. In the broader Seven-Gaps program the shear witness (and its encoded twin) supplies a concrete non-conformal edge perturbation, closing the existence half of the dimension-gap story on the $N=5$ torus and exhibiting an explicit tensor-sector direction orthogonal to the conformal ansatz. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is pure discrete-geometry scaffolding for the gravity edge sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.