integrate_scalar
plain-language theorem explainer
The definition supplies a discrete 10-point grid approximation to the spacetime volume integral of a scalar function weighted by the metric factor. It is invoked when constructing the Einstein-Hilbert action and the kinetic term for scalar fields. The body fixes n=10, scales by grid_spacing^4, and sums the product of sqrt_minus_g and the function value at each uniform grid point.
Claim. The discrete approximation to the integral of a scalar function $f$ over spacetime is given by $Δx^4 ∑_{i=0}^{9} √(-g)(i Δx) f(i Δx)$, where $Δx$ denotes the grid spacing supplied by the volume element and the sum evaluates the metric-weighted function on a uniform grid.
background
The module implements volume integration on spacetime using the √(-g) measure. It adopts a discrete approximation because the full continuous version would require Mathlib measure theory. VolumeElement is the structure holding a positive grid_spacing that defines the uniform sampling lattice. MetricTensor appears in multiple sibling modules as a local bilinear form or determinant interface; the present definition accepts any of these. sqrt_minus_g is the companion definition that currently returns the constant 1 as a scaffold placeholder.
proof idea
The definition is a direct term-mode construction. It binds n to 10, computes Δx4 as vol.grid_spacing raised to the fourth power, then multiplies Δx4 by the Finset.sum over range n of the product sqrt_minus_g g (constant function at i·spacing) and f at the same point.
why it matters
This definition is the integration primitive used by einstein_hilbert_action (which multiplies the Ricci scalar integral by M_P²/2) and by kinetic_action (which integrates the squared gradient). It therefore supplies the common volume factor needed for all action functionals in the Relativity.Fields.Integration module. Within the Recognition framework it discretizes the integral step that precedes the continuous field equations derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.