axisTTPlusNormalized_isTTPolarization
plain-language theorem explainer
The Frobenius-normalized axis-plus matrix is a continuum TT polarization against the axis wave covector: algebraically transverse-traceless with unit Frobenius norm squared. Continuum-preflight nonvacuity, the algebraic closer, and the edge-TT decomposition closer all cite it as the plus-channel Gate A0 witness. Proof is a one-line pairing of the TT lemma with the Frobenius-pin lemma.
Claim. Let $m=(1,0,0,0)$ be the axis wave covector and let $E_+=2^{-1/2}E_+^{\mathrm{raw}}$ be the axis-plus polarization scaled to unit Frobenius norm. Then $E_+$ is a continuum TT polarization relative to $m$: it is algebraically transverse-traceless against $m$ and $\|E_+\|_F^2=1$.
background
This module is the first binding increment of the Regge 4D continuum-closure plan. It freezes the independent weak-field Einstein-Hilbert target, the canonical Freudenthal 4-torus mesh ($N\ge 3$), normalized TT data, pure-gauge family, and honesty decoys before any continuum limit is attempted. Nothing here proves continuum recovery.
A continuum TT polarization is the conjunction of algebraic transverse-tracelessness against a Euclidean wave covector and unit Frobenius norm squared. Without that pin, a fixed continuum coefficient is ill-posed (Gate A0 analog). The axis wave is the covector $m=(1,0,0,0)$. The axis-plus matrix is the standard plus polarization along that axis, scaled by $1/\sqrt{2}$.
Two upstream facts are already on the shelf: the scaled matrix is TT against the axis wave, and its Frobenius norm squared equals one.
proof idea
Term-mode constructor for a conjunction. The goal IsTTPolarization4D unpacks as algebraic TT plus unit Frobenius norm squared, so the proof is exactly the ordered pair of the two component lemmas: the already-proved TT property of the normalized axis-plus matrix, and the already-proved identity that its Frobenius norm squared equals one. No further rewriting.
why it matters
Supplies the plus-channel witness that the OPEN continuum target quantifies over a nonempty TT class (paired with the cross witness in the nonvacuity theorem). Re-exported by the algebraic closer as the named plus-normalized polarization fact, and consumed by the edge-TT decomposition closer when attaching the algebraic decomposition ledger.
In the QG full-theory campaign this is frozen Gate A0 data: Frobenius-normalized Euclidean TT polarizations against which the independently defined linearized EH quadratic (using kappa_einstein, not a free lattice scale) will later be compared. It does not inhabit the continuum Tendsto Props, does not reverse-engineer lattice weights from the EH answer, and leaves S_RS_converges_EH_4d uninhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.