edgeStrain_neg
plain-language theorem explainer
Edge strain is odd in the metric perturbation: strain of −H equals minus strain of H, for any integer edge displacement in 4D. Anyone bilinearizing the midpoint Bloch first variation or proving strain subtraction cites this. The proof is a one-line wrapper of scalar homogeneity at −1.
Claim. For every $4\times 4$ real matrix $H$ and every integer-valued displacement $D:\{0,1,2,3\}\to\mathbb{Z}$, the quadratic edge strain satisfies $\mathrm{strain}(-H,D)=-\mathrm{strain}(H,D)$, where $\mathrm{strain}(H,D)=\sum_{i,j}H_{ij}D_i D_j$.
background
The ambient module treats the TT directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field sector. Edge strain is the quadratic form that pairs a metric perturbation matrix with an integer edge displacement: $\sum_{i,j} H_{ij} D_i D_j$. Here Mat4 is the 4D continuum preflight matrix type used throughout the Regge/Bloch analysis.
Sibling lemmas already record that strain is additive in $H$ and homogeneous under real scalar multiplication. The present statement is the sign-flip case of that homogeneity. A related but distinct lemma in MetricEdgeImage4D shows strain is even under $D\mapsto -D$; the two together control orientation and sign bookkeeping on patch edges.
The module honesty clause restricts all of this to the Euclidean weak-field TT continuum face: not a sourced field equation, not Ricci/null focusing, and not GAP1 closure.
proof idea
One-line wrapper. Instantiate the sibling scalar-homogeneity lemma edgeStrain_smul at the scalar $-1$, then simplify with the identity $(-1)\cdot H=-H$ (neg_one_smul). No unfolding of the double sum is required.
why it matters
Feeds the immediate sibling edgeStrain_sub, which rewrites strain of $H-K$ as a difference of strains and opens the cross-term / genuine bilinearization section of the first-variation development. Downstream, MetricEdgeImage4D uses the companion orientation-evenness fact (and related strain current symmetry) when assembling antisymmetric edge bookkeeping.
In the Recognition gravity stack this is pure linear-algebra scaffolding for the closed midpoint Bloch continuum face, not a physical law. It supports the transport of the torus-normalized continuum face via the banked S_RS_converges_EH_4d_closed Tendsto on $H\pm K$ plus polarization. It does not touch T5–T8 forcing, the RCL, or the alpha band; the missing future object remains a Recognition-derived Freudenthal exact-$J$ metric refinement that would identify sourced response with this midpoint variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.