rectangleShearFace5_apply_AD
plain-language theorem explainer
On the unit coordinate square of the 5×5×5 periodic torus, the explicit rectangle shear assigns strain −1 to the left y-edge A→D. Anyone computing support values or the self-inner-product of this shear witness cites this evaluation. The proof is a four-line decide-and-simp: AD is distinct from the three other face edges, so the nested if-definition collapses to −1.
Claim. Let $\sigma$ be the rectangle shear on the unit face of the $N=5$ periodic 3-torus (strain $+1$ on the two opposite $x$-edges, $-1$ on the two opposite $y$-edges, $0$ elsewhere). If $e_{AD}$ is the left $y$-edge from $(0,0,0)$ to $(0,1,0)$, then $\sigma(e_{AD})=-1$.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector beyond the vertex-conformal ansatz. That ansatz places 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 of the $5\times5\times5$ periodic Freudenthal 3-torus ($n_V=125$, $n_E=875$).
The explicit shear witness rectangleShearFace5 localizes a classical rectangle pattern on the unit coordinate square with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$: strain $+1$ on the two $x$-edges $AB$ and $DC$, $-1$ on the two $y$-edges $BC$ and $AD$, and $0$ on the remaining 871 edges. The four face edges are the concrete PeriodicEdge5 values with bases at those vertices and displacement classes $0$ ($+x$) or $1$ ($+y$).
This lemma is the pointwise evaluation of that witness on the left $y$-edge $AD$. Parallel evaluations exist for the other three supported edges.
proof idea
Three decide steps establish the Boolean inequalities $e_{AD}\neq e_{AB}$, $e_{AD}\neq e_{DC}$, and $e_{AD}\neq e_{BC}$. Unfolding the nested if-definition of the shear then reduces, under those inequalities, to the final branch that returns $-1$. The whole argument is a short simp after the three distinctness facts; no external lemmas are required.
why it matters
The four pointwise evaluations (AB, DC, BC, AD) are the arithmetic fuel for the shear's self-inner-product and for collapsing any 875-term edge inner product against the shear to its four supported edges. Downstream, periodicEdgeInnerProduct5_rectangleShearFace5_left rewrites $\langle\sigma,\eta\rangle=\eta(AB)+\eta(DC)-\eta(BC)-\eta(AD)$, and rectangleShearFace5_inner_self_eq_four then obtains $\langle\sigma,\sigma\rangle=4$ by substituting the four evaluations and normalizing.
Those identities certify that the localized rectangle pattern is a concrete, nonzero, non-conformal edge perturbation on the $N=5$ torus, witnessing the dimension gap (conformal rank $\le 125<875$) that the module establishes for the edge-tensor sector beyond the conformal ansatz. In the broader Recognition gravity program this is the explicit shear complement used to show the conformal slice is proper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.