rectangleShearFace5_nonzero_in_orthogonal_complement
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal 3-torus, the explicit rectangle face shear is a nonzero edge strain orthogonal to every vertex-conformal log-strain. Anyone citing the concrete shear complement inside the 875-dimensional edge space uses this. The proof is a one-line pairing of the already-proved orthogonality and nonzeroness lemmas.
Claim. Let $\varepsilon_{\square}$ be the rectangle face shear on the $N=5$ periodic torus (strain $+1$ on the two opposite $x$-edges of the unit square, $-1$ on the two opposite $y$-edges, $0$ elsewhere). Then $\langle \varepsilon_{\square}, c \rangle = 0$ for every edge perturbation $c$ in the vertex-conformal log-strain subspace, and $\varepsilon_{\square} \neq 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 potential per vertex and induces the log-strain $(\xi_u + \xi_v)/2$ on each edge ${u,v}$. On the concrete $5\times 5\times 5$ periodic Freudenthal 3-torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal image is a proper subspace of the full edge-perturbation space.
The witness rectangleShearFace5 localizes a classical rectangle shear on one coordinate face: strain $+1$ on the two opposite $x$-edges, $-1$ on the two opposite $y$-edges, and $0$ on the remaining 871 edges. The conformal slice is the set of periodic edge fields that arise as encoded conformal log-strains of some vertex potential. The periodic edge inner product pairs two such fields by summing products of their edge values.
Upstream, orthogonality of this shear to every conformal field follows from endpoint averaging around the square: $(\varphi_A+\varphi_B)+(\varphi_D+\varphi_C)-(\varphi_B+\varphi_C)-(\varphi_A+\varphi_D)=0$. Nonzeroness is the elementary check that the value on one $x$-edge is $1$.
proof idea
Term-mode pairing of two prior theorems. The left conjunct is exactly rectangleShearFace5_inner_conformal_eq_zero (inner product against any conformal $c$ vanishes by the telescoping endpoint identity). The right conjunct is exactly rectangleShearFace5_ne_zero (the shear is not the zero function because its value on the AB edge is $1$). No new algebra is performed here.
why it matters
This is Deliverable 5 of the orthogonal-split program in the edge-tensor sector: it upgrades the abstract dimension gap (conformal rank $\le 125 < 875$) to an explicit nonzero vector in the orthogonal complement of the conformal slice. The module already proves the shear is not vertex-conformal in typed and encoded coordinates; the present statement packages the stronger Hilbert-space fact that the shear sits in the metric orthogonal complement, not merely outside the range.
In the Recognition gravity lane this supplies a concrete tensor-mode witness beyond pure conformal (scalar) strain on the discrete 3-torus, the setting used to measure how much of the edge space the conformal ansatz misses. No downstream consumers are wired yet (used_by is empty), so this is presently a terminal citation point for the orthogonal-split witness form rather than an intermediate lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.