xUniformStrain5_apply_AB
plain-language theorem explainer
On the N=5 periodic Freudenthal 3-torus, the uniform +x edge strain evaluates to 1 on the bottom +x edge of the unit face square. Anyone computing face-shear inner products or conformal-obstruction witnesses cites this pointwise value. The proof is a definitional simplification once that edge's displacement class is identified as 0.
Claim. Let $\varepsilon_x$ be the edge perturbation that places unit strain on every $+x$ edge of the $N=5$ periodic 3-torus and zero on all other displacement classes. If $e_{AB}$ is the bottom $+x$ edge of the unit coordinate square (corners $(0,0,0)$ through $(0,1,0)$), then $\varepsilon_x(e_{AB}) = 1$.
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector of a 3D Regge triangulation beyond the vertex-conformal ansatz. That ansatz assigns one scalar per vertex and induces the log-strain $(\xi_u + \xi_v)/2$ on each edge ${u,v}$. The ambient space is far larger: on the concrete $5\times 5\times 5$ periodic Freudenthal 3-torus one has 125 vertices and 875 edges, so the conformal image is a proper subspace.
Edges of the periodic torus are classified by a base vertex and a displacement class in ${0,\ldots,6}$, with class $0$ the $+x$ direction. The bottom $+x$ edge of the unit face square is the edge whose base is the origin corner and whose displacement is $0$. The uniform $+x$ strain is the globally anisotropic perturbation that returns $1$ exactly on displacement class $0$ and $0$ elsewhere; it is a pure-shear-type witness complementary to the conformal slice.
proof idea
By definition the bottom $+x$ face edge has displacement class $0$. Unfolding the uniform $+x$ strain (the piecewise definition that returns $1$ on class $0$ and $0$ otherwise) and simplifying with that equality yields the value $1$. No external lemmas are required.
why it matters
This evaluation is the first of four pointwise facts needed to compute the inner product of the uniform $+x$ strain against the localized rectangle face shear: that pairing equals $2$, confirming the two witnesses are not orthogonal in a trivial way. The same evaluation is reused when proving the uniform $+x$ strain is not vertex-conformal: the conformal endpoint-average form on the witness square would force horizontal average $1$ and vertical average $0$, which the rectangle obstruction of TensorShearSector forbids. Together these close the explicit shear-complement story on the $N=5$ torus that the module header advertises (non-conformal typed and encoded witnesses, dimension gap $125 < 875$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.