rectangleShearFace5Encoded
plain-language theorem explainer
The unit-face rectangle shear on the N=5 periodic Freudenthal 3-torus, rewritten as an edge perturbation indexed by the encoded finite edge set Fin nE. Gravity and discrete-geometry workers cite it as the concrete non-conformal witness in the edge/tensor sector. It is a one-line pushforward of the typed shear through the typed-to-encoded edge equivalence.
Claim. Let $\varepsilon$ be the typed periodic edge perturbation that 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)$ on the $N=5$ torus (and $0$ elsewhere). Its encoded form is the edge perturbation on $\mathrm{Fin}\,n_E$ obtained by composing $\varepsilon$ with the periodic-edge equivalence of the triangulation.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector of discrete metric perturbations on the $5\times5\times5$ periodic Freudenthal 3-torus. The vertex-conformal ansatz assigns one scalar per vertex and induces the log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. That image is a proper linear subspace of the full edge-perturbation space: $n_V=125$ vertices versus $n_E=875$ edges, so conformal rank is at most 125.
An explicit shear complement is needed as a witness. The typed object places $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges of one unit face, and zero on the remaining 871 edges. Encoded edge perturbations are the same data reindexed by the finite edge set of the triangulation kernel $K$; the map that pushes a typed periodic perturbation across the edge equivalence produces the encoded view used by finrank and range arguments.
proof idea
One-line definitional wrapper: apply the typed-to-encoded pushforward to the typed rectangle shear. No tactics, no lemmas beyond the definition of that pushforward (evaluate the typed strain at the periodic edge corresponding to each encoded index).
why it matters
This is Deliverable 4 in encoded coordinates: the explicit localized face shear that realizes the dimension gap between the conformal slice and the full edge space. It is the witness in the constructive existence theorem (there exists a non-conformal encoded edge perturbation) and in the direct non-conformality theorem for the encoded shear. The Lane 3 capstone packages the rank bound $\le 125$, the equality $\mathrm{finrank}=875$, and non-conformality of this encoded shear into one statement that the edge/tensor sector properly exceeds the conformal ansatz on the $N=5$ torus. Downstream non-conformality is reduced to the typed obstruction via the typed/encoded conformal equivalence, so the encoding is bookkeeping that aligns the witness with finrank statements rather than a new geometric claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.