axisTTCrossNormalized_isTTPolarization
plain-language theorem explainer
The axis cross-mode Euclidean polarization, after Frobenius normalization, is a continuum TT polarization on the 4D wave carrier. Gravity analysts cite it when freezing Gate-A0 style TT data before continuum symbol comparisons. The proof is a two-field constructor pairing the algebraic TT lemma with the unit-Frobenius pin.
Claim. The axis-aligned cross TT matrix $E_{\times}$, normalized so that its Frobenius norm squared equals $1$, is a continuum TT polarization for the axis wave mode $m$: it is algebraically transverse-traceless with respect to $m$ and satisfies $\|E_{\times}\|_F^2 = 1$.
background
This module is the first binding increment of the 4D Regge continuum closure plan. It freezes the independent weak-field Einstein-Hilbert target, the canonical periodic Freudenthal 4-torus mesh ($N \ge 3$), normalized TT data, pure-gauge families, and honesty decoys before any continuum recovery is claimed. Nothing here proves continuum recovery.
A continuum TT polarization is defined as the conjunction of algebraic TT (transverse-traceless relative to a wave mode $m$) and Frobenius normalization $\mathrm{frobeniusNormSq}, E = 1$. Without the pin, a fixed continuum coefficient is ill-posed: scale freedom would make any later match to the frozen EH quadratic $-(1/4)$ meaningless.
The objects here are the axis wave mode and the cross-channel TT matrix on that axis, already normalized to unit Frobenius norm. Spatial dimension $D = 3$ is the ambient RS convention (T8), but this lemma is purely about the 4D Euclidean polarization algebra on the mesh carrier.
proof idea
Term-mode pair constructor. Unfold IsTTPolarization4D to the conjunction IsTT m E ∧ frobeniusNormSq E = 1, then supply the two already-proved conjuncts: axisTTCrossNormalized_isTT (algebraic TT for the axis cross matrix) and frobeniusNormSq_axisTTCrossNormalized (unit Frobenius pin). No further rewriting or case analysis.
why it matters
Frobenius-normalized TT data is Gate A0 of the 4D continuum preflight: without inhabited TT witnesses, the OPEN continuum target (exact flat cross-term symbol equals the frozen EH coefficient on TT and vanishes on pure gauge) is vacuous. Downstream, continuum_target_hypothesis_nonvacuous packages this lemma with the plus-channel twin to prove the TT class is nonempty. Regge4DAlgebraicCloser.cross_normalized_isTTPolarization re-exports it as a one-line wrapper for the algebraic closer layer. edge_tt_decomposition in the edge-TT decomposition closer consumes the same TT infrastructure when attaching ledger bookkeeping to geometric faces.
In the QG campaign this is scaffolding for later observation that the geometry-derived full symbol attains the independently frozen EH quadratic $-(1/4)$, never a fitted scale. Continuum Tendsto Props and S_RS_converges_EH_4d remain open; this lemma only banks the polarization witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.