edgeStrain_add
plain-language theorem explainer
Edge strain is additive in the metric perturbation: the quadratic form of H+K along integer edge increments equals the sum of the forms for H and for K. Anyone expanding midpoint Bloch coupling weights along a line H+tK cites this. The proof unfolds the double sum and splits it by matrix addition plus Finset sum distributivity.
Claim. For $4\times 4$ matrices $H,K$ and any integer edge increment $D:\mathrm{Fin}\,4\to\mathbb{Z}$, the edge strain satisfies $\mathrm{edgeStrain}(H+K,D)=\mathrm{edgeStrain}(H,D)+\mathrm{edgeStrain}(K,D)$, where $\mathrm{edgeStrain}(M,D)=\sum_{i,j} M_{ij}\,D_i\,D_j$.
background
This module works in the Euclidean weak-field transverse-traceless (TT) sector of the closed 4D midpoint Bloch continuum face. The goal is a genuine directional first variation of exactMidpointBlochSymbol, later transported by the banked continuum convergence on $H+K$ and $H-K$ plus polarization.
Mat4 is the 4×4 matrix type used for continuum metric perturbations. Edge strain of a matrix $M$ along an integer increment $D:\mathrm{Fin},4\to\mathbb{Z}$ is the quadratic form $\sum_{i,j} M_{ij} D_i D_j$ (the continuum image of edge stretch under the metric perturbation). That form is the elementary building block of coupling weights on the torus face.
The local honesty bound is strict: results here are TT Euclidean first-variation statements only, not source equations, not Ricci/null focusing, and not GAP1 closure.
proof idea
Unfold the definition of edge strain to the double sum over $\mathrm{Fin},4\times\mathrm{Fin},4$. The first calc step replaces $(H+K){ij}$ by $H{ij}+K_{ij}$ via Matrix.add_apply and splits the product by ring, under Finset.sum_congr. The second step applies Finset.sum_add_distrib on the inner $j$-sum for each fixed $i$. The third step applies Finset.sum_add_distrib on the outer $i$-sum, yielding the sum of the two separate double sums that define edgeStrain H D and edgeStrain K D.
why it matters
Additivity is the first half of the bilinearization toolkit for edge strain. Downstream, edgeStrain_sub is the one-line companion (via $H-K=H+(-K)$ and the negation lemma), and couplingWeight_line expands the coupling weight along the affine line $H+t\bullet K$ into constant, cross, and quadratic pieces. That line expansion is exactly the directional first variation of the closed midpoint Bloch symbol in the TT sector.
In the Recognition gravity stack this is scaffolding for the continuum face of the RS action, not a claim about Einstein equations or null focusing. The module doc is explicit: the missing future object is a Recognition-derived Freudenthal exact-$J$ metric refinement identifying sourced response with this midpoint variation, then Lorentzian null-dyad transport. Until that bridge exists, cite only as TT Euclidean first-variation algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.