rectangleShearFace5_inner_xUniformStrain5
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal 3-torus, the localized rectangle face shear pairs with the global uniform +x strain under the edge inner product to the constant 2. Gravity and Regge analysts cite this as the concrete pairing that shows the uniform x-strain is not orthogonal to the shear complement. The proof rewrites the 875-term product to four supported edges, substitutes the four strain values, and evaluates by arithmetic.
Claim. On the $N=5$ periodic 3-torus edge space, the standard Euclidean inner product of the localized rectangle face shear (strain $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges of one coordinate square) with the uniform $+x$ strain equals $2$.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector of a 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 Freudenthal torus one has $n_V=125$ and $n_E=875$, so the conformal rank is at most 125 and a large shear complement remains.
The localized witness rectangleShearFace5 puts strain $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges of the unit square with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$, and zero elsewhere. The global witness xUniformStrain5 is unit strain on every edge of displacement class $+x$ and zero on the other six classes. The periodic edge inner product is the ordinary sum of products of edge values over all 875 edges.
An upstream collapse lemma states that the inner product of the face shear against any edge field reduces exactly to the signed combination of the four supported edges: $\eta(AB)+\eta(DC)-\eta(BC)-\eta(AD)$.
proof idea
One short tactic proof. First rewrite by the collapse lemma periodicEdgeInnerProduct5_rectangleShearFace5_left, which replaces the full 875-term product by the four-edge signed sum against the uniform $x$-strain. Then rewrite each of those four edge values by the pointwise evaluation lemmas for xUniformStrain5 on the AB, DC, BC, and AD face edges (the two $x$-class edges contribute $1$, the two $y$-class edges contribute $0$). The resulting arithmetic expression $1+1-0-0$ is discharged by norm_num, yielding $2$.
why it matters
This pairing is the numerical engine behind xUniformStrain5_nonzero_orthogonal_component, which exhibits a nonzero orthogonal projection of the uniform $x$-strain onto the complement of the conformal subspace: the face shear annihilates every conformal edge field, yet pairs nontrivially with the uniform $x$-strain. That fact upgrades the abstract dimension gap (conformal rank $\le 125 < 875$) to an explicit, globally anisotropic shear mode that cannot be absorbed into vertex potentials.
In the Recognition gravity stack this is part of the Seven-Gaps program separating pure conformal (trace) edge data from genuine tensor shear on the forced $D=3$ eight-tick geometry. It does not itself force new constants; it supplies a concrete, fully proved witness that the edge sector is strictly larger than the conformal ansatz on the working torus used throughout the lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.