axisTTPlus_isTT
plain-language theorem explainer
The unnormalized plus polarization diag(0,0,1,−1) is algebraically transverse-traceless against the axis wave covector (1,0,0,0) on Fin 4. Gravity and Regge-normalization lemmas cite it as the canonical TT seed. The proof is a three-conjunct refine that discharges symmetry, Euclidean tracelessness, and transversality by exhaustive Fin cases and simp.
Claim. The matrix $H_+=\mathrm{diag}(0,0,1,-1)$ is algebraically TT with respect to the Euclidean wave covector $m=(1,0,0,0)$: $H_+$ is symmetric, has vanishing Euclidean trace $\sum_i H_{+ii}=0$, and is transverse ($m^i H_{+ij}=0$ for all $j$).
background
This module is the algebraic layer of the QG campaign lane edge_tt_decomposition: linear-algebra TT structure for symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. It lifts the 3D conventions (Euclidean trace, Euclidean transversality, symmetry) without a Frobenius pin; Minkowski/null specialization is deferred.
Algebraic TT means the conjunction of three props: symmetry of $H$, vanishing Euclidean trace $\sum_{i:F4} H_{ii}=0$, and transversality of $H$ to the wave covector $m$. The axis wave is the unit covector along the $0$-axis, $m=(1,0,0,0)$. The plus polarization is the unnormalized integer matrix with only nonzero entries $H_{22}=1$ and $H_{33}=-1$.
The broader decomposition theorem in the same file states that every symmetric $4\times 4$ matrix against nonzero $m$ splits as TT plus gauge plus transverse-trace residual, with the TT summand satisfying this same IsTT predicate.
proof idea
Term-mode proof via refine ⟨?_, ?_, ?_⟩ on the three conjuncts of algebraic TT.
- Symmetry: introduce indices $i,j$ and exhaust both by
fin_cases; each entry equality isrflagainst the explicit matrix definition. - Tracelessness: unfold the Euclidean-trace and traceless predicates together with the plus matrix;
simpwithFin.sum_univ_fourreduces the diagonal sum $0+0+1+(-1)$ to zero. - Transversality: introduce the free index and
fin_casesover it; each case simplifies using the plus matrix, the axis wave, and the four-term Fin sum, so the contraction $m^i H_{ij}$ vanishes componentwise.
why it matters
This is the concrete nonzero TT seed for the 4D edge-TT algebraic layer. Downstream, the continuum preflight normalizes it and re-proves TT; the edge stencil packages it with a nonzero finite TT quadratic as the seed for gauge non-invariance; the attachment module aliases it as both the decoy and the witness TT edge perturbation.
In the normalization-derived module it supplies the hypothesis that pins the Regge face constant: every $\rho\neq 1/2$ is refuted at this witness, and the midpoint Bloch value is shown nonzero (discrimination that agreement is not two zeros). Those steps sit inside the ledger closing name edge_tt_decomposition and feed the path toward continuum EH recovery, without themselves claiming lattice Regge decomposition or S_RS_converges_EH_4d.
Within Recognition gravity analysis this is the 4D lift of the 3D TT-polarization closer pattern: an explicit independent polarization on the axis wave, the first of the expected pair of 4D TT modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.