integrate_add
plain-language theorem explainer
The theorem establishes additivity of the discrete spacetime integral operator over sums of scalar fields on a four-dimensional grid. Researchers splitting kinetic plus potential contributions in discretized actions within the Recognition Science relativity module invoke it directly. The proof is a one-line term reduction that unfolds the integral definition and applies sum additivity together with the mul_add lemma.
Claim. Let $I(f,g,vol)$ denote the discrete integral of a scalar field $f$ against the volume element $vol$ weighted by the metric tensor $g$. Then $I(f_1+f_2,g,vol)=I(f_1,g,vol)+I(f_2,g,vol)$ for any scalar fields $f_1,f_2$.
background
The module implements volume integration on spacetime using a discrete approximation to the measure $d^4x$ with factor $√(-g)$. VolumeElement supplies the uniform grid spacing for the finite sum, while MetricTensor provides the local bilinear form that enters the weight. The upstream mul_add theorem from ArithmeticFromLogic supplies the required distributivity over the arithmetic of the grid points.
proof idea
The term proof unfolds integrate_scalar to expose the underlying Finset sum, then applies simp with Finset.sum_add_distrib to obtain additivity of the sums and mul_add to distribute the metric factor across the two fields.
why it matters
Linearity closes the basic algebraic step needed to decompose integrated actions such as the Einstein-Hilbert action and scalar kinetic terms into separate contributions inside the discrete scaffolding. It supports the finite-sum treatment of the action integral in the relativity module before any continuum limit is taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.