nullAxisTTPlus
plain-language theorem explainer
Explicit unnormalized plus-polarization matrix with only nonzero entries H_{22}=1 and H_{33}=-1 on Fin 4. It is the concrete plus basis tensor for null-wave transverse-traceless modes in the Lorentzian edge TT algebraic layer. Anyone verifying the two-dimensional TT kernel along a fixed null axis cites this representative. The body is a pure index pattern match with no proof content.
Claim. Let $H_+$ be the $4\times 4$ real matrix with $H_+_{22}=1$, $H_+_{33}=-1$, and all other entries zero (indices in $\{0,1,2,3\}$). This is the unnormalized plus polarization for the null-axis TT sector.
background
The module is the Lorentzian algebraic layer of the edge TT decomposition campaign (Wave 4 / W4-1). It treats symmetric $4\times 4$ real matrices against a Minkowski wave covector on Fin 4, signature $(-!+,+,+)$, including the physically relevant null case.
Mat4 is simply Matrix (Fin 4) (Fin 4) ℝ. Lorentz TT means the matrix is symmetric, Minkowski-traceless (minkowskiTrace H = -H_{00}+H_{11}+H_{22}+H_{33}=0), and transverse to the raised wave covector. For a null wave one uses an auxiliary null partner to build the projector; the two free TT polarizations are conventionally plus and cross.
This definition supplies the plus representative aligned to the module's fixed null axis (spatial plane spanned by indices 2 and 3).
proof idea
Pure definition: each of the sixteen entries is fixed by a pattern match on the pair of Fin 4 indices. No lemmas, tactics, or obligations. Downstream theorems read the entries by congruence on matrix components.
why it matters
Gives the concrete plus generator used by three immediate parents: nullAxisTTPlus_isLorentzTT (plus mode is Lorentz TT for the module null wave), nullAxisTTPlus_ne_zero (nontrivial), and nullAxisTT_independent (linear independence from the cross mode). Together they pin the two-dimensional algebraic TT kernel along the null axis.
In the Recognition gravity stack this is the Lorentzian linear-algebra substrate of ledger name edge_tt_decomposition. It does not yet touch Regge edge perturbations, S_RS_converges_EH_4d, or gap-action recovery; it only closes the algebraic polarization basis needed before those geometric steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.