minkowskiTrace_sub
plain-language theorem explainer
The Minkowski metric trace is linear under matrix subtraction on real 4×4 matrices: tr_η(A−B)=tr_η(A)−tr_η(B). Anyone proving that transverse or null projectors (and the TT projections built from them) are Lorentz-traceless cites this identity. The proof unfolds the four-term definition and finishes by ring arithmetic on the diagonal entries.
Claim. For any real $4\times 4$ matrices $A,B$, the Minkowski metric trace satisfies $\operatorname{tr}_\eta(A-B)=\operatorname{tr}_\eta(A)-\operatorname{tr}_\eta(B)$, where $\operatorname{tr}_\eta(H)=-(H_{00})+H_{11}+H_{22}+H_{33}$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless splitting of symmetric real $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.
The metric trace of a covariant matrix is the contraction $\eta^{ij}H_{ij}$, written explicitly as $-(H,0,0)+H,1,1+H,2,2+H,3,3$. Lorentz transversality contracts the second index of $H$ against the raised wave covector. Non-null and null projectors are built from outer products against that covector (and an auxiliary null partner in the null case).
Mat4 is simply Matrix (Fin 4) (Fin 4) ℝ. The present lemma is the subtraction half of linearity for that four-term functional; sibling lemmas handle scalar multiples and the metric itself.
proof idea
Term-mode proof in three steps. Unfold the definition of the Minkowski trace to the explicit combination $-(H00)+H11+H22+H33$. Simplify componentwise subtraction via sub_apply, so each diagonal entry of $A-B$ becomes a difference of reals. Close with ring, which cancels the four pairs of terms into $\operatorname{tr}\eta A-\operatorname{tr}\eta B$. No external lemmas beyond the definition and matrix subtraction.
why it matters
Linearity under subtraction is the algebraic hinge for every tracelessness claim in the Lorentzian TT layer. Downstream, minkowskiTrace_transverseProjector rewrites the non-null projector as $\eta$ minus a scaled outer square and obtains trace $3$; nullProjector_minkowskiTrace does the same for the null projector and obtains trace $2$. Those identities feed ttProject_traceless and nullTTProject_traceless, which assert that the residual-trace-corrected TT projections are Lorentz-traceless (IsLorentzTraceless).
In the Recognition Science gravity stack this sits inside the ledger-closing name edge_tt_decomposition: pure linear algebra that prepares TT modes for later continuum matching, without yet decomposing Regge edge perturbations or proving Einstein–Hilbert recovery. It is the Minkowski counterpart of the Euclidean TT algebraic layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.