reggeFace
plain-language theorem explainer
Scales the derived Einstein-Hilbert second-variation face by a free real ρ, giving the continuum face that the discrete Regge Hessian must match when Σ_h A_h δ_h = ρ ∫ R √g. Gravity analysts cite it when pinning Regge's normalization and discharging the historical factor-of-two gate. Body is the one-line product ρ · ehFace.
Claim. For $\rho \in \mathbb{R}$, a $4\times 4$ metric perturbation $H$, and four-momentum $k$, the Regge-side continuum face is $\rho$ times the derived Einstein-Hilbert face: $\mathrm{reggeFace}(\rho,H,k) := \rho \cdot \mathrm{ehFace}(H,k)$, where $\mathrm{ehFace}(H,k) = -\frac14 |k|^2 \|H\|_F^2$ is the phase-averaged second variation of $\int R\sqrt{g}$ per unit volume on a real transverse-traceless cosine wave.
background
Arc 2, step 7 of the gravity analysis compares two second-variation faces of curvature actions on the same transverse-traceless (TT) cosine waves in 4D. Upstream, ContinuumTTSecondVariation4D derives from the Levi-Civita connection alone that the phase average per unit volume of $d^2/dt^2 \int R\sqrt{g}$ is
$$\mathrm{ehFace}(H,k) = -\tfrac14 , |k|^2 , |H|_F^2.$$
The discrete side is the Regge action $\sum_h A_h \delta_h$ (area times deficit), not $\int R\sqrt{g}$. Classical input A4 writes $\sum_h A_h \delta_h = \rho \cdot \int R\sqrt{g}$ with $\rho$ free; historically $\rho = 1/2$. Wave vectors are maps $k : \mathrm{Fin},4 \to \mathbb{R}$. This definition simply multiplies the continuum EH face by that free scale so the two sides can be compared without assuming the classical value of $\rho$.
proof idea
Definitional one-liner: unfold to $\rho$ times the upstream ehFace. No tactics, no lemmas. Downstream equalities (reggeFace_eq, etc.) expand ehFace via the Frobenius and momentum-square identities and simplify by ring.
why it matters
Carries A4 into the comparison algebra. With $\rho$ left free, the module pins $\rho = 1/2$ against the banked dictionary $m^2$ moment (regge_normalization_pinned, reggeFace_eq_dictionary), shows the banked $-1/8$ is exactly the discrete-action face (exact_unit_coefficient_is_the_regge_face), and packages the discharge of the historical normalization gate (NormalizationGateDischarged), including the refutation that $\rho = 1$ fails on the witness. Downstream geometric-fold work uses it to place the Regge face strictly between two continuum moments (reggeFace_between). The factor of two between continuum $-1/4$ and discrete $-1/8$ is thereby identified as $1/\rho$, not an error in either Hessian. Independent Gauss-Bonnet checks on triangulated spheres (§6) sit outside this def but close the same arc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.