Gravity Einstein Hilbert Action Jacobi Variation Structural

The Jacobi variation

The Einstein-Hilbert action is a central object in general relativity: a single integral, S = (1/2κ) ∫ R √(−g) d⁴x, that encodes the entire gravitational field. The idea, due to Hilbert in 1915, is that the actual geometry of spacetime is the one that makes this action stationary under small changes of the metric. Varying the action with respect to the inverse metric g^μν gives the Einstein tensor G_μν; setting that variation to zero yields the vacuum field equations G_μν = 0.

One step in that variation is the Jacobi formula, which tells how the volume element √(−g) changes when the metric changes. The framework's declaration jacobi_variation_structural formalizes a very thin slice of this step. In the machine-checked library of formal theorems, it states that for any metric tensor, the variation of the metric with respect to itself is trivial: the metric equals itself. That is a tautology, proved by reflexivity, and it acts as a placeholder for the full Jacobi identity that would connect the variation of the determinant to the metric variation.

In Recognition Science, this declaration does not establish the full Hilbert variation. The library's own documentation is explicit: the complete chain, from the action to the Einstein tensor, requires the Palatini identity and the variation of the Ricci tensor, steps that depend on the covariant derivative and connection infrastructure. Those steps are not yet formalized. What is proved is the flat-spacetime case: the Minkowski metric satisfies the vacuum equations, the Lagrangian density vanishes when the scalar curvature is zero, and the Einstein tensor is symmetric and vanishes for flat spacetime. Those results are assembled in a certificate structure, HilbertVariationCert, which the library presents as the current extent of the Hilbert variation theorem.

What the declaration does not claim is therefore as important as what it claims. It does not assert that the Jacobi formula for determinants is proved, nor that the full variational principle is established for general metrics. The structural tautology is a bookkeeping device, not a derivation. A reader who sees jacobi_variation_structural and expects the complete Hilbert variation would be misled. The honest summary is that the framework has proved the flat case and the algebraic properties of the Einstein tensor, while the general variational chain remains open.

theorem jacobi_variation_structural (met : MetricTensor) :
    jacobi_variation met := fun _ _ => rfl

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 Jacobi formula for determinants is not proved by jacobi_variation_structural. The full Hilbert variational principle for general metrics is not established. No claim is made that the Einstein-Hilbert action is derived from Recognition Science first principles.

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: