rectangleShearFace5_apply_BC
plain-language theorem explainer
On the 5×5×5 periodic torus, the explicit rectangle shear edge perturbation evaluates to −1 on the right y-edge of the unit face. Anyone computing supports, inner products, or non-conformality of this shear witness cites the evaluation. The proof is a three-line simp after deciding the edge is distinct from the two x-edges that carry +1.
Claim. Let $\eta$ be the rectangle shear on the unit coordinate face of the $5\times 5\times 5$ periodic torus (strain $+1$ on the two opposite $x$-edges, $-1$ on the two opposite $y$-edges, $0$ elsewhere). Then $\eta$ evaluated on the right $y$-edge $B\to C$ equals $-1$.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector 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 $N=5$ Freudenthal 3-torus ($n_V=125$, $n_E=875$).
The explicit shear witness rectangleShearFace5 localizes strain on one unit face with corners $A=(0,0,0)$, $B=(1,0,0)$, $C=(1,1,0)$, $D=(0,1,0)$: $+1$ on the bottom and top $x$-edges $AB$ and $DC$, $-1$ on the right and left $y$-edges $BC$ and $AD$, and $0$ on the remaining 871 edges. The right $y$-edge $BC$ is the periodic edge with base $B$ and displacement class $+y$.
Pointwise evaluations of this witness on its four supported edges are the elementary facts needed before collapsing 875-term edge inner products.
proof idea
Unfold the piecewise definition of the shear. The value on $BC$ is the third branch ($-1$), reached only after ruling out equality with the two $x$-edges that carry $+1$. Those two inequalities are discharged by decide on the concrete edge encodings; simp then reduces the nested if to $-1`. No algebraic lemmas beyond definitional unfolding are required.
why it matters
This is one of the four support evaluations that make the shear witness computationally usable. Downstream, periodicEdgeInnerProduct5_rectangleShearFace5_left collapses any inner product against the shear to the four-edge combination $\eta(AB)+\eta(DC)-\eta(BC)-\eta(AD)$, quoting this lemma for the $BC$ term. That collapse feeds rectangleShearFace5_inner_self_eq_four, which shows the self-inner-product equals $4$ and thereby normalizes the witness.
In the broader Recognition gravity program the shear sits in the complement of the conformal ansatz on the edge space, giving a concrete non-conformal edge perturbation on the eight-tick-compatible $D=3$ lattice. It is scaffolding for the tensor sector beyond pure conformal strain, not a claim about continuum GR or about the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.