IsLorentzTraceless
plain-language theorem explainer
Defines Minkowski-tracelessness for a real 4×4 matrix: the metric contraction η^{ij} H_{ij} vanishes. Gravity and GR analysts cite it when stating algebraic TT conditions on symmetric tensors against a Minkowski background. The body is a one-line Prop alias of the metric-trace predicate.
Claim. A real $4\times 4$ matrix $H$ is Lorentz-traceless when its Minkowski metric trace vanishes: $\eta^{ij} H_{ij} = 0$, i.e. $-(H_{00}) + H_{11} + H_{22} + H_{33} = 0$ in signature $(-+++)$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless decomposition 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.
The metric trace of a covariant matrix is $\mathrm{minkowskiTrace},H = -(H,0,0)+H,1,1+H,2,2+H,3,3$, equal to $\eta^{ij} H_{ij}$. Matrices are plain Matrix (Fin 4) (Fin 4) ℝ. Index raising negates the time component, and the Minkowski pairing of covectors is $-(a_0)(b_0)+\sum_{i=1}^3 a_i b_i$.
Lorentz TT will later mean symmetric + Minkowski-traceless + Lorentz-transverse (contraction of the second index of $H$ against the raised wave covector). This definition isolates the middle leg of that conjunction.
proof idea
Definitional: the predicate is literally equality of the Minkowski metric trace to zero. No tactics, no lemmas. Downstream proofs unfold this name and reduce via minkowskiTrace_sub, minkowskiTrace_smul, and projector-trace identities.
why it matters
Feeds the composite algebraic TT predicate (symmetric ∧ Lorentz-traceless ∧ Lorentz-transverse), which is the target property for both non-null and null projectors in this file. Downstream, ttProject_traceless and nullTTProject_traceless prove the projected matrices satisfy this predicate; the explicit null-axis polarization matrices (nullAxisTTPlus, nullAxisTTCross) are checked against it by direct norm_num.
In the QG ledger this is pure linear algebra for edge_tt_decomposition. It does not itself recover Einstein–Hilbert action or close gap-action recovery; it only supplies the traceless half of the algebraic TT condition used when specializing the Euclidean TT layer to Minkowski signature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.