frobeniusNormSq_axisTTPlusNormalized
plain-language theorem explainer
The axis transverse-traceless plus polarization, scaled by $1/\sqrt{2}$, has Frobenius squared norm exactly one. Anyone pinning continuum TT data or Gate-A0-style polarization contracts cites this. The proof is a short algebraic reduction: scale the unnormalized pin of norm two by the squared inverse square root of two.
Claim. Let $E_+$ be the unnormalized axis TT-plus $4\times 4$ matrix and set $\widehat{E}_+ := (\sqrt{2})^{-1} E_+$. Then the Frobenius squared norm satisfies $\|\widehat{E}_+\|_F^2 = 1$, where $\|E\|_F^2 = \sum_{i,j=0}^{3} E_{ij}^2$.
background
This module freezes independent continuum targets for the 4D Regge weak-field campaign before any recovery proof: canonical Freudenthal 4-torus mesh ($N\ge 3$), Frobenius-normalized Euclidean TT polarizations, and an Einstein-Hilbert quadratic fixed by kappa_einstein, not by lattice fitting. Continuum recovery itself remains open.
The Frobenius squared norm on $4\times 4$ real matrices is the sum of squared entries. The unnormalized axis TT-plus matrix has Frobenius squared norm $2$. The normalized object is that matrix scaled by $(\sqrt{2})^{-1}$. Without a unit Frobenius pin, a fixed continuum coefficient on TT modes is ill-posed; the module treats this pin as the Gate A0 analog for continuum TT data.
proof idea
Unfold the normalized polarization to $(\sqrt{2})^{-1}\cdot E_+$. Apply the scaling identity $|cE|_F^2 = c^2|E|F^2$, substitute the unnormalized pin $|E+|_F^2 = 2$, and replace $((\sqrt{2})^{-1})^2$ by $1/2$. The product $(1/2)\cdot 2$ reduces by norm_num to $1$.
why it matters
Feeds the packing theorem that the normalized axis plus matrix is a continuum TT polarization: algebraic TT plus unit Frobenius norm. That packing is part of the frozen Gate-A0-style contract in the Regge 4D continuum preflight. The module is the first binding increment of the QG full-theory 4D continuum closure plan; it does not prove continuum Tendsto recovery or inhabit $S_{\mathrm{RS}}\to\mathrm{EH}$. The pin keeps later symbol-vs-EH comparisons honest: the EH quadratic is frozen independently, and lattice symbols must observe equality rather than absorb a free scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.