load_smul
plain-language theorem explainer
Real scalar homogeneity of the 4D matrix-vector load: loading cH against a covector equals c times loading H. Cited throughout the algebraic TT projector calculus whenever scalars leave a load. Proof unfolds the finite sum and applies Finset.mul_sum after simplifying scalar action on matrix entries.
Claim. For every real scalar $c$, every $4\times 4$ real matrix $H$, every map $m:\{0,1,2,3\}\to\mathbb{R}$, and every index $i$, the load of the scaled matrix equals the scaled load: $\sum_{j}(cH)_{ij}m_j = c\sum_{j}H_{ij}m_j$.
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: Euclidean transverse-traceless structure for symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer (symmetry, Euclidean trace, Euclidean transversality) without a Frobenius pin; Minkowski specialization is deferred.
Mat4 is the abbreviation for $\mathrm{Matrix},(\mathrm{Fin},4),(\mathrm{Fin},4),\mathbb{R}$. The load of a matrix $H$ against a covector $m$ is the ordinary matrix-vector product, componentwise $\mathrm{load}(H,m)i=\sum_j H{ij}m_j$. Transversality of a symmetric matrix is the statement that this load vanishes identically against the wave covector.
The theorem is pure finite-dimensional linear algebra over $\mathbb{R}$; the CostAlgebra/FunctionalEquation $H$ symbols appearing in the dependency graph are unrelated name collisions, not inputs here.
proof idea
Unfold the load definition to a finite sum over $\mathrm{Fin},4$. Simplify the scalar action on matrix entries via smul_apply and smul_eq_mul, then reassociate products with mul_assoc. Finish by invoking the standard identity that a constant factors out of a Finset sum (Finset.mul_sum), taken symmetrically so the scalar sits on the left as in the goal.
why it matters
Scalar pull-out is the elementary linearity step needed to evaluate loads of projectors built from outer products and scaled identity pieces. Downstream, load_transverseProjector rewrites the load of the transverse projector through load_sub, load_one, this lemma, and load_outerSq, then clears the nonzero momentum-squared denominator. The same identity appears inside ttProject_transverse, which shows the TT projection of an arbitrary matrix is transverse by reducing the load of the gauge-corrected piece to zero.
In the Recognition Gravity stack this sits in Wave 4 / lane W4-1: kernel-checked linear algebra only. It does not close continuum Einstein-Hilbert recovery or flip gap_action_recovery; it supplies the bookkeeping that lets the algebraic TT pair on the axis wave vector be manipulated without leaving scalars trapped inside sums.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.