frobeniusSq
plain-language theorem explainer
Defines the squared Frobenius norm of a 3×3 real matrix as the sum of squares of all nine entries (ordered-pair convention). Anyone working the Regge TT continuum-symbol or normalization gates cites it as the pin that makes a fixed numerical target well-posed. The body is a two-fold finite sum, not a theorem.
Claim. For a real $3\times 3$ matrix $E$, the Frobenius square-sum is $\|E\|_F^2 := \sum_{i=1}^{3}\sum_{j=1}^{3} E_{ij}^2$, summing over all ordered index pairs.
background
This module audits scaling well-posedness of the fixed continuum TT Bloch-symbol target $-1/4$ (Crux-1(c), Gate A0 of the Normalization-Gated Schläfli Two-Jet protocol). The plane-wave edge family is linear in the polarization matrix $E$ through the edge-class coefficient $c_d(E)=\sum_{ij} E_{ij} D_d^i D_d^j$, so $E\mapsto c\cdot E$ only reparametrizes the same family and the second-difference quadratic form must scale by $c^2$.
A TT polarization (from the preflight module) is a symmetric, traceless, $m$-transverse $3\times 3$ matrix whose Frobenius square-sum equals $1$. Both that pin and the edge coefficient use the ordered-pair double sum, i.e. the standard quadratic-form convention $D^T E D$. The present definition isolates that common square-sum so the audit can name it once and prove its scaling and pinning properties separately.
proof idea
Pure definition: unfold to the double sum $\sum_i\sum_j E_{ij}\cdot E_{ij}$ over Fin 3. No lemmas, no tactics. Downstream scaling lemmas (frobeniusSq_smul) simply unfold this and push the scalar through the two finite sums.
why it matters
The fixed-value claim over TT polarizations is well-posed only because this quantity is pinned to $1$ and scales as $c^2$ under $E\mapsto c\cdot E$. Sibling theorems frobeniusSq_smul, isTTPolarization_frobenius_pinned, and isTTPolarization_smul_iff use it to show the only rescalings that stay in the hypothesis class satisfy $c^2=1$, under which the symbol is invariant.
Downstream, the 4D exact-flat Hessian norm gate feeds it into continuum EH faces: continuumEHDiscreteFace and continuumEHScaleExplicit multiply bookkeeping or unit-Frobenius TT coefficients by this square-sum, recovering the $-1/4$ and $-1/8$ faces. The naming-defect note in ReggeNormalizationDerived4D records that one of those faces is the continuum $\int R\sqrt{g}$ face rather than the discrete Regge face. Within the QG full-theory campaign this is the normalization kernel that keeps Gate A0 coherent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.