Gravity Einstein Hilbert Action Hilbert Variation Holds

The Hilbert variation

The Einstein-Hilbert action is the starting point for deriving Einstein's field equations from a variational principle. In general relativity, the action is written as S = (1/2κ) ∫ R √(-g) d⁴x, where R is the scalar curvature, g is the determinant of the metric tensor, and κ is the coupling constant. The principle states that the physical spacetime metric is the one that makes this action stationary: the variation of S with respect to the inverse metric must vanish. In 1915, Albert Einstein and David Hilbert independently arrived at the field equations, and Hilbert's derivation used exactly this variational approach, which is why it carries his name.

When you vary the action with respect to the inverse metric g^μν, the result is δS/δg^μν = -(1/2κ) G_μν √(-g), where G_μν is the Einstein tensor. Setting this variation to zero gives the vacuum field equations G_μν = 0 (with cosmological constant Λ = 0). The Einstein tensor is defined as G_μν = R_μν - (1/2)R g_μν, built from the Ricci tensor R_μν and the scalar curvature R. This is the standard result that appears in every textbook on general relativity.

In Recognition Science, the machine-checked library of formal theorems contains a declaration called hilbert_variation_holds. This declaration defines a proposition: it states that the vacuum Einstein field equations hold for a given metric, inverse metric, connection coefficients, and their derivatives. The library proves that this proposition holds for flat spacetime, meaning the Minkowski metric satisfies the vacuum equations. The library also proves several supporting facts: the action density vanishes for flat spacetime, the action density is proportional to the scalar curvature, and the Einstein tensor is symmetric when the Ricci tensor is symmetric.

The library assembles these results into a certificate structure called HilbertVariationCert. This certificate bundles four proved statements: flat spacetime satisfies the Hilbert variation, the action density vanishes when curvature is zero, the Einstein tensor is symmetric under the appropriate condition, and the Einstein tensor is zero for Minkowski spacetime. Each of these is a proved theorem in the library, not an assumption. However, the full variational derivation, including the Palatini identity for the variation of the Ricci tensor and the integration by parts that eliminates boundary terms, is stated as a structural proposition but not fully formalized. The library's docstring says steps 1, 2, and 5 of the derivation are proved, while steps 3 and 4 require the full covariant derivative infrastructure that is not yet in place.

What does this establish in plain language? The declaration hilbert_variation_holds is a formal definition of what it means for the Hilbert variation to hold: namely, that the vacuum Einstein field equations are satisfied. The library proves that flat spacetime is one such solution. It does not prove that the variation of the action yields the Einstein tensor for arbitrary curved spacetimes; that full derivation remains incomplete. The certificate collects the proved pieces, which include the flat case and symmetry properties, but the general variational principle, the heart of Hilbert's derivation, is not yet a proved theorem in the library.

The practical consequence is modest but real: within the framework, the vacuum field equations are known to hold for the simplest spacetime, Minkowski space, and the action density has the expected algebraic properties. The general derivation from the action to the field equations, which is the content of Hilbert's 1915 paper, remains a target for formalization rather than a completed proof. This matters because it shows the boundary of what the framework currently certifies: the flat-space solution is established, but the full variational principle that generates the field equations for all spacetimes is not yet in the machine-checked library.

/-- **HILBERT VARIATIONAL PRINCIPLE (Axiom 2 Proved)**

    The variation of the Einstein-Hilbert action with respect to
    the inverse metric g^{mu nu} yields the Einstein tensor:

    delta S_EH / delta g^{mu nu} = -(1/2kappa) G_{mu nu} sqrt(-g)

    This is proved by the following chain:
    1. delta(R sqrt(-g)) = (R_{mu nu} - (1/2) R g_{mu nu}) sqrt(-g) delta g^{mu nu}
                           + (total divergence terms)
    2. The total divergence integrates to zero on a compact region
       (or vanishes at infinity with appropriate fall-off)
    3. Therefore delta S_EH = (1/2kappa) G_{mu nu} sqrt(-g) delta g^{mu nu}

    We formalize this as: stationarity of S_EH (delta S = 0) is equivalent
    to G_{mu nu} = 0 (for all delta g^{mu nu}). -/
def hilbert_variation_holds (met : MetricTensor) (ginv : InverseMetric)
    (gamma : Idx → Idx → Idx → ℝ)
    (dgamma : Idx → Idx → Idx → Idx → ℝ) : Prop :=
  vacuum_efe_coord met ginv gamma dgamma 0

/-- 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]

theorem hilbert_variation_cert : HilbertVariationCert where
  flat_ok := hilbert_variation_flat
  eh_flat := eh_flat
  einstein_symmetric := RicciTensor.einstein_symmetric
  einstein_flat := RicciTensor.einstein_flat

What this page does not claim

The full Hilbert variational principle for general spacetimes is not proved; only the flat spacetime case is established. The Palatini identity is stated as a structural proposition, not proved. The derivation steps involving the covariant derivative and integration by parts are not formalized.

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: