IndisputableMonolith.Gravity.EinsteinHilbertAction
The module formalizes the Einstein-Hilbert action density in the Recognition Science gravity sector as a function of scalar curvature and metric determinant. Physicists deriving variational field equations from the RS functional equation would cite these definitions and lemmas. The module supplies the Lagrangian together with flat-space reductions and variation identities built directly on the imported connection and Ricci primitives.
claimThe Einstein-Hilbert Lagrangian density is $L_{EH} = (1/2κ) R √(-det g)$, where $R$ denotes scalar curvature obtained from the Ricci tensor and $g$ is the metric tensor on a local coordinate patch.
background
This module sits inside the gravity domain and imports the RS time quantum τ₀ = 1 tick from Constants, the Levi-Civita connection expressed in local coordinates R⁴ → R^{4×4} from Connection, and the Ricci tensor together with the symmetric divergence-free Einstein tensor from RicciTensor. These imports supply the curvature quantities needed to write the action density without invoking Mathlib manifolds. The local theoretical setting is a smooth metric on a coordinate patch, allowing direct algebraic manipulation of Christoffel symbols, Riemann tensor, and scalar curvature.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the variational starting point for gravity within Recognition Science, feeding the sibling results on Hilbert variation and Palatini identity that support derivation of the Einstein equations. It closes the link between the connection and Ricci primitives and the action principle, consistent with the framework's derivation of D = 3 and the RS-native constants.
scope and limits
- Does not integrate the density over a spacetime volume.
- Does not incorporate matter Lagrangians or a cosmological term.
- Does not address quantization or higher-curvature corrections.
- Does not prove equivalence to the Palatini formulation.