lorentzLoad
plain-language theorem explainer
The Lorentz load of a real 4×4 matrix H against a covector m is the residual vector (H · m♯)_i obtained by contracting each row of H with the raised wave covector. Anyone proving Lorentz transversality or building the gauge correction in the 4D edge TT layer cites it as the quantity that vanishes iff H is Lorentz-transverse to m. It is a one-line definition: the ordinary matrix-vector product against the (−,+,+,+) raise of m.
Claim. For a real $4\times 4$ matrix $H$ and a covector $m\in\mathbb{R}^4$, define the Lorentz load by $(H\cdot m^\sharp)_i := \sum_{j=0}^{3} H_{ij}\,(m^\sharp)^j$, where index raising uses the signature $(-\!,+,+,+)$: $(m^\sharp)^0 = -m_0$ and $(m^\sharp)^k = m_k$ for spatial $k$.
background
This module is the Lorentzian algebraic layer of the QG edge TT decomposition campaign (Wave 4 / W4-1). It specializes the Euclidean 4×4 TT layer to symmetric matrices against a Minkowski wave covector on Fin 4, including the null case. Signature is (−,+,+,+); covectors are lowered by default.
Index raising negates only the time component: (raise v)_0 = −v_0 and (raise v)_i = v_i spatially. The Minkowski pairing of two covectors is then ∑_j a_j (raise b)j, and the metric-trace of a covariant matrix is η^{ij} H{ij}. Lorentz transversality is defined by contracting the second index of H against the raised wave covector, which is exactly the componentwise vanishing of the load defined here.
Mat4 is the abbreviation for Matrix (Fin 4) (Fin 4) ℝ. The load is the primitive residual used by every subsequent projector, gauge vector, and TT predicate in the file.
proof idea
Pure definition, no proof obligations. Body is the pointwise sum ∑_j H i j · (raise m) j. The companion lemma lorentzLoad_eq expands raise and Fin.sum_univ_four to the explicit form −(H i 0) m 0 + H i 1 m 1 + H i 2 m 2 + H i 3 m 3, which is the form used in almost every downstream rewrite.
why it matters
This residual is the working definition of Lorentz transversality: IsLorentzTransverse_iff_lorentzLoad states that H is Lorentz-transverse to m iff every component of the load vanishes. Downstream, gaugeVector builds the non-null gauge correction from the load; lorentzLoad_gaugePart and lorentzLoad_gaugePart_gaugeVector compute how the gauge piece cancels it; lorentzLoad_eta shows the metric itself loads to m; lorentzLoad_nullProjector_l handles the null-projector case.
It also powers the contrast theorem euclideanProjector_not_lorentzTransverse_on_nullAxis, which shows the Euclidean projector fails Lorentz transversality on a null axis. Within the Recognition gravity stack this is pure linear algebra for the ledger name edge_tt_decomposition: it does not yet touch Regge edge perturbations, S_RS → EH convergence, or gap_action_recovery, but every Lorentzian TT identity in the file routes through this contraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.