kinetic_action
The kinetic action for a scalar field is defined as one half the discrete integral of its metric-contracted gradient squared. Physicists building scalar-field actions in curved spacetime cite this when assembling the kinetic term of the Lagrangian density. The definition is realized as a direct one-line composition of the integrate_scalar routine with the gradient-squared operator.
claimFor a scalar field $φ$, metric $g$, and volume element $vol$, the kinetic action equals $½ ∫ √(-g) g^{μν} (∂_μ φ)(∂_ν φ) d⁴x$, where the integral is the discrete approximation supplied by the volume element.
background
The module implements volume integration on spacetime using a discrete grid. VolumeElement is a structure carrying a positive real grid_spacing that sets the uniform spacing Δx for summation. ScalarField is an abbreviation for a map from spacetime points (Fin 4 → ℝ) to reals. MetricTensor supplies the local bilinear form whose components yield both the inverse metric for index raising and the factor √(-g) for the measure. integrate_scalar performs the actual summation by evaluating the integrand at grid points and scaling by (grid_spacing)^4 times √(-g). The module documentation states that this is a scaffold using discrete approximation; a full measure-theoretic version would invoke Mathlib integration theory.
proof idea
The definition is a one-line wrapper that applies integrate_scalar to gradient_squared φ g and multiplies the result by 1/2.
why it matters in Recognition Science
This supplies the kinetic term inside PsiKinetic and the full ILG action, which in turn feeds the theorems gr_limit_reduces and gr_limit_zero showing reduction to the Einstein-Hilbert action when the coupling constants α and C_lag vanish. It therefore closes the discrete-to-continuous bridge for the ψ-sector in the relativity layer and supports the nonnegativity result kinetic_nonneg. The construction aligns with the Recognition Science treatment of field actions on a metric background.
scope and limits
- Does not implement a continuous manifold integral or Lebesgue measure.
- Does not fix any particular coordinate chart or explicit metric components.
- Does not extend to vector, spinor, or gauge fields.
- Does not incorporate higher-curvature or non-minimal coupling terms.
formal statement (Lean)
43noncomputable def kinetic_action
44 (φ : ScalarField) (g : MetricTensor) (vol : VolumeElement) : ℝ :=
proof body
Definition body.
45 (1/2) * integrate_scalar (gradient_squared φ g) g vol
46
47/-- Potential action integral: (1/2) ∫ √(-g) m² ψ² d⁴x. -/