loadNormSq
plain-language theorem explainer
Squared Euclidean norm of the matrix–vector product of a real 4×4 matrix H with a real 4-wave k: sum_m (sum_n H_mn k_n)^2. It is the load term in the closed-form midpoint Bloch m² expression. Gravity analysts cite it when reducing the 1208-coupling m² sum and when proving that transverse-traceless modes kill the load contribution. The body is a direct double sum, not a derived identity.
Claim. For a real $4\times 4$ matrix $H$ and a real $4$-vector $k$, define $\mathrm{loadNormSq}(H,k)=\sum_{m=0}^{3}\bigl(\sum_{n=0}^{3} H_{mn} k_n\bigr)^2$, i.e. the squared Euclidean norm of the ordinary matrix–vector product $Hk$.
background
This module closes the exact midpoint Bloch $m^2$ TT identity in 4D Regge analysis (script-backed kernel certs). The ambient objects are Mat4 (real $4\times 4$ matrices) and Wave4 (real maps on Fin 4), the discrete Hessian and Bloch wavevector slots for the midpoint expansion.
Sibling norms on the same types include the Frobenius square of $H$, the Euclidean square of $k$, the quadratic form $k^\top H k$, and the Euclidean trace. The closed-form $m^2$ expression assembles those pieces with rational coefficients; the load term is the one that measures how hard $H$ pushes on $k$.
The name collision with the RS cost reparametrization $H(x)=J(x)+1$ is accidental: here $H$ is only the matrix argument.
proof idea
Pure definition. Expand the squared Euclidean norm of $Hk$ as an outer sum over the four output components, each the square of an inner sum $\sum_n H_{mn}k_n$. No lemmas, no tactics.
why it matters
Feeds the closed-form midpoint Bloch $m^2$ polynomial: closedForm is $-\tfrac18|H|_F^2|k|^2 + \tfrac14,\mathrm{loadNormSq}(H,k)$ plus a trace–quadratic remainder. Downstream, biquad_closedCoeff_eq_closedForm unfolds this load term when matching the closed-coefficient bi-quadratic to that closed form for every $H$, not only symmetric ones.
Under the transverse-traceless hypothesis IsTT k H, closedForm_eq_neg_eighth_of_TT proves the load vanishes, so the identity collapses to $-\tfrac18|H|_F^2|k|^2$. The pure-gauge vanishing theorem closedForm_gaugePart_eq_zero likewise unfolds the load on gauge pairs. Together these steps discharge the exact midpoint $m^2$ TT identity that the module is written to close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.