axisTTPolarizationPlus
plain-language theorem explainer
Explicit matrix for the plus transverse-traceless polarization along the coordinate axis: diag(0, 1/√2, −1/√2). Gravity analysts cite it as the non-vacuous witness for axis-direction TT Bloch-symbol and second-variation checks on the Freudenthal torus. The body is a pure entry table, no proof.
Claim. Define the axis $+$ polarization as the symmetric $3\times 3$ matrix $e^+_{ij}$ with $e^+_{11}=1/\sqrt{2}$, $e^+_{22}=-1/\sqrt{2}$, and all other entries zero (i.e. $\mathrm{diag}(0,1/\sqrt{2},-1/\sqrt{2})$).
background
This module is Stage 1 of the Regge TT continuum-symbol campaign: the true nonlinear 3D Regge action on a periodic Freudenthal torus, its flat point, and the TT Bloch symbol object built from plane-wave edge fields. Polarizations enter as constant symmetric tensors that modulate those plane waves.
A transverse-traceless (TT) polarization relative to a wave vector $k$ is a symmetric matrix $e$ with vanishing trace and with $e\cdot k=0$. For the axis wave vector (momentum along the first coordinate), the C10 deterministic TT frame supplies a standard pair of polarizations, conventionally labeled $+$ and $\times$, unique up to sign. The $+$ choice is the diagonal transverse block written here.
The surrounding preflight already defines the true Regge action $S(\ell)=\sum_e\sqrt{\ell_e},(2\pi-\sum\theta)$ via Cayley–Menger dihedral angles, proves flat deficits and flat action vanish, and packages status flags for the continuum isotropy target (still OPEN as a theorem; supported only by preregistered numerics).
proof idea
Definition by exhaustive pattern match on $\mathrm{Fin},3\times\mathrm{Fin},3$. The only nonzero entries are the $(1,1)$ and $(2,2)$ slots, set to $1/\sqrt{2}$ and $-1/\sqrt{2}$ respectively; every other pair returns $0$. No lemmas are invoked.
why it matters
This matrix is the concrete $+$ witness that makes the continuum and second-variation pipelines non-vacuous. Downstream, axis_plus_continuum_symbol instantiates the closed continuum-symbol target at this polarization and the axis wave vector, claiming value $-1/4$ once the isotropy target is discharged. The flat second-variation module builds the reduced $S''(0)$ Finset sum and proves the Schläfli formula applies verbatim to this instance (GATE A2(c)), without claiming a numerical value.
In-module, axisTTPolarizationPlus_isTT certifies that the table is a genuine TT polarization for the axis wave vector, and status_flags_grounded ties preflight Boolean flags to kernel theorems at $N=3$. Within the QG full-theory campaign this is the standard $+$ leg of the C10 TT frame used to probe whether the true nonlinear Regge TT Bloch symbol is isotropic with Einstein–Hilbert coefficient $K(0)=-(1/4)I_{TT}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.