strainCurrent_axisTTCross_zero_twelve
plain-language theorem explainer
On the sixteen-site Freudenthal patch, the linearized strain current of the pure cross polarization H_{23}=H_{32}=1 evaluates to 2 on the edge from site 0 to site 12. Gravity analysts cite this as the concrete nonzero witness that the metric edge image is nontrivial. The proof unfolds the strain quadratic form, substitutes the binary displacement (0,0,1,1), and reduces by finite summation and arithmetic.
Claim. Let $H$ be the $4\times 4$ matrix with $H_{23}=H_{32}=1$ and all other entries zero. Let $D$ be the integer displacement of the patch edge from site $0$ to site $12$, namely $D=(0,0,1,1)$. Then the edge strain $\sum_{i,j} H_{ij} D_i D_j$ equals $2$.
background
This module freezes the linearized metric edge image on the sixteen-site Freudenthal patch used in the order-sensitive gravity proposition. A matrix perturbation $H:\mathrm{Fin},4\to\mathrm{Fin},4\to\mathbb{R}$ produces a strain current on patch edges by the quadratic form $\mathrm{edgeStrain}(H,D)=\sum_{i,j} H_{ij} D_i D_j$, where $D$ is the integer displacement between two of the sixteen binary patch sites. The image of this map is the set of admissible edge currents coming from flat-patch metric perturbations.
The witness matrix used here is the pure cross polarization with only $H_{23}=H_{32}=1$ (unnormalized). Upstream, patchDisp_zero_twelve records that the displacement from site 0 to site 12 is exactly $(0,0,1,1)$ in the four spacetime axes. The same strain formula appears in the Regge exact flat Hessian Bloch-symbol analysis, so the arithmetic here is compatible with that chain.
proof idea
Unfold the strain-current definition to the edge-strain quadratic form. Rewrite the displacement via patchDisp_zero_twelve, obtaining $D=(0,0,1,1)$. Unfold the cross-polarization matrix and the double sum over $\mathrm{Fin},4$. Only the two off-diagonal terms $H_{23}D_2 D_3$ and $H_{32}D_3 D_2$ survive; each contributes $1$, and norm_num closes $1+1=2$.
why it matters
The parent theorem MetricEdgeImage_nontrivial needs a single concrete nonzero value of some strain current to prove that the metric edge image is not the zero functional. This lemma supplies that value: after applying function extensionality at sites $(0,12)$, the equality to 2 contradicts the assumption that the current vanishes everywhere. Together with the companion membership axisTTCross_in_MetricEdgeImage, it discharges the nontriviality half of the module honesty claim (nontriviality, symmetry, properness against antisymmetric posting) for linearized flat-patch metric perturbations. In the broader Recognition gravity stack this is a local algebraic witness inside the Freudenthal-cover edge-current analysis, not a global curvature or continuum GR statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.