frobeniusSq_smul
plain-language theorem explainer
The squared Frobenius sum of a real 3×3 matrix scales by c² under entrywise multiplication by a real scalar c. Anyone checking that the TT polarization class is normalization-gated by the Frobenius pin cites this identity. The proof unfolds the double sum and factors c² out of each summand by ring algebra.
Claim. For every real scalar $c$ and every real $3\times 3$ matrix $E$, the squared Frobenius sum satisfies $\sum_{i,j}(c E_{ij})^2 = c^2 \sum_{i,j} E_{ij}^2$.
background
This module audits scaling well-posedness for the continuum TT Bloch symbol target in the Regge TT program (Crux-1(c), Gate A0 of the Normalization-Gated Schläfli Two-Jet protocol). The open isotropy target claims a fixed value $-1/4$ on every TT polarization. That fixed number is meaningful only if the hypothesis class cannot be rescaled into a contradiction.
Plane-wave edge lengths are linear in the polarization matrix $E$ through the edge-class coefficient $c_d(E)=\sum_{ij} E_{ij} D_d^i D_d^j$. Replacing $E\mapsto c\cdot E$ reparametrizes the same family ($t\mapsto c\cdot t$), so second-difference quadratic forms must scale by $c^2$. The Frobenius square-sum $\mathrm{frobeniusSq},E:=\sum_{i,j} E_{ij}^2$ is the fourth conjunct of the TT polarization predicate: it pins $\sum_{ij} E_{ij}^2=1$ and uses the same all-ordered-pairs convention as the edge coefficient (standard $D^T E D$).
This lemma is the elementary quadratic scaling step for that pin.
proof idea
Unfold the definition of the squared Frobenius sum (double Finset.sum of entrywise products). Pull the scalar $c^2$ out of the outer sum via Finset.mul_sum, then out of the inner sum the same way. On each summand the goal reduces to $(c E_{ij})(c E_{ij})=c^2(E_{ij} E_{ij})$, which ring closes. No external lemmas beyond Finset sum-scalar identities are required.
why it matters
Feeds directly into isTTPolarization_smul_iff: starting from a TT polarization $E$, the rescaled matrix $c\cdot E$ remains a TT polarization exactly when $c^2=1$. Symmetry, tracelessness, and transversality survive every rescaling; the Frobenius pin is the only normalization-fixing clause. With that pin, quantifying a fixed continuum symbol value over the TT class is well-posed, while an unnormalized fixed-value claim would be contradictory (the symbol itself scales as $c^2$ under $E\mapsto c\cdot E$).
In the QG full-theory campaign this closes the scaling-coherence half of Gate A0 for the Regge TT continuum isotropy target. It is pure linear algebra on $3\times 3$ matrices, not a gravity identity, but it is the kernel step that makes the $-1/4$ claim non-vacuous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.