eh_action_minkowski
plain-language theorem explainer
Einstein-Hilbert action on Minkowski spacetime evaluates to zero for any Planck mass squared and volume element. Researchers checking flat-space limits of gravitational dynamics or verifying action consistency in vacuum would cite this identity. The argument substitutes the action definition, rewrites the discrete integral as a finite sum, and reduces the sum to zero via the vanishing Ricci scalar on the Minkowski metric.
Claim. $S_{EH}(g, M_P^2, vol) = 0$ where $S_{EH}$ is the Einstein-Hilbert action $(M_P^2/2)∫√(-g) R d^4x$, $g$ is the Minkowski metric tensor, and $vol$ is the discrete volume element with grid spacing.
background
The module supplies discrete volume integration over spacetime with the √(-g) measure for the Einstein-Hilbert action. VolumeElement is the structure carrying grid spacing for uniform sampling of d⁴x. The action itself is defined as (M_P²/2) times the scalar integral of the Ricci scalar. Upstream, minkowski_ricci_scalar_zero states that the Ricci scalar vanishes identically on Minkowski space by unfolding the curvature definitions and summing constants to zero.
proof idea
Term-mode proof. It unfolds the action definition and integrate_scalar, then invokes Finset.sum_eq_zero. The remaining goal is discharged by showing each summand vanishes after substituting the zero Ricci scalar on the Minkowski tensor.
why it matters
The result supplies the expected zero value of the gravitational action in flat spacetime and serves as a base case for the discrete integration machinery. It depends directly on the upstream vanishing of the Ricci scalar and the definition of the Einstein-Hilbert action. Within the Recognition framework it confirms that zero curvature produces zero action contribution, consistent with the forcing chain steps that derive spatial dimensions and curvature from the J-functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.