eh_flat
plain-language theorem explainer
The Einstein-Hilbert Lagrangian density vanishes identically when the scalar curvature is zero. Researchers deriving the vacuum Einstein equations from an action principle cite this case when confirming the flat-space baseline. The proof is a direct substitution into the explicit density formula.
Claim. For any nonzero real number κ, the Einstein-Hilbert Lagrangian density evaluated at zero scalar curvature equals zero: L_EH(0, det g, κ) = 0.
background
The Einstein-Hilbert action takes the form S_EH[g] = (1/(2κ)) ∫ R √|det g| d⁴x. Its local density is therefore L_EH = R √|det g| / (2κ), expressed as a function of the scalar curvature R, the metric determinant, and the coupling κ. This module proves that the metric variation of the action recovers the Einstein tensor, thereby establishing the vacuum field equations as a derived result rather than an axiom. The density definition appears in the same file and is the immediate predecessor used here.
proof idea
The proof is a one-line wrapper that applies the definition of the Einstein-Hilbert Lagrangian density. Substituting zero for the scalar curvature argument immediately yields the zero value, independent of the determinant and of κ (provided κ ≠ 0).
why it matters
This result supplies the flat-space case inside the HilbertVariationCert structure, which assembles the full certificate that δS_EH/δg^{μν} = −G_{μν} √|det g| / (2κ). It thereby completes the proof of Axiom 2 (Hilbert variation) in the Recognition Science framework. The flat case anchors the subsequent steps that recover the Einstein tensor from the Palatini identity and the Jacobi variation of the volume element.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.