frobId_axisTTPlus
plain-language theorem explainer
The unnormalized plus TT polarization diag(0,0,1,−1) has Frobenius squared norm exactly 2. Downstream dictionary-m² and Einstein–Hilbert face evaluations on this witness cite the pin so coefficients become pure numerals. Proof is a direct unfold of the 4×4 sum of squares followed by norm_num.
Claim. Let $E$ be the unnormalized plus transverse-traceless polarization matrix with $E_{22}=1$, $E_{33}=-1$, and all other entries zero. Then its Frobenius squared norm equals two: $\sum_{i,j=0}^{3} E_{ij}^{2} = 2$.
background
In the 4D Regge continuum analysis, banked TT witnesses are fixed 4×4 real matrices. The plus polarization is the unnormalized diagonal form diag(0,0,1,−1): only the spatial (2,2) and (3,3) entries are nonzero. The Frobenius squared norm is the plain sum of squares of all sixteen entries, $\sum_{i,j} E_{ij}^{2}$.
This module (Arc 2, step 8) compares the geometric hinge fold of the exact Regge action against the algebraic midpoint-Bloch dictionary. Both sides are evaluated on TT witnesses at a fixed symbol direction whose momentum squared is also 2. Without pinning the Frobenius weight of each witness, continuum coefficients are ill-posed: a fixed numerical second variation would scale with an arbitrary matrix normalization.
Upstream, the same Frobenius definition appears in the midpoint-M² identity layer and in the continuum preflight package that states continuum TT polarization requires algebraic TT plus Frobenius normalization.
proof idea
One-line computational proof. Unfold the Frobenius squared-norm definition and the explicit matrix entries of the plus polarization. The double sum over Fin 4 collapses to two nonzero contributions, $1^{2}+(-1)^{2}$. Discharge the finite sum with norm_num and Fin.sum_univ_four.
why it matters
This pin is the normalization half of every numerical certificate on the plus witness in the geometric-fold-versus-dictionary comparison. The parent dict_m2_axisTTPlus_symbolDir rewrites the dictionary m² via the eighth-Frobenius TT identity, substitutes this lemma and the wave-id pin, and obtains exactly −1/2. The parent ehFace_axisTTPlus_symbolDir likewise substitutes Frobenius weight 2 and momentum squared 2 into the continuum EH face and obtains −1.
Those two numerals feed the module’s main claim: at both banked TT witnesses the dictionary m² is exactly twice the geometric hinge moment, so residual R1 (fold equals dictionary) is false and the corrected residual is the factor-of-two statement already present as discreteExactReggeSymbol. Combined with Regge’s 1/ρ from step 7, that accounts for the residual factor 4 recorded in the torus continuum limit (−1/16 geometric against −1/4 Einstein–Hilbert). Only the ρ half is derived from first principles; this lemma makes the fold-to-dictionary half fully explicit on the plus axis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.