xUniformStrain5_apply_DC
plain-language theorem explainer
On the 5×5×5 periodic torus, the uniform +x edge strain evaluates to 1 on the top face edge D→C. Anyone computing inner products or conformal-obstruction checks against that global shear cites this evaluation. The proof is a two-line simplification: the edge has displacement class 0, and the strain is defined to be 1 exactly on that class.
Claim. Let $e_{DC}$ be the top $+x$ edge of the unit coordinate square on the $N=5$ periodic Freudenthal 3-torus (displacement class $0$). The uniform $+x$ strain field, which equals $1$ on every edge of displacement class $0$ and $0$ otherwise, satisfies $\varepsilon_x(e_{DC}) = 1$.
background
Lane 3 of the Seven-Gaps gravity program studies the edge (tensor) sector of discrete strain on a finite 3D Regge complex, 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 the full edge-perturbation space; on the concrete $5\times 5\times 5$ periodic torus one has $n_V=125$ and $n_E=875$, so the conformal image is a proper subspace.
Edges of the periodic torus are encoded by a base vertex and a displacement class in ${0,\ldots,6}$. Class $0$ is the $+x$ direction. The face edge $D\to C$ is defined with base at face vertex $D$ and displacement $0$, so it is a pure $+x$ edge of the unit square with corners $(0,0,0)$, $(1,0,0)$, $(1,1,0)$, $(0,1,0)$.
The uniform $+x$ strain is the globally anisotropic field that puts value $1$ on every edge with displacement class $0$ and $0$ on the other six classes. It is a pure-shear-type witness used to probe the complement of the conformal range.
proof idea
Term-mode proof by definition chase. First record that the displacement of the top face edge $D\to C$ is definitionally $0$ (rfl). Unfold the uniform $+x$ strain (the piecewise definition that returns $1$ precisely when disp = 0) and simplify with that fact; the conditional collapses to $1$.
why it matters
This is a pointwise evaluation lemma for the second explicit shear witness of the edge-tensor sector. Downstream, rectangleShearFace5_inner_xUniformStrain5 uses it (with the three sibling evaluations on $AB$, $BC$, $AD$) to show that the face rectangle shear pairs to $2$ against the uniform $+x$ strain under the periodic edge inner product, confirming the two witnesses are not orthogonal in a trivial way.
It is also consumed by xUniformStrain5_not_conformal_typed, which proves the uniform $+x$ strain lies outside the vertex-conformal subspace by feeding the four face-edge values into the rectangle obstruction from TensorShearSector (horizontal average $1$, vertical average $0$, hence $h\neq v$). Together these close the "explicit shear witness" bullet of the module status header: the conformal ansatz is a proper subspace of edge perturbations on the $N=5$ torus, witnessed by concrete non-conformal fields rather than dimension counting alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.