axisTTCrossNormalized_isTT
plain-language theorem explainer
The Frobenius-normalized axis cross polarization is algebraically TT against the axis wave covector: symmetric, Euclidean-traceless, and transverse. Continuum-preflight and Gate-A0 style arguments cite it when locking normalized TT data before symbol comparison. The proof scales the unnormalized cross TT certificate by a constant and checks the three IsTT conjuncts.
Claim. Let $m=(1,0,0,0)$ be the axis wave covector and let $H$ be the Frobenius-normalized cross polarization (the scalar multiple of the matrix with $H_{23}=H_{32}=1$ and zeros elsewhere). Then $H$ is algebraically TT with respect to $m$: it is symmetric, Euclidean-traceless, and transverse to $m$.
background
This module freezes continuum-preflight contracts for the 4D Regge campaign: canonical Freudenthal 4-torus mesh, Frobenius-normalized Euclidean TT polarizations, and an independently defined linearized Einstein-Hilbert quadratic. Nothing here proves continuum recovery; it only locks the TT data and decoys before later symbol comparison.
Algebraic TT (IsTT) means a $4\times 4$ matrix is symmetric, Euclidean-traceless (sum of diagonal entries zero), and transverse to a wave covector $m$. The unnormalized cross polarization axisTTCross places ones at the $(2,3)$ and $(3,2)$ slots; axisTTCross_isTT already certifies it is TT against the axis wave $m=(1,0,0,0)$. The normalized object is that matrix scaled to unit Frobenius norm, the Gate A0 analog named in the frozen contracts.
proof idea
Term-mode refine into the three IsTT conjuncts. Symmetry: pointwise simp through the scalar multiple, using the symmetry half of axisTTCross_isTT. Tracelessness: unfold Euclidean trace on the scaled matrix, sum over Fin 4, and reduce via the unnormalized cross entries (diagonal zero). Transversality: apply smul_preserves_transverse to the transverse half of axisTTCross_isTT, so constant scaling keeps $H\cdot m=0$.
why it matters
Feeds axisTTCrossNormalized_isTTPolarization, which packages this TT certificate with the unit Frobenius-norm identity to lock a normalized TT polarization for preflight. That is the Gate A0 analog in the module's frozen contracts: Frobenius-normalized Euclidean TT data must be in place before comparing the exact flat cross-term symbol to the independently frozen EH quadratic on TT modes.
In the QG continuum-closure plan this is bookkeeping, not recovery. The OPEN continuum Tendsto targets and S_RS_converges_EH_4d remain uninhabited; this lemma only ensures the normalized cross mode is a legitimate TT probe when those later comparisons run.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.