reggeFace_eq
plain-language theorem explainer
The Regge-normalized continuum second-variation face equals -(ρ/4) times the product of the squared Frobenius norm of the metric perturbation H and the squared wave-norm of momentum k. Gravity analysts matching discrete Regge actions to continuum Einstein-Hilbert faces cite this algebraic identity. The proof unfolds the two face definitions, rewrites the scalar factors, and closes by ring.
Claim. For every real normalization constant $\rho$, every $4\times 4$ real matrix $H$, and every four-component real wave vector $k$, the Regge-normalized continuum face equals $-(\rho/4)$ times the squared Frobenius norm of $H$ times the squared wave-norm of $k$.
background
From the continuum second-variation analysis, the phase average of $d^2/dt^2\int R\sqrt{g}$ per unit volume on a real transverse-traceless cosine wave is the Einstein-Hilbert face
$$\mathrm{ehFace}(H,k)=-(1/4),|k|^2,|H|_F^2,$$
derived from the Levi-Civita connection alone, with no Regge input.
This module leaves Regge's normalization free: the discrete action $\sum_h A_h\delta_h$ is related to the continuum integral by $\sum_h A_h\delta_h=\rho\cdot\int R\sqrt{g}$, historically $\rho=1/2$. The Regge face is that continuum face scaled by $\rho$. Four-component wave vectors are just maps $\mathrm{Fin},4\to\mathbb{R}$. The two scalar building blocks are the squared Frobenius norm of $H$ and the squared wave-norm of $k$; sibling equalities identify those with the expressions inside the face definitions.
proof idea
Short term proof. Unfold the Regge face and the underlying Einstein-Hilbert face to expose the product of $\rho$ with the continuum expression. Rewrite the Frobenius and momentum scalar factors by the two sibling equalities that name those squares. The remaining polynomial identity is discharged by ring.
why it matters
Local algebraic engine for the rest of the module. Downstream P2 substitutes Regge's normalization and shows the derived face equals the banked dictionary $m^2$ moment exactly, with no residual. Downstream P3 uses the same identity to force $\rho=1/2$ from 1,208 discrete Heron/Gram rows (a check that could have failed). The discrimination theorem refutes $\rho=1$ at a concrete TT witness by the same rewrite.
In the Arc 2 story this is step 7, second half: the factor of two between the continuum dictionary value $-(1/8)$ and the frozen preflight $-(1/4)$ is exactly $1/\rho$. Both numbers are correct faces of different actions; the historical gate failed because the two sides varied different functionals, not because the Regge computation was wrong.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.