axisTTPlus
plain-language theorem explainer
Unnormalized plus polarization on the axis wave vector: the 4×4 matrix diag(0,0,1,−1). It is one of the two explicit independent TT basis matrices used throughout the 4D edge TT algebraic layer. Downstream lemmas prove it is TT, nonzero, and linearly independent of the cross polarization; Regge closer work evaluates one-orbit m² symbols and moment contributions on it.
Claim. The unnormalized plus polarization is the real $4\times 4$ matrix whose only nonzero entries are $M_{22}=1$ and $M_{33}=-1$ (i.e. $\mathrm{diag}(0,0,1,-1)$ in the standard basis of $\mathbb{R}^4$).
background
This module is the algebraic layer of the QG campaign item edge_tt_decomposition: linear-algebra transverse-traceless (TT) structure for symmetric real $4\times 4$ matrices relative to a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Conventions lift the 3D closer chain (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
Mat4 is simply $\mathrm{Matrix}(\mathrm{Fin},4,\mathrm{Fin},4,\mathbb{R})$. A matrix is TT when it is symmetric, Euclidean-traceless, and transverse to the chosen wave covector. The module supplies an explicit independent TT pair on the axis wave vector with unnormalized integer entries; this definition is the plus member of that pair (the cross member has $H_{23}=H_{32}=1$).
proof idea
Pure definition by cases on the sixteen entries of a $4\times 4$ matrix: every entry is zero except position $(2,2)\mapsto 1$ and $(3,3)\mapsto -1$. No proof obligations.
why it matters
This constant is the standard plus generator for the two-polarization story in 4D Euclidean TT algebra. Immediate consumers prove it is TT (axisTTPlus_isTT), nonzero (axisTTPlus_ne_zero), and linearly independent of the cross polarization (axisTT_independent).
In Regge4DAlgebraicCloser it is the probe matrix for one-orbit m² symbols and full-moment orbit contributions: decoy identities show the single-orbit coefficient on this matrix is $-3$, not the continuum Einstein–Hilbert TT target $-1/4$; banked identities keep the ledger flags fullTTIsotropyClosed and gapActionRecovery false. The module doc is explicit that this algebraic layer does not yet decompose Regge EDGE perturbations, prove $S_{\mathrm{RS}}$ converges to EH in 4D, or flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.