eh_flat
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not treat the variation of the action in curved spacetime.
- Does not include a cosmological constant term.
- Does not derive the numerical value of κ from the phi ladder.
- Does not address matter coupling or non-vacuum sources.
formal statement (Lean)
48theorem eh_flat (det_g kappa : ℝ) (hk : kappa ≠ 0) :
49 eh_lagrangian_density 0 det_g kappa = 0 := by
proof body
Term-mode proof.
50 simp [eh_lagrangian_density]
51
52/-- The EH lagrangian density is proportional to the scalar curvature. -/