periodicEdgeInnerProduct5_rectangleShearFace5_left
plain-language theorem explainer
The Euclidean inner product of the localized face-shear edge field against any periodic edge perturbation on the 5×5×5 torus collapses from 875 terms to the four supported edges of the unit square. Anyone proving conformal-orthogonality or norm identities for this shear witness cites the reduction. The argument is a Finset sum-subset filter plus the four pointwise shear values, finished by ring.
Claim. For every periodic edge perturbation $\eta$ on the $5\times 5\times 5$ Freudenthal 3-torus, the edge inner product of the rectangle face shear $\sigma$ against $\eta$ equals $\eta(e_{AB})+\eta(e_{DC})-\eta(e_{BC})-\eta(e_{AD})$, where $\sigma$ places $+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)$.
background
Lane 3 of the Seven-Gaps gravity development 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 present module measures how small that conformal image is inside the full edge-perturbation space of the concrete $N=5$ periodic Freudenthal 3-torus ($n_V=125$, $n_E=875$).
The face shear is the explicit localized witness: strain $+1$ on the two $x$-edges and $-1$ on the two $y$-edges of the unit coordinate square. The periodic edge inner product is the plain Euclidean sum over all 875 edges. Because the shear vanishes off those four edges, the full sum is expected to reduce to a four-term alternating combination of $\eta$ on the square boundary.
This reduction is the computational engine behind the later claims that the shear is conformal-orthogonal, has self-norm $4$, and pairs nontrivially with the uniform $x$-strain.
proof idea
Restrict the universal Finset sum that defines the inner product to the four-edge support of the shear. First record that those four edges form a subset of Finset.univ. Off the support, the shear vanishes by the pointwise off-support lemma, so each product term is zero by zero_mul. Finset.sum_subset therefore replaces the 875-term sum by the four-edge sum. Expand that sum with four successive sum_insert/sum_singleton steps (using the disjointness lemmas for the four edges), substitute the four on-support values $+1,+1,-1,-1$, and finish with ring.
why it matters
This is the workhorse identity for the explicit shear witness in the edge-tensor sector. Three immediate parents apply it: conformal-orthogonality of the face shear (endpoint averages telescope around the square to zero), the self-inner-product identity equaling $4$ (so the shear is a nonzero vector in the conformal orthogonal complement), and the pairing of the shear against the uniform $x$-strain equaling $2$.
Together those facts discharge the concrete half of the dimension-gap story on the $N=5$ torus: the conformal range has rank at most $125<875$, and an explicit nonzero vector orthogonal to that range is exhibited. In the broader Recognition gravity program this supplies a typed, fully proved tensor-mode witness beyond the pure conformal (scalar) ansatz on a compact 3-manifold with $D=3$ forced by the foundation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.