Gravity Einstein Hilbert Action

The action and its variation

The Einstein-Hilbert action is the starting point for deriving general relativity from a principle of least action. It is a single number assigned to a region of spacetime, written as S = (1/2κ) ∫ R √(-g) d⁴x, where R is the Ricci scalar curvature, g is the determinant of the metric tensor, and κ is the Einstein gravitational constant. The action measures how much spacetime is curved in the region. The central idea is that the physically realized spacetime is the one that makes this number stationary, meaning a small change in the metric produces no first-order change in the action.

This variational principle has a precise history. The action is named for David Hilbert, who in 1915, nearly simultaneously with Albert Einstein, showed that varying it with respect to the metric yields the Einstein field equations. The result is that the variation of S with respect to the inverse metric g^{μν} is proportional to the Einstein tensor G_{μν}. Setting the variation to zero gives the vacuum field equations G_{μν} = 0, which describe gravity in the absence of matter. This is the classical result that the framework's machine-checked library of formal theorems reproduces.

In Recognition Science, the framework models this classical derivation as a formal theorem rather than an axiom. Its library proves that the Lagrangian density (the integrand of the action) vanishes for flat spacetime, where R = 0, and that it is proportional to the scalar curvature. The library also proves the key structural facts: the Hilbert variation holds for Minkowski spacetime, the Einstein tensor is symmetric, and it vanishes for the flat metric. These are gathered in a certificate structure that bundles the results into a single machine-checked object.

The framework's library proves the flat-spacetime cases and the proportionality facts, but it does not yet fully formalize the complete variation chain. The steps requiring the full covariant derivative, the Palatini identity and the integration of total divergence terms, remain open in the formal library. The framework has proved that stationarity of the action is equivalent to the vacuum field equations for the cases it handles, and it has certified the flat solution, but the general proof that the variation of the action yields the Einstein tensor for arbitrary metrics is not yet in the machine-checked library.

/-- The Einstein-Hilbert action density at a point (before spatial integration):
    L_EH = (1/2kappa) * R * sqrt(-det g)

    We represent this as a function of the scalar curvature and determinant. -/
noncomputable def eh_lagrangian_density (R_scalar det_g kappa : ℝ) : ℝ :=
  R_scalar * Real.sqrt (|det_g|) / (2 * kappa)

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

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

/-- The EH lagrangian density is proportional to the scalar curvature. -/
theorem eh_proportional_to_R (R1 R2 det_g kappa : ℝ)
    (hk : 0 < kappa) (hd : 0 < |det_g|) :
    eh_lagrangian_density R1 det_g kappa / eh_lagrangian_density R2 det_g kappa = R1 / R2 := by
  simp [eh_lagrangian_density]
  have hsd : 0 < Real.sqrt (|det_g|) := Real.sqrt_pos.mpr hd
  have h2k : 0 < 2 * kappa := by linarith
  field_simp [ne_of_gt hsd, ne_of_gt h2k]

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 complete variation chain for arbitrary metrics is not yet proved in the framework's library. The framework does not derive the value of the cosmological constant Λ from this action. The framework does not claim that the Palatini identity is proved; it is stated as a structural proposition.

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: