periodicTorus5_exists_nonconformal_constructive
plain-language theorem explainer
On the $N=5$ periodic Freudenthal 3-torus there is an explicit encoded edge strain that lies outside the vertex-conformal ansatz. Gravity and discrete-geometry workers citing the shear complement of the conformal slice use this constructive form rather than a pure existence claim. The proof is a one-line pair: the rectangle face-shear witness together with its already-proved non-conformality.
Claim. There exists an encoded edge perturbation $\varepsilon$ on the $5\times 5\times 5$ periodic Freudenthal 3-torus such that $\varepsilon$ is not vertex-conformal: it does not lie in the image of the conformal log-strain map sending a real potential at each vertex $u$ to the edge value $(\xi_u+\xi_v)/2$ on $\{u,v\}$.
background
The module treats Lane 3 of the Seven-Gaps program: the edge (tensor) sector of a 3D Regge complex beyond the pure conformal ansatz. That ansatz assigns one real scalar $\xi$ per vertex and induces the log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. The full edge-perturbation space is much larger; the file packages the ansatz as an $\mathbb{R}$-linear map from vertex potentials into edge strains and measures its image on the concrete $5\times 5\times 5$ periodic Freudenthal 3-torus ($n_V=125$, $n_E=875$).
A perturbation is called conformal when it lies in that image. The sibling rank bound already shows the conformal range has finrank at most $125<875$, so a non-conformal edge strain must exist. The present declaration supplies an explicit one rather than a pure dimension argument.
The witness is the unit coordinate-square shear: strain $+1$ on the two $x$-edges and $-1$ on the two $y$-edges of the face with corners $(0,0,0),(1,0,0),(1,1,0),(0,1,0)$, pushed forward into encoded $\mathrm{Fin},n_E$ coordinates.
proof idea
One-line constructive term proof. The existential is inhabited by the pair consisting of the encoded rectangle face shear and the upstream theorem that this encoded strain is not conformal. That upstream fact reduces encoded non-conformality to the typed rectangle obstruction via the equivalence between the periodic conformal log-subspace and its encoded counterpart, then invokes the typed non-conformality of the same face shear. No new calculation is performed here.
why it matters
Closes the constructive half of the Lane-3 deliverable that the conformal ansatz is a proper subspace of edge strains on the $N=5$ torus. The non-constructive sibling already gives existence from the rank gap ($\le 125<875$); this form names the shear witness so downstream discrete-gravity arguments can point at a concrete pure-shear mode rather than an abstract complement vector.
In the Recognition gravity stack this is the edge-tensor counterpart of leaving the conformal (scalar) sector: shear modes on the Freudenthal lattice are the discrete stand-in for tensor degrees of freedom beyond a pure Weyl rescaling. The module header lists it among the fully proved items (zero sorry, no silent hypotheses). No downstream consumers are wired yet; the natural parents are any gluing or gap-closure theorems that need an explicit non-conformal test strain on the periodic 3-torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.