nullAxisTT_independent
plain-language theorem explainer
The two unnormalized null-axis TT polarizations (plus: spatial diag(1,−1); cross: H_{23}=H_{32}=1) are linearly independent over ℝ as 4×4 matrices. Gravity analysts counting Lorentzian TT degrees of freedom on the null cone, or closing the edge TT decomposition, cite this. Proof reads the (2,2) and (2,3) entries of the linear combination and simplifies.
Claim. Let $H_{+}$ be the $4\times 4$ plus polarization with only nonzero entries $H_{+}_{22}=1$, $H_{+}_{33}=-1$, and $H_{\times}$ the cross polarization with only nonzero entries $H_{\times}_{23}=H_{\times}_{32}=1$. If $a,b\in\mathbb{R}$ satisfy $a\,H_{+}+b\,H_{\times}=0$ as matrices, then $a=0$ and $b=0$.
background
This module is the Lorentzian algebraic layer of the QG campaign item edge_tt_decomposition: transverse-traceless decomposition of symmetric real $4\times 4$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, signature $(-+++)$, including the physically relevant null case. Covectors are lowered by default; index 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}$.
On the null cone one works with an auxiliary null covector $\ell$ with $m\cdot\ell\neq 0$ and the projector $P_{ij}=\eta_{ij}-(m_i\ell_j+\ell_i m_j)/(m\cdot\ell)$. The two standard gravitational-wave polarizations along a fixed null axis are encoded here as unnormalized matrices: plus is spatial $\mathrm{diag}(1,-1)$, cross has $H_{23}=H_{32}=1$, all other entries zero. Linear independence of these two matrices is the elementary algebraic fact needed before any span or dimension count of the null TT space.
proof idea
Term-style tactic proof by component extraction. From the matrix equation $a,H_{+}+b,H_{\times}=0$, apply congruence on the $(2,2)$ entry and on the $(2,3)$ entry. Unfold the two polarization definitions and scalar multiplication: the $(2,2)$ entry of the combination is exactly $a$, and the $(2,3)$ entry is exactly $b$. The two simplified equalities are $a=0$ and $b=0$, returned as a conjunction. No external lemmas beyond definitional unfolding are required.
why it matters
Sits in the Lorentzian specialization of the Euclidean TT layer, Wave 4 / lane W4-1 of the full-theory gravity campaign. The module's binding tier is THEOREM (kernel-checked, no sorry): this independence fact is the first algebraic check that the two physical null polarizations are distinct basis directions before any projector identity or kernel-dimension argument. Downstream use sites are not yet wired in this graph snapshot (used_by empty), but the natural consumers are null-cone TT span/dimension lemmas and any later bridge from algebraic TT matrices toward Regge edge modes.
Framework role is local linear algebra for gravity, not a forcing-chain landmark (T0–T8). The module doc is explicit that this layer does not decompose Regge EDGE perturbations, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and attaches no physical polarization normalization. It closes a pure algebraic prerequisite inside the ledger name edge_tt_decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.