ttProject_isLorentzTT
plain-language theorem explainer
For any symmetric 4×4 real matrix H and non-null Minkowski wave covector m, the algebraic TT projector of H is Lorentz-TT: symmetric, Minkowski-traceless, and Lorentz-transverse to m. Gravity analysts cite it when assembling the non-null Lorentzian edge TT decomposition. The proof is a three-field constructor packaging the symmetry, tracelessness, and transversality lemmas for the projector.
Claim. Let $H$ be a symmetric $4\times 4$ real matrix and let $m\in\mathbb{R}^4$ satisfy $m\cdot_{\eta} m\neq 0$ under the Minkowski pairing of signature $(-+++)$. Then the algebraic TT projection of $H$ against $m$ is Lorentz-TT: it is symmetric, has vanishing Minkowski trace, and is Lorentz-transverse to $m$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition (Wave 4 / W4-1). It specializes the Euclidean TT layer of EdgeTTDecomposition4D to signature $(-+++)$ on Fin 4, with covectors lowered by default. Index raising negates the time component; the Minkowski pairing is $m\cdot_{\eta}n=-(m_0)(n_0)+\sum_{i=1}^3 m_i n_i$, and the metric-trace of a covariant matrix is $\eta^{ij}H_{ij}=-(H_{00})+H_{11}+H_{22}+H_{33}$.
Lorentz transversality contracts the second index of $H$ against the raised wave covector. In the non-null regime $m\cdot_{\eta}m\neq 0$, the transverse projector is $P_{ij}=\eta_{ij}-m_i m_j/(m\cdot m)$. Algebraic Lorentz TT means the conjunction of symmetry, Minkowski-tracelessness, and Lorentz transversality.
The projector ttProject is imported from the Euclidean sibling: it subtracts a gauge correction and a residual-trace multiple of the transverse projector. The three component lemmas (symmetry, tracelessness, transversality of the image) are the immediate upstream facts used here.
proof idea
Term-mode constructor for the three-conjunct definition of Lorentz TT. The proof is the triple
⟨ttProject_symmetric, ttProject_traceless, ttProject_transverse⟩
applied at $(m,H)$ under the standing hypotheses that $H$ is symmetric and $m\cdot_{\eta}m\neq 0$. No further algebraic work occurs at this site: each conjunct is discharged by the corresponding named lemma already proved for the projector.
why it matters
This is the certification step that the non-null TT projector lands in the Lorentz-TT subspace. The sole downstream consumer is exists_lorentzTTDecomposition, the named non-null Lorentzian algebraic edge TT decomposition: every symmetric $4\times 4$ matrix against a non-null Minkowski wave covector splits as Lorentz-TT plus gauge plus transverse-trace part, with the TT summand identified as ttProject m H.
In the campaign taxonomy this is pure linear algebra for the ledger closing name edge_tt_decomposition. It does not touch continuum limits, Regge edge perturbations, or the Einstein-Hilbert recovery gap. Within Recognition Science gravity analysis it supplies the algebraic TT piece needed before any physical polarization or eight-tick continuum identification is attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.