IndisputableMonolith.Gravity.EinsteinHilbertAction
The module encodes the Einstein-Hilbert action density for Recognition Science gravity derivations. It defines L_EH pointwise from scalar curvature R and metric determinant, importing the Levi-Civita connection and Ricci tensor. Workers recovering classical GR from the RS forcing chain cite these objects. The module supplies the density function plus flat-space and variation lemmas.
claim$L_{EH} = \frac{1}{2\kappa} R \sqrt{-\det g}$, expressed as a function of scalar curvature and metric determinant in local coordinates.
background
The module belongs to the Gravity domain. It imports the RS time quantum from Constants, the coordinate-patch Levi-Civita connection from Connection (avoiding Mathlib manifold gaps), and the Ricci tensor, scalar curvature, and Einstein tensor from RicciTensor. RicciTensor proves the Einstein tensor is symmetric and divergence-free. The module then introduces the action density per its documentation.
proof idea
This is a definition module. It introduces eh_lagrangian_density together with supporting lemmas eh_flat, eh_proportional_to_R, hilbert_variation_holds, and palatini_identity that relate the density to curvature and verify structural identities.
why it matters in Recognition Science
The module supplies the variational starting point for Einstein equations inside the RS framework. It fills the classical GR action step that connects to the T0-T8 forcing chain and the eight-tick octave through curvature scalars. No downstream theorems are listed yet.
scope and limits
- Does not integrate the density over spacetime.
- Does not include matter or cosmological terms.
- Does not derive kappa from RS constants.
- Does not address global topology or singularities.