axisTTPlusNormalized_isTT
plain-language theorem explainer
The Frobenius-normalized axis plus polarization remains algebraically TT against the axis wave covector. Gravity analysts freeze this as Gate-A0 style TT data on the 4-torus mesh before continuum symbol comparisons. The proof lifts the unnormalized TT certificate through scalar multiplication: symmetry and transversality are inherited, and the Euclidean trace stays zero by direct sum.
Claim. Let $m=(1,0,0,0)$ be the axis wave covector and let $H_+$ be the unnormalized plus polarization $\mathrm{diag}(0,0,1,-1)$. If $H_+^{\mathrm{n}}$ denotes its Frobenius-normalized scalar multiple, then $H_+^{\mathrm{n}}$ is algebraically TT with respect to $m$: it is symmetric, Euclidean-traceless, and transverse to $m$.
background
This module freezes independent continuum targets for the 4D Regge weak-field campaign before any continuum recovery is claimed. Among the frozen contracts are Frobenius-normalized Euclidean TT polarizations (Gate A0 analog) on the canonical periodic Freudenthal 4-torus of side $N\ge 3$.
Algebraic TT is the triple of properties from the edge TT decomposition layer: a $4\times 4$ matrix $H$ is TT against a wave covector $m$ when it is symmetric, Euclidean-traceless ($\sum_i H_{ii}=0$), and transverse ($H m=0$). The unnormalized plus polarization is the diagonal matrix with entries $(0,0,1,-1)$; the axis wave is $m=(1,0,0,0)$. The unnormalized matrix is already known to be TT.
The normalized object is a real scalar multiple of that matrix, chosen so the Frobenius norm squared equals one. Scalar multiples preserve the TT cone once transversality under scaling is available.
proof idea
Term-mode proof that packages the three TT conjuncts via refine ⟨?_, ?_, ?_⟩.
- Symmetry: unfold the normalized matrix as a scalar multiple and apply the symmetry half of the unnormalized certificate
axisTTPlus_isTT, using that scalar multiplication preserves matrix entries componentwise. - Tracelessness: unfold Euclidean trace on the scaled matrix; the four diagonal contributions reduce by
Fin.sum_univ_fourto a multiple of $1+(-1)=0$. - Transversality: invoke the local lemma that scalar multiplication preserves transversality, feeding the transversality half of
axisTTPlus_isTT.
why it matters
Feeds directly into axisTTPlusNormalized_isTTPolarization, which pairs this TT certificate with the unit Frobenius-norm identity to produce a full normalized TT polarization datum. That datum is part of the frozen Gate-A0-style TT bank used throughout the Regge 4D continuum preflight: later symbol comparisons (exact flat cross-term symbol versus the independently frozen linearized EH quadratic) are evaluated on these polarizations.
The module explicitly does not prove continuum recovery; OPEN props such as Regge4DContinuumEHTarget and S_RS_converges_EH_4d remain uninhabited. This lemma only locks the algebraic TT status of the normalized plus mode so those later comparisons have a fixed, non-fitted probe. It sits in the gravity analysis stack supporting the continuum-closure plan, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.