IsLorentzTransverse
plain-language theorem explainer
Lorentz transversality for a covariant 4×4 matrix against a wave covector: each row of H, contracted with the raised covector m^j under signature (−,+,+,+), vanishes. Gravity and GR analysts cite it when building algebraic TT conditions on Minkowski space. It is a one-line Prop definition, not a proved statement.
Claim. A real $4\times 4$ matrix $H$ is Lorentz-transverse to a covector $m\in\mathbb{R}^4$ when $\sum_j H_{ij}\,m^j=0$ for every row index $i$, with index raising $m^0=-m_0$ and $m^i=m_i$ (spatial), i.e. $-(H_{i0})m_0+H_{i1}m_1+H_{i2}m_2+H_{i3}m_3=0$.
background
This module is the Lorentzian algebraic layer of the QG campaign item edge_tt_decomposition (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; raising negates the time component.
The Minkowski pairing is $\langle a,b\rangle=-(a_0)(b_0)+\sum_{k=1}^3 a_k b_k$, equal to $\sum_j a_j(\mathrm{raise},b)j$. Metric-trace of a covariant matrix is $\eta^{ij}H{ij}=-(H_{00})+H_{11}+H_{22}+H_{33}$. Lorentz transversality is the row-wise contraction of $H$ against the raised wave covector, exactly as written in the module conventions.
Mat4 is simply $\mathrm{Matrix}(\mathrm{Fin},4)(\mathrm{Fin},4),\mathbb{R}$. Non-null projectors use $P_{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$; null projectors use an auxiliary null partner $\ell$ with $m\cdot\ell\neq 0$.
proof idea
Pure definition: the predicate is the universal quantification over row indices $i:\mathrm{Fin},4$ of the Minkowski contraction of row $i$ of $H$ with raised $m$. No tactics, no lemmas. Downstream code rewrites it through the equivalent load form (lorentzLoad H m i = 0) when convenient.
why it matters
This is the transversality leg of algebraic Lorentz TT. The sibling predicate packages symmetry, Minkowski-tracelessness, and this condition into the full TT type used throughout the file.
It is the target property in gauge-correction lemmas (gauge-corrected matrices are transverse for non-null $m$), in the null PHP and null TT projectors (transverse to $m$ or to the auxiliary null $\ell$), and in the residual identity exists_nullLorentzTTDecomposition that closes the null algebraic edge-TT decomposition. It also underwrites the negative control that the Euclidean projector fails Lorentz transversality on a null axis.
Within Recognition Science this is linear-algebra scaffolding for the ledger name edge_tt_decomposition, not a physical polarization normalization and not a bridge to $S_{\mathrm{RS}}\to\mathrm{EH}$. It sits downstream of the $D=3$ / eight-tick geometric forcing only insofar as the ambient spacetime dimension is fixed to four.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.