rectangleShearFace5
plain-language theorem explainer
Explicit edge-strain witness on the 5×5×5 periodic Freudenthal torus: +1 on the two opposite x-edges and −1 on the two opposite y-edges of one coordinate face, zero elsewhere. Gravity and discrete-geometry workers cite it as the concrete shear complement to the vertex-conformal ansatz. The body is a four-branch piecewise definition on the typed periodic edges.
Claim. Define the rectangle shear on the unit face of the $N=5$ periodic torus by the edge function that sends the bottom and top $x$-edges to $+1$, the left and right $y$-edges to $-1$, and every other typed periodic edge to $0$.
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 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 actual $5\times5\times5$ periodic Freudenthal 3-torus ($125$ vertices, $875$ edges).
PeriodicEdgePerturbation5 is simply a real-valued function on typed periodic edges. The four supporting edges of the unit square with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$ are named: bottom $x$-edge $A\to B$, top $x$-edge $D\to C$, right $y$-edge $B\to C$, left $y$-edge $A\to D$. The present definition places the classical rectangle/shear pattern on exactly those four edges.
proof idea
Pure definition, not a proof. The function is introduced by nested equality tests on the four face edges: value $1$ on the two $x$-edges, $-1$ on the two $y$-edges, and $0$ on the residual $871$ edges. Downstream apply lemmas discharge each branch by simp plus decide inequalities among the four edge constants.
why it matters
This is the explicit localized shear witness advertised in the module header. It feeds the pointwise evaluation lemmas, the collapse of the $875$-term inner product to the four supported edges, the encoded-coordinate twin, and the non-conformality theorems (rectangleShearFace5_not_conformal_typed, rectangleShearFace5Encoded_not_conformal). Together with the rank gap (conformal image rank $\le 125 < 875$), it shows the conformal ansatz is a proper subspace and that a concrete shear mode lives in the complement. In the Recognition gravity stack this is the discrete tensor-sector evidence that edge degrees of freedom are not exhausted by vertex potentials on the eight-tick / $D=3$ lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.