axisTTPolarizationCross
plain-language theorem explainer
Explicit 3×3 matrix for the × TT polarization along the coordinate axis: only the transverse off-diagonal entries equal 1/√2, all others zero. Gravity analysts cite it when building axis-directed TT Bloch symbols for the true nonlinear Regge action. It is a pure case-table definition, not a proved claim.
Claim. The $\times$-polarization for the axis wave direction is the symmetric map $e:\{0,1,2\}^2\to\mathbb{R}$ with $e_{12}=e_{21}=1/\sqrt{2}$ and $e_{ij}=0$ for all other pairs $(i,j)$.
background
This module is Stage 1 of the Regge TT continuum-symbol program in the QG full-theory campaign. It defines the true nonlinear 3D Regge action on a periodic Freudenthal torus as a function of an arbitrary edge squared-length field, reusing Cayley–Menger dihedral angles, and sets up TT Bloch symbol objects (plane-wave edge fields, second differences, continuum-symbol targets).
A TT polarization is a symmetric, traceless, transverse 3×3 tensor relative to a chosen wave vector. For the axis wave vector the two standard linear polarizations are $+$ (diagonal transverse) and $\times$ (off-diagonal transverse). This declaration supplies the $\times$ table with the conventional $1/\sqrt{2}$ normalization so that the pair is orthonormal under the Frobenius product on the transverse plane.
Sibling edge-field and deficit machinery (flat fields, conformal fields, true Regge action) lives in the same file; the continuum isotropy target remains open and is only numerically evidenced.
proof idea
No proof: the declaration is a definition by exhaustive pattern match on Fin 3 × Fin 3. Each of the nine entries is a literal real constant (zero or $1/\sqrt{2}$). Downstream theorems discharge TT axioms by fin_cases and simp against this table.
why it matters
Supplies the concrete $\times$-witness consumed by axisTTPolarizationCross_isTT, which asserts that this matrix is a TT polarization for the axis wave vector. That witness is part of the scaffolding for TT Bloch symbols of the true nonlinear Regge action, the objects whose continuum limit is the open target ReggeTTContinuumIsotropyTarget (numerically reported isotropic with $K(0)=-(1/4)I_{TT}$, matching linearized Einstein–Hilbert). Without an explicit normalized $\times$ table, the axis-direction TT sector cannot be instantiated in Lean. The definition itself carries no continuum or dynamical content; it only fixes the polarization basis used by the preflight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.