IsTTPolarization4D
plain-language theorem explainer
Defines continuum TT polarization in 4D: a mode–matrix pair is TT-polarized when the matrix is algebraically transverse-traceless relative to the mode and has Frobenius norm squared equal to one. Gravity continuum-preflight and algebraic-closer results cite it as the Gate-A0 style hypothesis class. The body is a pure conjunction of the algebraic TT predicate with the unit Frobenius pin.
Claim. A wave mode $m \in \mathbb{R}^4$ and a real $4\times 4$ matrix $E$ form a continuum TT polarization when $E$ is symmetric, Euclidean-traceless, and transverse to $m$, and $\|E\|_F^2 = 1$.
background
This module freezes the independent continuum target for the 4D Regge weak-field campaign before any recovery proof: canonical periodic Freudenthal 4-torus mesh ($N \ge 3$), normalized TT data, pure-gauge family, and honesty decoys. Nothing here proves continuum recovery of Einstein–Hilbert.
Wave4 is a real 4-vector (Bloch/mode data). Mat4 is a real $4\times 4$ matrix (edge or metric perturbation amplitudes). Upstream IsTT m E means $E$ is symmetric, Euclidean-traceless, and transverse to $m$. The local frobeniusNormSq is $\sum_{i,j} E_{ij}^2$.
The doc-comment states the modeling reason for the pin: without Frobenius normalization, a fixed continuum coefficient on TT data is ill-posed. This is the Gate A0 analog in the frozen contracts.
proof idea
Definitional abbreviation, not a proved statement. The predicate is the conjunction of the upstream algebraic TT predicate IsTT m E (symmetric, traceless, transverse) with the equality frobeniusNormSq E = 1. No tactics or lemmas are applied at the definition site; downstream theorems discharge each conjunct separately and pack them with ⟨_, _⟩.
why it matters
This is the normalized TT hypothesis class used throughout the 4D continuum preflight and algebraic closer. Downstream, axisTTPlusNormalized_isTTPolarization and axisTTCrossNormalized_isTTPolarization inhabit it on the axis plus and cross polarizations; continuum_target_hypothesis_nonvacuous and the closer's tt_witnesses_nonvacuous record that the class is non-empty. The recognition-mesh bridge ExactJEqualsTrueReggeHessian quantifies over this predicate when identifying the exact-$J$ amplitude Hessian with the true-weight Regge Hessian.
In the module's frozen contracts it is item 2: Frobenius-normalized Euclidean TT polarizations. It does not close continuum Tendsto targets (Regge4DContinuumEHTarget, S_RS_converges_EH_4d remain open); it only makes the coefficient comparison well-posed so later equality can be observed rather than fitted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.