einstein_hilbert_action
plain-language theorem explainer
The Einstein-Hilbert action is defined as half the squared Planck mass times the discrete integral of the Ricci scalar over spacetime volume. Researchers deriving gravitational dynamics within the Recognition Science metric framework would cite this when evaluating the action or taking flat-space limits. The definition is a direct one-line composition of the integrate_scalar routine applied to the pointwise Ricci scalar.
Claim. The Einstein-Hilbert action is given by $ (M_P^2 / 2) $ times the integral of the Ricci scalar $R$ over spacetime, using the metric measure $d^4x$ supplied by the volume element.
background
The module supplies discrete volume integration on spacetime with the metric determinant factor. MetricTensor is the local symmetric bilinear form on four-dimensional spacetime points. VolumeElement encodes the uniform grid spacing for the discrete four-volume approximation. integrate_scalar performs a finite sum that approximates the integral of any scalar function weighted by the volume measure. ricci_scalar returns the trace $g^{mu nu} R_{mu nu}$ computed from the metric.
proof idea
This is a one-line wrapper that scales the Planck mass squared by one half and feeds the Ricci scalar function into the integrate_scalar integrator together with the metric and volume element.
why it matters
This definition supplies the pure gravitational term whose Minkowski specialization yields the vanishing-action theorem eh_action_minkowski. It bridges the curvature scalar produced by ricci_scalar to the integrated dynamics required by the Relativity.Fields layer. In the Recognition Science chain it supports the geometric side of the forcing sequence leading to D=3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.