edgeStrain_smul
plain-language theorem explainer
Edge strain is homogeneous of degree one: scaling a 4×4 metric perturbation by a real constant scales the strain along any integer lattice direction by the same constant. Anyone expanding midpoint Bloch coupling weights along the line H + t K cites this. The proof unfolds the double-sum definition and factors the scalar through Finset.mul_sum.
Claim. For every real scalar $c$, every $4\times 4$ real matrix $H$, and every integer direction $D:\{0,1,2,3\}\to\mathbb{Z}$, the edge strain of $cH$ along $D$ equals $c$ times the edge strain of $H$ along $D$.
background
The module works in the Euclidean weak-field transverse-traceless sector of the closed 4D midpoint Bloch continuum face. It prepares the directional first variation of the exact midpoint Bloch symbol and transports that face via the banked continuum convergence on $H+K$ and $H-K$ plus polarization.
Edge strain is the quadratic form
$$\sum_{i,j=0}^{3} H_{ij},D_i,D_j$$
on a $4\times 4$ matrix $H$ and an integer edge direction $D$. The same formula appears in the Regge exact-flat Hessian Bloch symbol and in the metric-edge image layer; both treat it as the discrete strain current on patch edges. Here Mat4 is the continuum-preflight $4\times 4$ matrix type.
Homogeneity under scalar multiplication is the elementary algebraic step needed before one can expand coupling weights along affine lines in matrix space.
proof idea
Unfold the double-sum definition of edge strain. The first calc step rewrites each summand $(c\bullet H){ij} D_i D_j$ as $c\cdot(H{ij} D_i D_j)$ by Matrix.smul_apply, smul_eq_mul, and ring, under two nested Finset.sum_congr. The second step pulls the constant out of both sums via Finset.mul_sum (outer sum, then inner sum by congruence). No external lemmas beyond Mathlib sum algebra are required.
why it matters
This is a local linearity lemma inside the TT first-variation pipeline. Downstream, edgeStrain_neg is the one-line specialization at $c=-1$, and couplingWeight_line expands
$$W(H+tK)=W(H)+t,W_{\mathrm{cross}}(H,K)+t^2 W(K)$$
by feeding the same homogeneity into every edge contribution. That expansion is the algebraic engine of the directional first variation of the closed midpoint Bloch symbol.
In the broader Recognition gravity stack the lemma sits strictly inside the Euclidean weak-field TT continuum face. The module honesty block forbids reading it as a source equation, Ricci/null focusing, or GAP1 closure; those require a future Freudenthal exact-$J$ metric refinement and Lorentzian null-dyad transport. It does not touch the T0–T8 forcing chain or the RCL directly; it only clears scalar bookkeeping for the continuum face already banked by S_RS_converges_EH_4d_closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.