lorentzLoad_eta
plain-language theorem explainer
Loading the Minkowski metric against any covector m recovers m componentwise: (η · m^♯)_i = m_i. Gravity and TT-decomposition proofs cite this as the identity action of η under the Lorentz load. The proof expands the load formula, unfolds the diagonal metric, and checks the four index cases by simplification and ring normalization.
Claim. For every covector $m \in \mathbb{R}^4$ and every index $i \in \{0,1,2,3\}$, the Lorentz load of the Minkowski metric $\eta = \mathrm{diag}(-1,1,1,1)$ against $m$ equals $m$ itself: $(\eta \cdot m^{\sharp})_i = m_i$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless splitting of symmetric $4\times 4$ real 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$ spatially. The Lorentz load of a matrix $H$ against a covector $m$ is the contraction $(\mathrm{lorentzLoad},H,m)i = \sum_j H{ij}(\mathrm{raise},m)j$, equivalently $-(H{i0})m_0 + H{i1}m_1 + H{i2}m_2 + H_{i3}m_3$. The metric $\eta$ is the standard diagonal Minkowski matrix from the Clausius–Einstein bridge.
Upstream, lorentzLoad_eq expands the sum over $\mathrm{Fin},4$ into that explicit four-term formula, which is the algebraic handle used here.
proof idea
Term-mode proof in three steps. Rewrite the goal by lorentzLoad_eq, replacing the load by the explicit four-term contraction against $m$. Unfold minkowskiEta and minkowskiEta4 so the matrix entries become the diagonal pattern $(-1,1,1,1)$. Case-split on the four values of $i$ via fin_cases; each branch simplifies by the diagonal structure and finishes with ring_nf.
why it matters
Identity action of $\eta$ under Lorentz load is the base case for every projector-transversality lemma in this file. Downstream, lorentzLoad_transverseProjector uses it to show that the non-null projector $P_{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$ loads to zero against $m$. The null-projector lemmas lorentzLoad_nullProjector_m and lorentzLoad_nullProjector_l likewise rewrite through this identity when proving $P^{\mathrm{null}}\cdot m^{\sharp}=0$ and $P^{\mathrm{null}}\cdot l^{\sharp}=0$.
Within the Recognition gravity stack this is pure Lorentzian linear algebra supporting the ledger name edge_tt_decomposition. It does not itself recover Einstein–Hilbert dynamics or close gap-action recovery; it supplies the metric-load identity those later algebraic steps need when building TT projectors in $D=4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.