xUniformStrain5_apply_BC
plain-language theorem explainer
The uniform +x edge strain on the 5×5×5 periodic Freudenthal torus evaluates to zero on the right y-edge of the unit face square. Anyone pairing that anisotropic shear against the rectangle face shear, or proving the strain is non-conformal, cites this pointwise evaluation. The proof decides the edge is not in the +x displacement class and simplifies the piecewise definition.
Claim. On the $5\times 5\times 5$ periodic Freudenthal 3-torus, the uniform $+x$ edge strain (value $1$ on every edge of displacement class $0$, and $0$ on the other six classes) evaluates to $0$ on the right $y$-edge of the unit coordinate square (base at vertex $B$, displacement class $+y$).
background
Lane 3 of the Seven-Gaps gravity work studies the edge (tensor) sector 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; the module measures how small that conformal slice is inside the full edge-perturbation space on the concrete $N=5$ periodic 3-torus ($125$ vertices, $875$ edges).
The uniform $+x$ strain is the globally anisotropic edge perturbation that puts unit strain on every edge of displacement class $0$ ($+x$) and zero on the other six classes. The right $y$-edge of the unit face square is the periodic edge with base at face vertex $B$ and displacement class $1$ ($+y$). Because that class is not $+x$, the strain definition forces the value zero on this edge.
These pointwise evaluations feed the discrete $L^2$ pairing against the localized rectangle shear and the direct non-conformality argument that reuses the TensorShearSector rectangle obstruction.
proof idea
Decide that the displacement class of the right $y$-edge is not $0$ (the $+x$ class); this is a finite enumeration, discharged by decide. Then simp unfolds the piecewise definition of the uniform $+x$ strain and rewrites the if e.disp = 0 then 1 else 0 branch to $0$ under that inequality. No external lemmas beyond the two definitions are required.
why it matters
This is one of the four face-edge evaluations needed to compute the pairing of the rectangle face shear against the uniform $+x$ strain, which equals $2$ and shows the two witnesses are not orthogonal in a trivial way. The same family of evaluations is reused when proving the uniform $+x$ strain is not vertex-conformal: endpoint averages on the witness square force horizontal strain $1$ and vertical strain $0$, which the TensorShearSector rectangle obstruction forbids.
In the broader Seven-Gaps story, these explicit shear witnesses certify that the conformal image is a proper subspace of the edge-perturbation space on the $N=5$ torus (rank at most $125$ versus edge dimension $875$). That gap is the concrete tensor-sector content beyond the conformal ansatz in the gravity lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.