lorentzLoad_one
plain-language theorem explainer
The Lorentz load of the 4×4 identity against any covector m equals the raised covector componentwise. Gravity analysts cite it when reducing transversality of projectors to a pure raise identity. The proof unfolds the load sum and collapses it by the single-term Finset identity for the Kronecker delta.
Claim. For every covector $m:\mathrm{Fin}\,4\to\mathbb{R}$ and every index $i$, the Lorentz load of the identity matrix satisfies $(\mathbf{1}\cdot m^\sharp)_i = (m^\sharp)_i$, where raising negates the time component under signature $(-+++)$.
background
This module is the Lorentzian algebraic TT layer for 4×4 real symmetric matrices against a Minkowski wave covector (signature $(-+++)$). Covectors are lowered by default; index raising is raise, with $(m^\sharp)_0=-m_0$ and $(m^\sharp)_i=m_i$ spatially. The Minkowski pairing is $\sum_j a_j(m^\sharp)_j$.
The Lorentz load of a matrix $H$ is the covector contraction $(H\cdot m^\sharp)i=\sum_j H{ij}(m^\sharp)_j$. Lorentz transversality is exactly vanishing of this load. The identity matrix is the unit of Mat4:=Matrix (Fin 4)(Fin 4) ℝ.
The surrounding campaign is Wave 4 edge TT decomposition: algebraic TT against null and non-null wave covectors, not yet a lattice Regge EDGE decomposition.
proof idea
Term-mode tactic proof. Unfold the load definition to the explicit sum $\sum_j \mathbf{1}_{ij}(m^\sharp)_j$. Simplify matrix-one entries to Kronecker deltas. Apply Finset.sum_eq_single at index $i$: the diagonal term is $(m^\sharp)i$; off-diagonal terms vanish by $\mathbf{1}{ij}=0$ when $j\neq i$; the membership side-condition is discharged by $i\in\mathrm{univ}$.
why it matters
Feeds euclideanProjector_not_lorentzTransverse_on_nullAxis, which shows that the Euclidean transverse projector on the null axis (where the Euclidean norm squared is 2) fails Lorentz transversality. That contrast is the algebraic reason the Lorentzian null projector must use an auxiliary null partner $l$ rather than the Euclidean formula.
In the QG full-theory campaign this sits in the Lorentzian linear-algebra layer of ledger name edge_tt_decomposition. It does not itself close continuum EH recovery or flip gap action recovery; it is a load identity used to police projector claims under Minkowski raising. Framework landmark contact is indirect: the ambient 4D setting is consistent with forced $D=3$ spatial plus time from the forcing chain, but this lemma is pure Minkowski linear algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.