IsLorentzTT
plain-language theorem explainer
Algebraic Lorentz transverse-traceless (TT) condition on a real 4×4 matrix relative to a Minkowski wave covector: symmetry, vanishing Minkowski trace, and Lorentz transversality. Gravity and GR analysts cite it as the target class for edge TT projectors in the Lorentzian layer. It is a three-way conjunction of the sibling predicates, not a derived theorem.
Claim. A real $4\times 4$ matrix $H$ is Lorentz-TT with respect to a covector $m\in\mathbb{R}^4$ when $H$ is symmetric, its Minkowski trace vanishes ($\eta^{ij}H_{ij}=0$), and it is Lorentz-transverse to $m$ (each row of $H$ contracts to zero against the raised covector $m^\sharp$).
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition: 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; raising negates the time component.
The Minkowski pairing is $m\cdot n=-(m_0)(n_0)+\sum_{i=1}^3 m_i n_i$, and the metric-trace of a covariant matrix is $\mathrm{tr}\eta H=-(H{00})+H_{11}+H_{22}+H_{33}$. Lorentz transversality contracts the second index of $H$ against the raised wave covector: $\forall i,; H_{i\mu}m^\mu=0$.
Sibling predicates package the three pieces: matrix symmetry $H_{ij}=H_{ji}$, Minkowski-tracelessness, and the contraction condition above. Non-null and null projectors (with an auxiliary null partner $\ell$ when $m\cdot m=0$) are built later in the file.
proof idea
Pure definitional abbreviation: the predicate is the conjunction of the three sibling Props (symmetry of $H$, vanishing Minkowski trace, and Lorentz transversality of $H$ to $m$). No tactics, no lemmas, no computation.
why it matters
This is the target class for the Lorentzian algebraic edge TT decomposition. Downstream, exists_lorentzTTDecomposition and its primed form prove every symmetric matrix against a non-null wave covector splits as Lorentz-TT plus gauge plus transverse-trace residual, with the TT summand satisfying this predicate. The null analogue exists_nullLorentzTTDecomposition does the same with $m$-gauge, $\ell$-gauge, bilinear, and screen-trace pieces.
Projector lemmas (ttProject_isLorentzTT, nullTTProject_isLorentzTT) and explicit null-axis polarization checks (nullAxisTTPlus_isLorentzTT, nullAxisTTCross_isLorentzTT) discharge membership in this class. In the broader RS gravity stack this is linear-algebra scaffolding only: it does not yet touch Regge EDGE perturbations, $S_{\mathrm{RS}}\to EH$ convergence, or gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.