integrate_smul
plain-language theorem explainer
The scaling property for discrete scalar integration over a spacetime grid states that multiplying the integrand by a real constant c scales the entire integral by the same factor. Physicists discretizing actions in general relativity would cite this when pulling constants out of kinetic or potential terms in the action functional. The proof works by unfolding the sum definition, verifying a pointwise algebraic identity on the grid, commuting the constant through the finite sum, and finishing with ring simplification.
Claim. For $c$ a real number, $f$ a real-valued function on spacetime points, $g$ a metric tensor, and vol a volume element with positive grid spacing, the discrete integral satisfies $c$ times the integral of $f$ equals the integral of the pointwise product $c f$, where each integral is the finite sum over the grid weighted by the volume factor at each point.
background
The module implements volume integration on spacetime via a discrete grid approximation to the measure involving the volume factor. VolumeElement is the structure carrying the uniform grid spacing used for sampling points. MetricTensor supplies the local bilinear form whose determinant yields the volume weight at each grid point. This construction appears in the relativity section as a scaffold toward continuous integration, with the discrete sum standing in for the spacetime volume element in action functionals.
proof idea
The proof unfolds the definition of the discrete scalar integral to expose the explicit weighted sum. It introduces a pointwise ring identity showing the volume factor times the scaled function equals the constant times the unscaled product. simp_rw substitutes the identity across the grid, rw pulls the constant out of the sum using the distributive law for finite sums, and ring closes the equality.
why it matters
This linearity property supports the definitions of kinetic_action, potential_action, and einstein_hilbert_action in the same module by allowing constant coefficients to be extracted from the integrated terms. It fills a basic algebraic step in the discrete variational setup for relativistic field equations. Within the Recognition Science framework it closes a small gap in the scaffolding for metric-based integrals that appear downstream from the forcing chain and metric constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.