kinetic_nonneg
plain-language theorem explainer
Kinetic action of a scalar field is nonnegative whenever the squared gradient is nonnegative at every point. Discrete spacetime modelers cite it to guarantee the action functional is bounded from below. The term proof unfolds the integral definition then chains nonnegativity of multiplication, fourth powers, and finite sums.
Claim. Let ϕ be a scalar field, g a metric tensor, and V a volume element with positive grid spacing. If ∀x, 0 ≤ g^{μν}(∂_μ ϕ)(∂_ν ϕ)(x), then 0 ≤ (1/2) ∫_V √(-g) g^{μν} (∂_μ ϕ)(∂_ν ϕ) d⁴x.
background
The module supplies discrete approximations to spacetime integrals. VolumeElement is a structure carrying a positive real grid_spacing that scales the four-dimensional volume element. ScalarField is the abbreviation for maps from a finite index set to the reals. MetricTensor is the local bilinear form supplying g_{μν} components at each point.
proof idea
The term proof unfolds kinetic_action to (1/2) times integrate_scalar of gradient_squared, then applies mul_nonneg to the constant factor 1/2, pow_nonneg to the positive grid_spacing raised to the fourth power, Finset.sum_nonneg over the sample points, and the supplied hypothesis hSign at each point.
why it matters
The result secures positivity of the kinetic term inside the action integral, a prerequisite for stability of the Euler-Lagrange equations. It feeds the Einstein-Hilbert action construction later in the same module. In the Recognition framework it aligns with the positive spatial signature required by the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.