sphereEHIntegral
plain-language theorem explainer
The Einstein-Hilbert integral ∫R√g on the 2-sphere equals 8π, via Gauss-Bonnet (∫K√g = 4π) and R = 2K. Gravity analysts cite it when matching discrete Regge deficit sums to continuum curvature for the normalization constant ρ. The body is a pure numerical abbreviation of that value.
Claim. On the unit 2-sphere, the Einstein-Hilbert integral $\int R\sqrt{g}\,dA$ equals $8\pi$. This follows from Gauss-Bonnet $\int K\sqrt{g}\,dA = 2\pi\chi = 4\pi$ together with the two-dimensional identity $R = 2K$.
background
This module derives Regge's normalization without assuming it. Continuum second variation of ∫R√g on a transverse-traceless cosine wave yields ehFace = −(1/4)|k|²‖H‖²_F. The discrete Regge action is Σ_h A_h δ_h, related by Σ A_h δ_h = ρ · ∫R√g, historically with ρ = 1/2.
Gauss-Bonnet on closed surfaces supplies an independent check. The hinge deficit is 2π − Σθ (DihedralAngle / Schläfli). Both reference polyhedra give total deficit sum 4π. On the continuum side, χ(S²) = 2 so ∫K√g = 4π, and in two dimensions R = 2K, hence ∫R√g = 8π.
This definition packages that continuum target value for the comparison.
proof idea
Definitional constant only. The right-hand side is written 2 · (2π · 2), which expands to 8π and encodes the product of the curvature factor R = 2K with the Gauss-Bonnet integral 4π. No lemmas, tactics, or algebraic reduction beyond the arithmetic abbreviation.
why it matters
Feeds regge_constant_from_gauss_bonnet, which states 4π = ρ · sphereEHIntegral and thereby forces ρ = 1/2 once the polyhedral deficit sum is 4π. Also feeds gauss_bonnet_refutes_rho_one: ρ = 1 would demand deficit sum 8π, contradicting both polyhedra. Together these close Arc 2 step 7's independent Gauss-Bonnet check that the historical gate mismatch was a functional mismatch (Regge vs Einstein-Hilbert), not a computational error. Downstream NormalizationGateDischarged packages the discharged ρ = 1/2 gate for the discrete bookkeeping factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.