reggeFace_eq_dictionary
plain-language theorem explainer
At Regge's normalization, the continuum face of the Regge action equals the banked dictionary m² moment exactly, for every transverse-traceless H and every wave momentum k. Gravity analysts matching discrete Regge calculus to continuum second variations cite this as the exact bridge (P2). The proof expands both sides to multiples of |k|² times the Frobenius norm squared and closes by ring.
Claim. For every $4\times 4$ real matrix $H$ and every four-momentum $k\in\mathbb{R}^4$, if $H$ is transverse-traceless with respect to $k$, then the continuum face of the Regge action evaluated at Regge's normalization constant equals the exact-midpoint Bloch $m^2$ dictionary moment of $(H,k)$. Both sides agree with no residual factor and no tolerance.
background
This module sits in Arc 2, step 7 of the 4D gravity analysis. Independently of any Regge input, the continuum TT second variation shows that the phase average of $d^2/dt^2\int R\sqrt{g}$ per unit volume on a real transverse-traceless cosine wave is
$$\mathrm{ehFace}(H,k)=-(1/4),|k|^2,|H|_F^2.$$
The discrete object is the Regge action $\sum_h A_h\delta_h$ (area times deficit). Regge's classical normalization asserts $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$ with $\rho=1/2$; this module leaves $\rho$ free and measures it against the banked dictionary. The dictionary side of the comparison is the exact-midpoint Bloch $m^2$ moment, known upstream to equal $-(1/8),|k|^2,|H|_F^2$ on TT modes.
Here $k$ is a four-component real wavevector (Wave4), and $H$ is constrained by the transverse-traceless predicate. The two faces therefore differ by a pure constant; that constant is Regge's $\rho$.
proof idea
Term-mode algebraic reduction in three steps. First rewrite the dictionary side by the upstream identity that the exact-midpoint Bloch $m^2$ moment equals $-\tfrac18$ times the TT Frobenius form. Second expand the Regge face via the in-module face-equality lemma, which expresses it as a multiple of the same Frobenius scalar involving the free normalization constant. Third unfold that constant and finish with ring, which cancels the numerical prefactors and yields exact equality.
why it matters
This is proposition P2 of the Regge-normalization arc: at the classical value of $\rho$, the derived continuum face and the banked dictionary moment coincide with no residual. Downstream, normalizationGateDischarged packages the equality as the first witness that the historical normalization gate is discharged rather than failed; the gate failed only because the two sides were varying different functionals (Regge vs Einstein-Hilbert), not because either computation was wrong. The geometric-fold comparison also rewrites through this identity to place the Regge face strictly between two dictionary moments, which is the content of the two-step decomposition. In framework terms the result pins the discrete-to-continuum bookkeeping factor $1/\rho=2$ as a derived constant, clearing the path for P3 (dictionary forces $\rho=1/2$) and the independent Gauss-Bonnet checks on triangulated spheres.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.