ttProject_symmetric
plain-language theorem explainer
The transverse-traceless projection of a symmetric 4×4 real matrix against a wave covector is again symmetric. Gravity and GR linearization work cites this when assembling the Lorentzian TT triple (symmetric, metric-traceless, transverse). The proof is a short componentwise rewrite through gauge-correction symmetry and transverse-projector symmetry.
Claim. Let $m\in\mathbb{R}^4$ be a covector and $H$ a symmetric $4\times 4$ real matrix. Then the transverse-traceless projection $\mathrm{ttProject}(m,H)$ is symmetric: $\mathrm{ttProject}(m,H)_{ij}=\mathrm{ttProject}(m,H)_{ji}$ for all indices $i,j\in\{0,1,2,3\}$.
background
This module is the Lorentzian algebraic layer of the QG campaign lane edge_tt_decomposition: TT decomposition of symmetric $4\times 4$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, signature $(-+++)$, including the null case. Matrices are Mat4 $:=$ $\mathrm{Matrix}(\mathrm{Fin},4,\mathrm{Fin},4,\mathbb{R})$. Symmetry means $H_{ij}=H_{ji}$.
The TT projector is built by first subtracting a gauge (longitudinal) correction, then applying a transverse projector $P$ (non-null: $P_{ij}=\eta_{ij}-m_im_j/(m\cdot m)$; null uses an auxiliary null $l$). Lorentz transversality contracts the second index of $H$ against the raised covector; the metric-trace is $\eta^{ij}H_{ij}$.
Upstream, the Euclidean sibling already proves that gauge correction and the transverse projector each preserve symmetry (gaugeCorrected_symmetric, transverseProjector_symmetric). Those facts transfer directly into the Lorentzian construction.
proof idea
Tactic proof, componentwise. Fix indices $i,j$. Unfold ttProject (difference of a scalar multiple of the transverse projector against the gauge-corrected matrix) and simplify matrix arithmetic (sub_apply, smul_apply). Rewrite the $(i,j)$ entry using gaugeCorrected_symmetric m H hH (gauge correction of a symmetric matrix stays symmetric) and transverseProjector_symmetric m (the transverse projector itself is symmetric). Equality of the swapped indices follows at once. No case split on null versus non-null is needed for symmetry alone.
why it matters
Symmetry is the first leg of the Lorentzian TT package. Downstream, ttProject_isLorentzTT packages this lemma with the traceless and transverse legs:
⟨ttProject_symmetric …, ttProject_traceless …, ttProject_transverse …⟩,
under the non-null hypothesis $m\cdot m\neq 0$. The Euclidean twin ttProject_isTT uses the same pattern.
In the Recognition Science gravity stack this is pure linear algebra supporting the ledger name edge_tt_decomposition (Wave 4 / W4-1). It does not yet touch Regge edge perturbations, Einstein-Hilbert recovery, or polarization normalizations; those sit further down the forcing and continuum-limit chain. Closing the algebraic TT layer is a prerequisite before continuum or lattice gravity claims can quote a well-typed TT projector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.