xUniformStrain5
plain-language theorem explainer
Defines the uniform +x edge strain on the 5×5×5 periodic Freudenthal torus: value 1 on every edge of displacement class 0, and 0 on the other six classes. It is the global pure-shear-type witness used to prove the conformal ansatz is a proper subspace of edge perturbations. Citation target for non-conformality and inner-product calculations against the rectangle face shear. The body is a one-line piecewise assignment on the typed edge displacement.
Claim. Let $E_5$ be the set of typed edges of the $5\times 5\times 5$ periodic Freudenthal 3-torus. The uniform $+x$ strain is the real-valued edge field $\sigma_x: E_5\to\mathbb{R}$ given by $\sigma_x(e)=1$ if the displacement class of $e$ is $0$ (the $+x$ direction) and $\sigma_x(e)=0$ otherwise.
background
Lane 3 of the Seven-Gaps gravity development studies the edge (tensor) sector of a finite Regge triangulation beyond the vertex-conformal ansatz. That ansatz assigns one scalar potential per vertex and induces the log-strain $(\xi_u+\xi_v)/2$ on each edge ${u,v}$. The ambient space is the full real vector space of edge perturbations.
On the concrete $N=5$ periodic Freudenthal 3-torus one has $n_V=125$ vertices and $n_E=875$ edges, so the conformal image has rank at most 125 and cannot fill the 875-dimensional edge space. Typed edge perturbations are functions PeriodicEdge5 → ℝ, abbreviated PeriodicEdgePerturbation5. Displacement classes label the seven Freudenthal edge directions; class 0 is the positive $x$-axis.
The uniform $+x$ strain is the second explicit shear witness in the file (after the localized rectangle face shear). It is globally anisotropic: constant unit strain on every $+x$ edge and zero on all other directions.
proof idea
Pure definition, not a proved statement. The body is the piecewise map sending a typed edge $e$ to $1$ when $e.\mathrm{disp}=0$ and to $0$ otherwise. Downstream evaluation lemmas (xUniformStrain5_apply_AB, _DC, _BC, _AD) discharge the branch by rfl or decide on the displacement of the four unit-square edges, then simp.
why it matters
Supplies the global pure-shear witness that the conformal slice is proper inside the edge-perturbation space on the $5\times 5\times 5$ torus. Downstream, the four face-edge evaluations feed the inner-product identity rectangleShearFace5_inner_xUniformStrain5 (pairing equals 2 against the conformal-orthogonal face shear) and the non-conformality theorems xUniformStrain5_not_conformal_typed and xUniformStrain5Encoded_not_conformal, which reuse the rectangle obstruction. Also supports xUniformStrain5_nonzero_orthogonal_component.
In the Recognition gravity stack this is concrete evidence that tensor (shear) degrees of freedom exist beyond vertex-conformal log-strain on a periodic 3-complex, aligning with the $D=3$ spatial forcing (T8) and the need for a genuine edge sector in discrete gravity. It does not itself close a forcing-chain step; it is a computational witness inside the Seven-Gaps edge-tensor lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.