frobSq_eq
plain-language theorem explainer
On any 4×4 real matrix the continuum-side Frobenius square equals the shared Frobenius-norm-squared used on the Regge side; the two names are definitionally identical double sums. Gravity analysts comparing Einstein–Hilbert and Regge second-variation faces cite it to erase the notational seam. The proof is pure reflexivity.
Claim. For every real $4\times 4$ matrix $H$, the continuum Frobenius square $\sum_{i,j} H_{ij}^2$ equals the Frobenius norm-squared $\|H\|_F^2$ (the same double sum under the Regge-side name).
background
Arc 2, step 7 of the gravity analysis derives Regge's classical normalization $\rho$ by placing two second-variation faces side by side. From the Levi-Civita connection alone, the continuum module obtains the phase-averaged Einstein–Hilbert face
$$\mathrm{ehFace},H,k = -\tfrac14,|k|^2,|H|_F^2$$
on a real transverse-traceless cosine wave, with no Regge imports.
To keep that isolation, the continuum side defines its own frobSq as $\sum_{i,j} H_{ij}^2$. The Regge and preflight modules use the identical double sum under the name frobeniusNormSq. Both are ordinary real Frobenius squares on Mat4; neither involves the complex two-qubit variant. This lemma is the definitional bridge that lets later rewrites mix the two vocabularies without smuggling Regge assumptions into the continuum derivation.
proof idea
One-line reflexivity. Both sides expand to the same term $\sum_{i:\mathrm{Fin},4}\sum_{j:\mathrm{Fin},4} H_{ij}\cdot H_{ij}$, so rfl closes the goal. No algebraic lemmas are needed.
why it matters
Without this bridge, every comparison between the continuum EH face and the discrete Regge face would carry a notational tax. Downstream, reggeFace_eq rewrites through it to obtain $\mathrm{reggeFace},\rho,H,k = -(\rho/4),|H|_F^2,|k|^2$; lagrangian_route_same_face uses it when showing the Lagrangian density averages to ehFace; and the two face-identification theorems (frozen_preflight_is_the_eh_integral_face, exact_unit_coefficient_is_the_regge_face) rely on a single shared $|H|_F^2$ so that the factor-of-two gap can be read cleanly as Regge's $\rho=1/2$ rather than as a computational error.
In the module narrative this is bookkeeping that makes A4 (the fourth classical input) checkable: the historical gate failed because the two sides varied different functionals, not because either coefficient was wrong. The lemma itself is not a forcing-chain step (T0–T8); it is local glue inside the 4D Regge–continuum dictionary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.