frobeniusNormSq_axisTTCrossNormalized
plain-language theorem explainer
The axis cross TT polarization, scaled by 1/√2, has Frobenius squared norm exactly 1. Anyone assembling Gate-A0-style continuum TT data on the 4-torus mesh cites this pin. The proof is a short algebraic reduction: scale-homogeneity of the Frobenius square, the unnormalized cross norm 2, and (1/√2)² = 1/2.
Claim. Let $E$ be the axis cross TT matrix and set $\hat E := (\sqrt{2})^{-1} E$. Then the Frobenius squared norm satisfies $\|\hat E\|_F^2 = 1$.
background
This module is the first binding increment of the Regge 4D continuum closure plan. It freezes the independent continuum target, canonical mesh carrier, normalized TT data, pure-gauge family, and honesty decoys before any continuum recovery is claimed. Nothing here proves continuum recovery.
Among the frozen contracts is Frobenius-normalized Euclidean TT polarizations (Gate A0 analog). The Frobenius squared norm of a $4\times 4$ real matrix $E$ is $\sum_{i,j} E_{ij}^2$. The unnormalized axis cross polarization axisTTCross has Frobenius square 2; the normalized object is the scalar multiple $(\sqrt{2})^{-1}\cdot$ that matrix.
Without the unit-Frobenius pin, a fixed continuum coefficient on TT modes is ill-posed: the later comparison of the exact flat cross-term symbol to the independently frozen Einstein-Hilbert quadratic needs a canonical amplitude on the polarization tensors.
proof idea
One short term-mode chain. Unfold the definition of the normalized axis cross (scalar $(\sqrt{2})^{-1}$ times the unnormalized matrix). Apply scale-homogeneity of the Frobenius square: $|cE|_F^2 = c^2|E|_F^2$. Substitute the already-proved facts $|\mathrm{axisTTCross}|_F^2 = 2$ and $((\sqrt{2})^{-1})^2 = 1/2$. Finish by norm_num: $(1/2)\cdot 2 = 1$.
why it matters
Feeds directly into axisTTCrossNormalized_isTTPolarization, which packages algebraic TT-ness with this unit-Frobenius pin into the continuum TT polarization predicate. That predicate is part of the frozen Gate-A0-style TT data required before any honest comparison of the exact flat Regge cross-term symbol to the independently frozen linearized EH quadratic (with kappa_einstein, not a free lattice scale).
In the module's tier tags this sits under THEOREM: Frobenius pin lemmas. The continuum Tendsto targets and S_RS_converges_EH_4d remain OPEN; this lemma only locks the polarization amplitude so later algebraic closers can observe equality rather than fit a scale. It does not reverse-engineer lattice weights from the EH answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.