rectangleShearFace5_apply_DC
plain-language theorem explainer
On the 5×5×5 periodic torus, the explicit rectangle shear assigns strain +1 to the top x-edge of the unit face (corners (0,0,0)–(1,1,0)). Anyone computing inner products or norms of this shear witness cites the evaluation. The proof is a two-line decide-and-simp: the top edge is distinct from the bottom edge, so the piecewise definition returns 1.
Claim. Let $\eta$ be the rectangle shear on the unit coordinate face of the $N=5$ periodic Freudenthal 3-torus: strain $+1$ on the two opposite $x$-edges, $-1$ on the two opposite $y$-edges, and $0$ elsewhere. Then $\eta$ evaluates to $1$ on the top $x$-edge (base at $(0,1,0)$, displacement class $+x$).
background
Lane 3 of the Seven-Gaps gravity development studies the edge (tensor) sector of a 3D Regge triangulation 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 question is how small this conformal slice sits inside the full edge-perturbation space.
On the concrete $5\times5\times5$ periodic Freudenthal 3-torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal image has rank at most 125 and is a proper subspace. An explicit shear complement is the rectangle pattern on the unit face 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 top $x$-edge $DC$ is the periodic edge with base $D$ and displacement class $0$ ($+x$). The present lemma records the pointwise value of the shear on that edge.
proof idea
Unfold the piecewise definition of the rectangle shear. It returns $1$ on the bottom $x$-edge $AB$, else $1$ on the top $x$-edge $DC$, else $-1$ on the two $y$-edges, else $0$. A decide step shows the top edge is not equal to the bottom edge, so the second branch fires and simp closes with value $1$.
why it matters
This is one of four pointwise evaluations that pin the support of the shear witness. Downstream, the 875-term periodic edge inner product against the shear collapses to the four supported edges, and the self-inner-product identity then reads off $\langle\eta,\eta\rangle=1+1+(-1)^2+(-1)^2=4$ by rewriting with those four evaluations and norm_num.
Together with the typed and encoded non-conformality theorems for the same witness, the evaluations certify a concrete, localized tensor mode orthogonal to the conformal ansatz on the $N=5$ torus. In the Recognition gravity program this supplies the explicit shear complement demanded by the dimension gap (conformal rank $\le 125 < 875$), closing the constructive half of Lane 3 without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.