ttProject
plain-language theorem explainer
Algebraic transverse-traceless projection of a real 4×4 matrix against a Minkowski wave covector: strip the gauge piece, then subtract the residual metric-trace times the transverse projector. Gravity and QG ledger work cites it as the explicit TT component in the Lorentzian edge decomposition. The body is a one-line composition of three sibling operators.
Claim. For a wave covector $m \in \mathbb{R}^4$ and a matrix $H \in M_4(\mathbb{R})$, the TT projection is $\mathrm{TT}(m,H) := H^{\mathrm{gc}} - \beta\, P$, where $H^{\mathrm{gc}}$ is $H$ after subtracting its pure-gauge part along $m$, $\beta$ is the residual Minkowski trace of $H^{\mathrm{gc}}$ (normalized by the transverse dimension), and $P$ is the transverse projector built from $m$ (non-null or null form).
background
This module is the Lorentzian algebraic layer of the QG campaign name edge_tt_decomposition (Wave 4 / W4-1): TT decomposition of symmetric $4\times 4$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, signature $(-+++)$, including the null case. Matrices are Mat4 $= M_4(\mathbb{R})$. Covectors are lowered; raising negates the time component. Lorentz transversality contracts the second index of $H$ against the raised wave covector; the metric-trace is $\eta^{ij}H_{ij}$.
The Euclidean sibling defines the same three building blocks: gauge correction $H - \mathrm{gaugePart}(m,v)$, residual trace of the gauge-corrected matrix over the transverse directions, and the transverse projector $P$ (non-null: $\eta - mm^T/(m\cdot m)$; null: involving an auxiliary null $l$ with $m\cdot l \neq 0$). The Lorentzian file reimplements those operators with Minkowski pairing and trace, then assembles the same projection formula.
Upstream cost-algebra $H$ names in the dependency graph are unrelated parameter collisions; here $H$ is always the matrix being projected.
proof idea
Pure definition, not a theorem. The body is the single term
gaugeCorrected m H - residualTrace m H • transverseProjector m:
first remove the pure-gauge piece along $m$, then subtract the scalar residual Minkowski trace times the transverse projector so the result is both transverse and traceless (when the nondegeneracy hypotheses of the sibling lemmas hold). No tactics; identical shape to the Euclidean ttProject.
why it matters
Supplies the explicit TT summand for the algebraic edge TT decomposition in Lorentzian signature. Downstream Euclidean-layer theorems (exists_edgeTTDecomposition, exists_edgeTTDecomposition', ttProject_isTT, decoy checks that projection restores transversality) use the same pattern; the Lorentzian file is the specialization that also covers null wave covectors needed for gravitational-wave polarizations.
In the Recognition Science gravity stack this is linear-algebra scaffolding toward closing the ledger name edge_tt_decomposition. Module tier tags stress it does not yet decompose Regge EDGE perturbations on a 4D lattice, does not prove $S_{RS}$ converges to Einstein–Hilbert in 4D, and attaches no physical polarization normalization. It sits under the broader forcing/geometry program (D = 3 spatial, eight-tick structure upstream) but is strictly the algebraic projector step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.