lorentzLoad_eq
plain-language theorem explainer
Expands the Lorentz load of a 4×4 matrix H against a covector m into the explicit Minkowski contraction with signature (−,+,+,+). Anyone proving Lorentz transversality or TT projection cites this to swap the summed definition for component form. The proof unfolds index raising and evaluates the four-term Fin sum.
Claim. For any real $4\times 4$ matrix $H$ and covector $m\in\mathbb{R}^4$, the Lorentz load at index $i$ equals $-(H_{i0})m_0 + H_{i1}m_1 + H_{i2}m_2 + H_{i3}m_3$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless decomposition of symmetric $4\times 4$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the null case. Signature is $(-!,+,+,+)$; covectors are lowered by default.
Index raising negates the time component: $(\mathrm{raise},v)0=-v_0$ and $(\mathrm{raise},v)i=v_i$ for spatial $i$. The Lorentz load is the matrix-vector product of $H$ against the raised covector, $(\mathrm{lorentzLoad},H,m)i=\sum_j H{ij}(\mathrm{raise},m)j$. Lorentz transversality is the statement that this load vanishes for every $i$, which the module doc writes componentwise as $-(H{i0})m_0+H{i1}m_1+H{i2}m_2+H_{i3}m_3=0$.
The load is the bridge between the summed definition used in projectors and the expanded form used in transversality predicates.
proof idea
One-line unfold-and-simp proof. Unfold lorentzLoad and raise, then apply Fin.sum_univ_four to expand $\sum_{j:\mathrm{Fin},4} H_{ij}(\mathrm{raise},m)j$. The $j=0$ term contributes $H{i0}(-m_0)$; the three spatial terms contribute $H_{ij}m_j$. No external lemmas beyond the Fin sum identity.
why it matters
Canonical expansion used throughout the Lorentz TT layer. Downstream, IsLorentzTransverse_iff_lorentzLoad equates the predicate to vanishing load via this identity in both directions. Gauge correction transversality (gaugeCorrected_transverse), metric load (lorentzLoad_eta), null PHP transversality in both legs (nullPhp_transverse_m, nullPhp_transverse_l), and null/non-null TT projectors (nullTTProject_transverse_*, ttProject_transverse) all rewrite through it before simplifying.
It sits inside the ledger name edge_tt_decomposition as pure Lorentzian linear algebra: no Regge edge perturbations, no $S_{\mathrm{RS}}\to\mathrm{EH}$ convergence, no polarization normalization. Closes the notational gap between the raised-index definition and the component form stated in the module conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.