rectangleShearFace5_apply_AB
plain-language theorem explainer
On the 5×5×5 periodic torus, the explicit rectangle shear edge perturbation evaluates to +1 on the bottom x-edge of the unit face. Downstream proofs of the four-edge inner-product collapse, the self-norm equal to 4, and non-vanishing all cite this evaluation. The proof is a one-line simp unfolding of the piecewise definition.
Claim. Let $\eta$ be the rectangle/shear edge perturbation on the $N=5$ periodic Freudenthal 3-torus (strain $+1$ on the two opposite $x$-edges of the unit face, $-1$ on the two opposite $y$-edges, and $0$ elsewhere). Then $\eta(e_{AB})=1$, where $e_{AB}$ is the bottom $x$-edge of that face (displacement class $+x$ from the origin vertex).
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 $5\times5\times5$ periodic torus one has $n_V=125$ and $n_E=875$, so the conformal rank is at most 125, strictly less than the edge dimension.
The explicit shear witness rectangleShearFace5 places strain $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges of the unit coordinate square with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$, and zero on the remaining 871 edges. The bottom $x$-edge of that face is the periodic edge with base at the origin vertex and displacement class $0$ (the $+x$ direction).
proof idea
One-line wrapper: simp [rectangleShearFace5] unfolds the piecewise definition of the shear pattern. The first branch matches the queried edge (the bottom $x$-edge), so the goal reduces to the literal $1=1$.
why it matters
This evaluation is the first of four pointwise facts that pin the support of the rectangle shear. It is rewritten into the collapsed four-term inner product against an arbitrary edge field, into the self-inner-product identity equaling 4, and into the non-vanishing argument (congruence at this edge yields $1\neq0$). Those facts certify that the shear witness is a concrete, nonzero, non-conformal edge perturbation on the $N=5$ torus, closing the existence half of the dimension-gap story in the edge-tensor sector: the conformal ansatz does not exhaust the 875-dimensional edge space, and an explicit localized rectangle obstruction sits outside it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.