reggeNormalization
plain-language theorem explainer
Regge's classical normalization constant ρ = 1/2, relating the discrete hinge action Σ_h A_h δ_h to the continuum Einstein-Hilbert integral via Σ_h A_h δ_h = ρ ∫ R √g. Gravity analysts matching continuum TT second variations to discrete Regge faces cite it as the fixed scale between those functionals. It is a bare real definition; later theorems force and independently check the value.
Claim. The Regge normalization constant is the real number $\rho = 1/2$, so that the discrete Regge action and the continuum Einstein-Hilbert integral are related by $\sum_h A_h \delta_h = \frac{1}{2} \int R \sqrt{g}$.
background
Arc 2, step 7 (second half) of the 4D gravity analysis. From the Levi-Civita connection alone, with no Regge input, the continuum module shows that the phase-averaged second variation of $\int R \sqrt{g}$ per unit volume on a real transverse-traceless cosine wave is $\mathrm{ehFace}, H, k = -\frac{1}{4}, |k|^2, |H|_F^2$.
The discrete object is the Regge action $\sum_h A_h \delta_h$ (area times deficit angle). That functional is not identical to $\int R \sqrt{g}$; classically one writes $\sum_h A_h \delta_h = \rho \cdot \int R \sqrt{g}$. This module leaves $\rho$ free at first, then shows the banked dictionary forces $\rho = 1/2$, refutes the frozen preflight choice $\rho = 1$, and checks $\rho = 1/2$ against Gauss-Bonnet on two triangulated spheres.
The factor of two between the continuum face $-1/8$ and the frozen $-1/4$ is exactly this normalization: both numbers are correct faces of different actions. The discrete bookkeeping factor $2$ is $1/\rho$.
proof idea
Literal definition: the constant is fixed to the real value $1/2$. No lemmas, no tactics. Downstream theorems unfold this definition and combine it with the continuum face formula, the dictionary $m^2$ identity, and the Gauss-Bonnet sphere check.
why it matters
Pins the scale that reconciles continuum Einstein-Hilbert second variation with the discrete Regge face in 4D. Downstream, reggeFace_eq_dictionary shows that at this $\rho$ the derived continuum face equals the banked midpoint Bloch $m^2$ moment exactly for every TT pair $(H,k)$. discreteBookkeepingFactor_is_inverse_regge records that the historical factor $2$ is simply $1/\rho$. exact_unit_coefficient_is_the_regge_face identifies the banked $-1/8$ as the face of the discrete action. regge_constant_from_gauss_bonnet checks $4\pi = \rho \cdot 8\pi$ on spheres. The compound gate NormalizationGateDischarged packages equality at $\rho=1/2$, uniqueness of that $\rho$, and refutation of $\rho=1$. Geometric fold and SRS convergence modules consume the same constant when placing the Regge face between continuum and dictionary faces. Closes Arc 2 step 7: 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.