frobeniusPairing4D
plain-language theorem explainer
Euclidean Frobenius pairing of two real 4×4 matrices: the sum of entrywise products. Gravity analysts cite it as the bilinear form that polarizes the continuum Einstein–Hilbert face and appears as the limit of the torus-normalized midpoint TT first variation. The body is the standard double sum over Fin 4 indices.
Claim. For real $4\times 4$ matrices $H$ and $K$, the Euclidean Frobenius pairing is $\langle H,K\rangle_F := \sum_{i=1}^{4}\sum_{j=1}^{4} H_{ij} K_{ij}$.
background
The ambient module studies the directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field transverse-traceless (TT) sector. Matrices live in Mat4, the 4×4 continuum preflight type used for weak-field strain modes on the torus.
The classical Frobenius inner product on matrix space is the unique (up to scale) $O(n)$-invariant pairing given by the entrywise $\ell^2$ product. Here $n=4$ matches the Euclidean 4D continuum face. Downstream polarization identities relate differences of squared Frobenius norms on $H\pm K$ to four times this pairing, which is the algebraic engine behind the continuum-face cross term.
Module honesty restricts the whole development to that Euclidean weak-field TT sector: not a sourced field equation, not Ricci or null focusing, and not GAP1 closure.
proof idea
Pure definition: expand as the double finite sum $\sum_{i:\mathrm{Fin},4}\sum_{j:\mathrm{Fin},4} H_{ij}K_{ij}$. No lemmas, no tactics.
why it matters
This pairing is the target bilinear form for the headline continuum TT theorem: the torus-normalized midpoint first variation tends to $-(1/4)$ times the Frobenius pairing of the two TT strains. It is used directly by the algebraic continuum-face polarization identity (difference of EH-scale faces on $H\pm K$ equals $-1/4$ times the pairing), by the polarization identity relating Frobenius-norm squares on $H\pm K$ to four times the pairing, by the trivial self-pairing rewrite of the squared Frobenius norm, and by the certificate bundle that packages line derivative, polarization, and the continuum TT limit.
In the Recognition gravity stack this is the Euclidean weak-field cross-term skeleton that a future Freudenthal exact-$J$ metric refinement would have to match before Lorentzian null-dyad Ricci transport. It does not itself close GAP1 or supply a source equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.