edgeStrain_sub
plain-language theorem explainer
Edge strain is linear under matrix subtraction: the strain of H−K along a discrete edge direction equals the difference of the two strains. Anyone assembling the first variation or polarization identity for the 4D midpoint Bloch symbol in the Euclidean weak-field TT sector will cite this. The proof is a three-rewrite chain through additivity and oddness.
Claim. For $4\times 4$ real matrices $H,K$ and any integer edge-direction label $D:\mathrm{Fin}\,4\to\mathbb{Z}$, the edge strain satisfies $\mathrm{strain}(H-K,D)=\mathrm{strain}(H,D)-\mathrm{strain}(K,D)$.
background
The ambient module derives the directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field transverse-traceless sector, then transports the torus-normalized continuum face via the banked continuum limit on $H+K$ and $H-K$ plus polarization. Honesty constraints in the module doc restrict all theorems here to that sector: not a source equation, not Ricci/null focusing, and not GAP1 closure.
Mat4 is the local abbreviation for the $4\times 4$ matrix type used by the Regge 4D continuum preflight. Edge strain (imported from MetricEdgeImage4D) assigns to a metric perturbation matrix and a discrete edge direction $D$ the scalar strain felt along that edge image. Sibling lemmas already record additivity, scalar homogeneity, and oddness of this map in the matrix slot.
The parameters named $H$, $K$, and $D$ in the signature are ordinary matrix and direction arguments; they are not the global RS cost $H$, bridge ratio $K$, or spatial dimension $D=3$.
proof idea
One short rewrite chain. Expand subtraction as addition of the negative, apply the already-proved additivity lemma for edge strain, apply the already-proved oddness lemma (edgeStrain_neg), then fold the resulting sum-of-negative back into a subtraction. No case splits and no analytic estimates.
why it matters
Linearity under subtraction is the missing half of the algebraic toolkit (with additivity, homogeneity, and oddness) needed to polarize products of edge strains. The next section of the module introduces the coupling-weight cross term as that polarization and builds the exact midpoint Bloch first variation from it.
In the Recognition gravity program this sits inside the Euclidean weak-field TT analysis that prepares a continuum face for later comparison with Einstein–Hilbert structure via S_RS_converges_EH_4d_closed. It does not itself close the sourced response or the Lorentzian null-dyad transport; the module doc names the missing future object as a Recognition-derived Freudenthal exact-$J$ metric refinement. No downstream consumers are wired yet in the dependency graph, so the lemma is presently infrastructure for the in-module first-variation assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.