xUniformStrain5_apply_AD
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, the uniform +x edge strain vanishes on the left y-edge of the unit face square. Anyone computing inner products or conformal checks against that global anisotropic mode cites this evaluation. The proof is a one-step simplification: the edge’s displacement class is not the +x class, so the piecewise definition returns zero.
Claim. Let $e_{AD}$ be the left $y$-edge of the unit coordinate square on the $N=5$ periodic torus (displacement class $1$). The uniform $+x$ strain mode, which equals $1$ on every edge of displacement class $0$ and $0$ otherwise, evaluates to $0$ at $e_{AD}$.
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 full edge-perturbation space on a finite Regge complex is much larger. On the concrete $5\times5\times5$ periodic Freudenthal 3-torus one has $n_V=125$ and $n_E=875$, so the conformal image is a proper subspace.
The uniform $+x$ strain is the globally anisotropic mode that puts unit strain on every edge whose displacement class is $0$ (the $+x$ class) and zero on the other six classes. The witness square has corners $A,B,C,D$ with edges $AB,BC,CD,DA$; the left $y$-edge $A\to D$ is coded as base vertex $A$ with displacement $1$. Evaluating the mode on that edge is the elementary building block for both the rectangle-shear inner product and the non-conformality argument that reuses the TensorShearSector rectangle obstruction.
proof idea
By definition the left $y$-edge has displacement field equal to $1$, hence not equal to $0$. Unfold the piecewise definition of the uniform $+x$ strain: the if e.disp = 0 then 1 else 0 branch is forced into the else arm, giving $0$. The inequality disp ≠ 0 is discharged by decide on the concrete PeriodicEdge5 literal; simp finishes.
why it matters
This evaluation is one of the four face-edge specializations needed to compute the inner product of the rectangle face shear against the uniform $+x$ strain, which equals $2$ and exhibits a concrete conformal-orthogonal shear direction. The same family of evaluations feeds the typed non-conformality proof: endpoint averages on the witness square force horizontal strain $h=1$ and vertical strain $v=0$, which the TensorShearSector rectangle obstruction forbids for any vertex-conformal mode.
In the broader Recognition gravity stack this sits inside the edge-tensor sector that witnesses the dimension gap between conformal rank ($\le 125$) and full edge space ($875$) on the $N=5$ torus. It is fully proved scaffolding for the shear complement, not a forcing-chain landmark (T0–T8), but it makes the abstract proper-subspace claim explicit and reusable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.