eh_lagrangian_density
plain-language theorem explainer
This definition supplies the pointwise Einstein-Hilbert Lagrangian density as R times the square root of the absolute metric determinant, divided by twice the coupling kappa. Researchers deriving the Einstein equations from the variational principle cite it when building the action integral in the Recognition Science gravity module. It is realized as a direct one-line algebraic expression with no auxiliary lemmas.
Claim. The Einstein-Hilbert Lagrangian density at a spacetime point is $L_{EH}(R, g, k) = R / (2k) * sqrt(|det g|)$, where $R$ is the scalar curvature, $det g$ the determinant of the metric, and $k$ the coupling constant.
background
The module defines the Einstein-Hilbert action as the spacetime integral of the Lagrangian density, $S_{EH}[g] = (1/(2k)) integral R sqrt(-g) d^4x$, and shows that its metric variation yields the Einstein tensor, thereby proving Axiom 2. The scalar curvature enters via the Ricci contraction defined in the RicciTensor module, while the volume factor uses the absolute determinant of the metric. Kappa is treated as a free real parameter here, though upstream definitions in AnnularCost and ThermalConductivityRegimesFromPhiLadder set it to (log phi)^2 or phi^k, consistent with RS-native units where G scales as phi^5 / pi.
proof idea
This is a direct definition whose body is the expression R_scalar * Real.sqrt (|det_g|) / (2 * kappa). No tactics or lemmas are invoked; the implementation simply transcribes the standard formula into Lean reals.
why it matters
The definition anchors the HilbertVariationCert structure, which records that the action variation produces G_mu nu sqrt(-g) / (2 kappa) and thereby recovers the vacuum Einstein equations. It feeds the sibling theorems eh_flat (vanishing on Minkowski) and eh_proportional_to_R (linearity in R). Within the framework it embeds the Einstein-Hilbert principle inside the T0-T8 forcing chain, with kappa ultimately traceable to the phi-ladder and the eight-tick octave. The module leaves the full Palatini identity for the covariant derivative terms as an open implementation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.