nullAxisTTPlus_ne_zero
plain-language theorem explainer
The unnormalized plus polarization on the null axis, the diagonal pattern (0,0,1,−1) in Mat4, is not the zero matrix. Anyone assembling a Lorentzian TT basis for null wave covectors cites this to keep the plus mode nontrivial. Proof is a direct entry extraction: the (2,2) component equals 1 under the definition.
Claim. Let $H^+$ be the $4\times 4$ real matrix with $H^+_{22}=1$, $H^+_{33}=-1$, and all other entries zero (the unnormalized plus polarization). Then $H^+ \neq 0$ in $\mathrm{Mat}_4(\mathbb{R})$.
background
This module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1): transverse-traceless splitting of symmetric $4\times 4$ real matrices against a Minkowski wave covector on $\mathrm{Fin},4$, including the physically relevant null case. Signature is $(-!,+,+,+)$; covectors are lowered by default; index raising negates the time component.
The plus polarization is the standard GW pattern $\mathrm{diag}(0,0,1,-1)$ (unnormalized), written entrywise as a Mat4. Lorentz TT means symmetric, Minkowski-traceless, and transverse to the raised wave covector. For null $m$ one also needs an auxiliary null $l$ with $m\cdot l\neq 0$ to build the projector. The module is pure linear algebra: it does not yet decompose Regge EDGE perturbations or recover the Einstein–Hilbert action.
proof idea
Assume for contradiction that the plus matrix equals the zero matrix. Apply congruence of the evaluation map $M\mapsto M_{22}$ to both sides. Unfolding the entrywise definition of the plus polarization forces $1=0$, which is absurd. No external lemmas are required beyond definitional simplification of the matrix entries.
why it matters
Inside the QG full-theory campaign this is a minimal sanity check on the null-axis TT basis: the plus mode must be a genuine nonzero tensor before one can claim a two-dimensional polarization space or project edge fluctuations onto it. The module doc binds the tier as THEOREM (kernel-checked, no sorry) and situates the file as the Lorentzian specialization of the Euclidean TT layer, under the ledger closing name edge_tt_decomposition.
No downstream consumers are wired yet (used_by is empty). The result does not flip gap_action_recovery, does not prove $S_{\mathrm{RS}}$ converges to EH in 4D, and attaches no physical polarization normalization. It simply keeps the algebraic scaffolding honest so later null-case projector identities can quote a nonzero plus generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.