rectangleShearFace5_inner_self_eq_four
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, the explicit face-shear edge perturbation has squared L2 norm equal to 4. Anyone proving that this shear lies outside the vertex-conformal subspace cites the identity: conformal modes are orthogonal to the shear, so a nonzero self-product blocks membership. The proof rewrites the 875-term product to the four supported edges and evaluates them by norm_num.
Claim. Let $\eta$ be the rectangle face-shear edge field on the $5\times 5\times 5$ periodic torus ($+1$ on the two opposite $x$-edges of the unit square, $-1$ on the two opposite $y$-edges, and $0$ elsewhere). Then the periodic edge inner product satisfies $\langle\eta,\eta\rangle=4$.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector of a 3D Regge triangulation 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 $N=5$ periodic Freudenthal 3-torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal rank is at most 125, strictly less than the edge dimension.
The witness rectangleShearFace5 places strain $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges of the unit coordinate square with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$, and zero on the remaining 871 edges. The periodic edge inner product is the standard Euclidean product on $\mathbb{R}^{875}$. An upstream collapse lemma shows that the inner product of this shear against any edge field $\eta$ reduces to the four supported edges: $\eta(AB)+\eta(DC)-\eta(BC)-\eta(AD)$.
proof idea
One rewrite chain. First apply the collapse lemma periodicEdgeInnerProduct5_rectangleShearFace5_left with $\eta$ equal to the shear itself, reducing the self-product to the four face-edge values. Then rewrite each value by the pointwise evaluation lemmas: the two $x$-edges evaluate to $+1$ and the two $y$-edges to $-1$. The resulting arithmetic expression $1+1-(-1)-(-1)$ is discharged by norm_num, yielding 4.
why it matters
This identity is the numerical engine of the typed non-conformality proof for the face shear. Downstream, rectangleShearFace5_not_conformal_typed assumes the shear lies in the periodic conformal log-subspace, invokes orthogonality of the shear to every conformal mode (hence to itself), rewrites the self-product to 4, and obtains $4=0$. The same witness also feeds the encoded-coordinate non-conformality statement and the broader existence claim that the conformal range is a proper subspace of the 875-dimensional edge space.
In the Recognition gravity lane this closes the concrete half of the dimension-gap story on the $N=5$ torus: not only is conformal rank $\le 125<875$, but an explicit, localized shear of squared norm 4 sits outside the conformal slice. No open scaffolding remains for this particular identity; it is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.