frobeniusNormSq_axisTTPlus
plain-language theorem explainer
The unnormalized plus TT polarization matrix diag(0,0,1,−1) has Frobenius norm-squared equal to 2. Gravity analysts cite it whenever the continuum or Regge second-variation faces are evaluated on the standard plus witness. The proof is a one-line numerical reduction of the double sum over Fin 4.
Claim. Let $H_+$ be the $4\times 4$ matrix with $1$ at $(2,2)$, $-1$ at $(3,3)$, and zeros elsewhere (the unnormalized plus transverse-traceless polarization). Then $\|H_+\|_F^2 = 2$.
background
This module sits in Arc 2 of the 4D Regge–continuum comparison. The continuum side produces the phase-averaged second variation $ehFace,H,k = -\tfrac14,|k|^2,|H|_F^2$ from the Levi-Civita connection alone. The discrete side is the Regge action $\sum_h A_h\delta_h$, related to $\int R\sqrt g$ by an unknown normalization $\rho$. The module leaves $\rho$ free and forces $\rho=1/2$ by matching faces on a fixed witness.
The witness polarization is the plus mode axisTTPlus: the diagonal matrix $\mathrm{diag}(0,0,1,-1)$. Its Frobenius squared norm is $\sum_{i,j} H_{ij}^2$, the standard Euclidean sum of squares of entries. That scalar multiplies the wave-number factor in both the continuum and dictionary identities, so its exact value must be pinned before any coefficient comparison.
An identical statement already exists in the frozen preflight module; this copy lives next to the derived normalization theorems so the discrimination lemmas can cite a local fact.
proof idea
One-line wrapper: unfold the Frobenius double sum and the explicit matrix entries of the plus polarization, reduce the finite sums over Fin 4, and discharge the arithmetic by norm_num. Only the two nonzero diagonal entries $\pm 1$ contribute, each squaring to 1, hence the total is 2.
why it matters
Without $|H_+|F^2=2$, the dictionary witness value, the non-vanishing check, and the refutation of $\rho=1$ cannot fire. Downstream, dictionary_witness_value rewrites the exact midpoint Bloch face on $(H+,k)$ to $-1/4$ by substituting this identity together with the wave-norm fact; witness_nonzero uses it to show the product of norms is nonzero, so the pinning argument for $\rho$ is not $0=0$; rho_one_fails uses it to show that the Regge face at $\rho=1$ disagrees with the continuum face at the same witness.
In the broader story this is bookkeeping for A4: Regge's classical normalization $\rho=1/2$ (equivalently the discrete bookkeeping factor 2) is forced by matching two independently computed faces, not assumed. The continuum coefficient $-1/4$ and the dictionary coefficient $-1/8$ differ by exactly that factor; both are correct for their own functionals. The result is pure linear algebra on a fixed matrix and does not itself invoke the forcing chain T0–T8, but it is a necessary pin inside the gravity-side continuum limit that those landmarks eventually feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.