IndisputableMonolith.Gravity.EinsteinHilbertAction
The module defines the Einstein-Hilbert action density for Recognition Science gravity models. It expresses L_EH as a function of scalar curvature R and metric determinant, importing the Levi-Civita connection and Ricci definitions. Researchers deriving field equations from variational principles in the RS framework would cite it. The module acts as a container for definitions and lemmas with no proofs inside.
claim$L_{EH} = (1/(2κ)) R √(-det g)$, represented as a function of the scalar curvature and the metric determinant.
background
The module sits in the Gravity domain and imports the RS time quantum τ₀ = 1 tick. The Connection module formalizes the Levi-Civita connection in local coordinates where the metric is a smooth map from R^4 to R^{4×4}, avoiding Mathlib abstract manifold gaps. The RicciTensor module defines the Ricci tensor, scalar curvature, and Einstein tensor from the Riemann tensor while proving symmetry and the divergence-free property.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the action density used in variational calculations for gravity. It supports sibling results on Hilbert variation and Jacobi variation within the same module. It links the standard GR action form to RS constants and curvature identities from the imported modules.
scope and limits
- Does not integrate the density over spacetime.
- Does not derive the Einstein field equations from variation.
- Does not incorporate phi-ladder or RS-specific corrections to the action.
- Does not address coordinate invariance beyond local patches.