xUniformStrain5Encoded_not_conformal
plain-language theorem explainer
The uniform x-directed edge strain on the 5×5×5 periodic Freudenthal 3-torus stays non-conformal after transport into encoded edge coordinates. Discrete-gravity and Regge workers cite it when they need an explicit shear witness outside the vertex-potential image in the encoded API. The proof is a one-line transfer of the typed non-conformality result across the typed/encoded conformal equivalence.
Claim. The image of the uniform $x$-strain under the canonical encoding of periodic edge data on the $5\times 5\times 5$ torus is not a conformal edge perturbation of the associated triangulation $K$.
background
The module treats the edge (tensor) sector of discrete gravity beyond the vertex-conformal ansatz. That ansatz places one real scalar at each vertex and induces the log-strain $(\xi_u+\xi_v)/2$ on the edge ${u,v}$. On any finite 3D Regge complex the conformal image therefore has rank at most the vertex count. On the working $N=5$ periodic torus one has $n_V=125$ and $n_E=875$, so the conformal slice is a proper subspace of the full edge-perturbation space.
Two concrete shear witnesses are built. The uniform $x$-strain is constant on edges parallel to the $x$-axis (typed picture). Its non-conformality is first proved in typed coordinates by recycling the rectangle-face obstruction. Encoded coordinates are the form used by the broader edge-tensor stack, so the same fact must be restated after the canonical map from periodic to encoded edge data.
The bridge lemma equates membership of a typed periodic edge field in the conformal log-subspace with the encoded predicate IsConformalEdgePerturbation for PeriodicTorus5.K.
proof idea
Term-mode proof by contradiction. Assume the encoded uniform $x$-strain is conformal. The right-to-left direction of the typed/encoded bridge then places the typed field in the periodic conformal log-subspace, contradicting the already-proved typed non-conformality of the uniform $x$-strain. Pure transfer across the equivalence; no new geometric argument.
why it matters
Lane 3 of the Seven-Gaps gravity program needs explicit non-conformal edge modes to show that the tensor (shear) sector is strictly larger than the conformal ansatz on the working $5^3$ torus. The typed non-conformality of the uniform $x$-strain already exists; this declaration supplies the encoded twin so encoded-edge arguments can invoke the witness without leaving that API. The module status header lists both the rectangle-face encoded witness and this result among the fully proved shear examples, sitting next to the dimension gap $125<875$ that forces a nontrivial shear complement. No downstream theorem yet consumes it. In the RS discrete-gravity setting it supports a genuine edge-tensor sector on the $D=3$ lattice rather than a pure scalar conformal reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.