frobeniusNormSq_axisTTCross

This module freezes independent continuum targets for the 4D Regge gravity campaign before any continuum-limit proof: canonical Freudenthal 4-torus mesh, Frobenius-normalized Euclidean TT polarizations, and an independently defined linearized Einstein-Hilbert quadratic. Nothing here proves continuum recovery.

The matrix axisTTCross is the unnormalized cross TT polarization: only the symmetric off-diagonal pair $H_{23}=H_{32}=1$ is nonzero. The local Frobenius squared norm is the entrywise sum of squares $\sum_{i,j},E_{ij}^{2}$ on Mat4 (real $4\times 4$ matrices indexed by Fin 4). Without a fixed Frobenius pin, a continuum TT coefficient is ill-posed; Gate A0-style normalization depends on knowing this raw norm first.

Term-mode proof by direct evaluation. Unfold the Frobenius sum and the piecewise definition of the cross matrix, reduce the double sum over Fin 4 with Fin.sum_univ_four, then close by norm_num. Only the two unit entries contribute, each squaring to 1, so the total is 2.

Feeds the immediate parent frobeniusNormSq_axisTTCrossNormalized, which scales the cross polarization by $1/\sqrt{2}$ and obtains unit Frobenius norm. That normalized witness is part of the frozen TT data contract in the Regge 4D continuum preflight: Frobenius-normalized Euclidean TT polarizations (Gate A0 analog) must be fixed before comparing the exact flat cross-term symbol to the independently frozen EH quadratic.

In the module tiering this is a THEOREM-class Frobenius pin lemma. It does not touch continuum Tendsto goals (Regge4DContinuumEHTarget, S_RS_converges_EH_4d) or gap-action recovery; it only banks the algebraic norm needed so later symbol comparisons are well-posed and not reverse-engineered from the EH answer.