rectangleShearFace5Encoded_not_conformal
plain-language theorem explainer
The encoded rectangle-face shear on the N=5 periodic Freudenthal 3-torus is not vertex-conformal. Gravity and discrete-Regge workers cite it as the explicit encoded witness that the edge (tensor) sector properly exceeds the conformal ansatz. The proof is a one-line transfer: push the encoded claim across the typed/encoded conformal equivalence, then apply the already-proved typed non-conformality.
Claim. Let $\varepsilon$ be the encoded edge perturbation on the $N=5$ periodic Freudenthal 3-torus that places strain $+1$ on the two opposite $x$-edges and $-1$ on the two opposite $y$-edges of one unit coordinate face (and $0$ elsewhere). Then $\varepsilon$ is not a vertex-conformal edge perturbation: it does not lie in the image of the conformal log-strain map from vertex potentials.
background
Lane 3 of the Seven-Gaps gravity program studies the edge (tensor) sector of a finite 3D Regge complex beyond the vertex-conformal ansatz. That ansatz assigns one real scalar per vertex and induces the symmetric log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. Membership in the image of this linear map is the predicate "is a conformal edge perturbation."
On the concrete $5\times5\times5$ periodic Freudenthal 3-torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal image has rank at most 125 inside an 875-dimensional edge space. The module builds an explicit localized witness: the rectangle/shear pattern on one unit face, with strain $+1$ on the two opposite $x$-edges, $-1$ on the two opposite $y$-edges, and $0$ on the remaining 871 edges. That pattern is defined first in typed periodic edge coordinates, then pushed to the encoded edge-perturbation type used by the conformal predicate.
Upstream, periodicConformalLogSubspace5_iff_encodedConformal identifies the typed conformal slice with the encoded conformal predicate across the canonical edge equivalence, and rectangleShearFace5_not_conformal_typed already rules out a vertex-conformal realization in typed coordinates.
proof idea
Term-mode proof by contradiction. Assume the encoded rectangle shear is conformal. Apply the reverse direction of the typed/encoded equivalence (periodicConformalLogSubspace5_iff_encodedConformal) to the typed rectangle shear, obtaining that the typed pattern lies in the typed conformal log-subspace. Feed that into the already-proved typed non-conformality lemma (rectangleShearFace5_not_conformal_typed) to reach False. No new geometric argument is introduced here; the work is pure transport across the encoding equivalence.
why it matters
This is Deliverable 4 in encoded form: the explicit non-conformal edge perturbation needed so that existence is constructive rather than pure dimension-counting. Downstream, periodicTorus5_exists_nonconformal_constructive packages the pair (encoded rectangle shear, this theorem) as a concrete witness, and the Lane 3 capstone periodicTorus5_edge_tensor_sector_beyond_conformal conjoins the rank bound (conformal rank $\le 125$, edge space dimension $875$) with this same non-conformality statement.
In the Recognition gravity stack the point is structural: the edge/tensor sector on a realistic periodic 3-complex is strictly larger than any vertex-scalar conformal ansatz, so shear degrees of freedom are forced rather than optional. The result sits inside the proved (zero-sorry) block of the EdgeTensorSector module; it does not itself touch the forcing chain T0–T8, but it supplies the discrete geometric gap those continuum claims eventually rest on when gravity is read off Regge data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.