frobSq
plain-language theorem explainer
The squared Frobenius norm of a 4×4 real matrix: sum of squares of all entries. Continuum and exact EH second-variation modules cite it as the polarization amplitude factor in the TT face formula. It is a one-line double sum, restated locally so the continuum derivation never imports the Regge dictionary.
Claim. For a real $4\times 4$ matrix $H$, define $\|H\|_F^2 := \sum_{i,j=0}^{3} H_{ij}^2$.
background
This module (Arc 2, step 7) derives the continuum Einstein-Hilbert second variation on a real transverse-traceless plane wave from the linearized Levi-Civita connection alone. It deliberately imports only Mathlib and edge TT linear algebra, so no Regge coefficient can leak in.
The discrete Regge side already uses an identical sum-of-squares of polarization components. Restating that scalar here keeps the continuum face formula self-contained. The matrix $H$ is the constant amplitude of the real cosine metric perturbation $h(x)=H\cos(k\cdot x)$; under the TT gauge the second-variation density is proportional to $|H|_F^2$ times $\cos^2$ of the local phase.
Named classical input A1 is the linearized Christoffel symbol; the Frobenius square is the algebraic amplitude that multiplies the momentum factor after all derivatives and contractions are performed.
proof idea
Pure definition: expand the double sum over Fin 4 × Fin 4 of entrywise squares. No lemmas, no tactics. The body is definitionally the same expression as the Regge-side Frobenius square, copied so this file stays import-isolated.
why it matters
Every continuum face coefficient in this arc factors through this scalar. densityOfPhase multiplies $-(1/2),k^2|H|_F^2\cos^2\theta$; ehFace is the phase average $-(1/4),k^2|H|_F^2$. Theorems ehFace_rigid and ehSecondVariationDensity_tt pin that the Levi-Civita calculation produces exactly that prefactor.
Downstream, EHSecondVariationExact4D normalizes at $|H|_F^2=2$ and proves the exact (non-linearized) wavelength average equals ehFace, and that a longitudinal decoy misses the face. The definition therefore closes the non-circular comparison between continuum EH and the banked Regge midpoint dictionary without importing the answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.