Gravity Einstein Hilbert Action Hilbert Variation Flat

The flat vacuum check

The Einstein-Hilbert action is the starting point for deriving general relativity from a principle. It assigns a number to a spacetime geometry, the integral of the scalar curvature over the volume, and the field equations come from asking which geometry makes that number stationary. In the standard form, the action is S = (1/2κ) ∫ R √(-g) d⁴x, where R is the scalar curvature, g is the metric determinant, and κ couples geometry to matter. The variation of this action with respect to the metric yields the Einstein tensor G_μν, and setting the variation to zero gives the vacuum field equations G_μν = 0.

Hilbert derived this variational principle in 1915, months after Einstein published the field equations from a different route. The action approach has since become the standard way to think about gravity as a geometric theory, and it extends naturally to include matter and a cosmological constant. The key step in the variation is the Palatini identity, which handles the variation of the Ricci tensor, and the Jacobi formula, which handles the variation of the metric determinant. These are classical results, taught in every graduate course on general relativity.

In Recognition Science, the framework's machine-checked library of formal theorems contains a small result called hilbert_variation_flat. It proves that for Minkowski spacetime, the flat empty geometry of special relativity, the vacuum field equations hold. In plain language, the theorem states that a spacetime with zero curvature and no matter satisfies Einstein's equations with zero cosmological constant. This is a consistency check, not a new physical prediction. The library also proves that the Einstein-Hilbert Lagrangian density vanishes when the scalar curvature is zero, which is the flat spacetime case, and that the Einstein tensor is symmetric and vanishes for Minkowski spacetime.

The flat check matters because it anchors the variational principle to the simplest known solution. Any proposed action that did not admit flat empty spacetime as a stationary point would be suspect. The library's certificate bundles these checks together: the flat variation holds, the Lagrangian vanishes for zero curvature, and the Einstein tensor is symmetric and zero for Minkowski. What the declaration does not claim is the full Hilbert variation for general curved spacetimes. The complete chain, including the Palatini identity with a real connection, remains open in the library. The flat case is proved; the general case is a target.

/-- For flat spacetime, the Hilbert variation is satisfied. -/
theorem hilbert_variation_flat :
    hilbert_variation_holds minkowski minkowski_inverse
      (fun _ _ _ => 0) (fun _ _ _ _ => 0) :=
  minkowski_is_vacuum_solution

/-- The EH lagrangian density vanishes for flat spacetime (R = 0). -/
theorem eh_flat (det_g kappa : ℝ) (hk : kappa ≠ 0) :
    eh_lagrangian_density 0 det_g kappa = 0 := by
  simp [eh_lagrangian_density]

What this page does not claim

The full Hilbert variation for general curved spacetimes is not proved in this declaration. The Palatini identity is not proved; it is stated as a structural proposition with a vacuous body. The framework does not derive the Einstein field equations from the action here; it only checks the flat case.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/EinsteinHilbertAction.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: