edgeLoad_smul
plain-language theorem explainer
Homogeneity of the 4D quadratic edge load: scaling the matrix by a real constant scales the load by the same constant. Cited by anyone transporting TT/gauge decompositions or plane-wave edge perturbations through scalar multiples. Proof unfolds the double-sum definition and factors the scalar out of both finite sums.
Claim. For any $c \in \mathbb{R}$, any $4\times 4$ real matrix $H$, and any $d \in \mathbb{R}^4$, the quadratic edge loading satisfies $\sum_{i,j} (c H)_{ij} d_i d_j = c \sum_{i,j} H_{ij} d_i d_j$.
background
This module attaches the Euclidean $4\times 4$ TT/gauge/transverse-trace split to plane-wave edge loadings on axis edges of the 4-torus (QG Wave 4, lane W4-1). The loading convention matches the 3D chain: a quadratic form $D^T H D$.
The local definition is edgeLoad: for a matrix $H$ and direction $d$, $\mathrm{edgeLoad}(H,d)=\sum_{i,j} H_{ij} d_i d_j$. Axis edges use $d$ equal to a standard basis vector, so the load collapses to the diagonal entry $H_{aa}$. Sibling lemmas already record additivity; this lemma is the matching scalar-homogeneity step.
(The import graph also touches cost-algebra $H$, but that is a name collision with the matrix parameter; the proof uses only the quadratic-form definition.)
proof idea
Tactic proof. Unfold the double-sum definition of the edge load, then simplify scalar action on matrix entries ($c\bullet H$ acts entrywise by multiplication). A short calc reassociates $c\cdot H_{ij}\cdot d_i\cdot d_j$ to $c\cdot(H_{ij} d_i d_j)$ by ring inside nested Finset.sum_congr, then pulls $c$ out of both sums with Finset.mul_sum.
why it matters
Linearity of edge load is the algebraic hinge that lets the TT/gauge/residual split pass to edge observables: load of a sum equals sum of loads, and load of a scalar multiple scales. This lemma is the scalar half.
Downstream it discharges edgeLoad_neg (via $c=-1$), planeWaveAxisEdgePert_smul (midpoint cosine times the load), and classCoeff_smul in the 4D Regge edge stencil (class coefficients are edge loads on the 15 edge classes). Together with additivity it underwrites the module claim that edge load of $H$ equals the sum of loads of the TT, gauge, and residual parts.
Scope stays inside the plane-wave attachment layer: it does not close full edge_tt_decomposition, continuum Einstein-Hilbert recovery, or gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.