potential_action
plain-language theorem explainer
This definition supplies the potential term in the scalar field action as (m²/2) times the integral of the squared field over the spacetime volume element. Researchers assembling ILG actions or verifying GR limits cite it when the lag parameter vanishes. It is realized as a direct one-line composition with integrate_scalar applied to the squared field.
Claim. The potential action for scalar field $φ$ with mass-squared parameter $m^2$ on metric $g$ and volume element $vol$ equals $(m^2/2) ∫ φ² dV_g$, where $dV_g$ is the discrete volume measure induced by $g$.
background
The module supplies discrete spacetime integration using the √(-g) measure. VolumeElement is a structure carrying a positive grid spacing that approximates the four-volume integral as a finite weighted sum. MetricTensor provides the local bilinear form whose determinant enters the volume factor.
proof idea
One-line wrapper that applies integrate_scalar to (field_squared φ) and scales the result by m_squared / 2.
why it matters
It is called by PsiPotential and by the GR-limit theorems gr_limit_reduces and gr_limit_zero, which recover the Einstein-Hilbert action when α = 0 and C_lag = 0. The definition completes the potential sector of the ILG action, consistent with the Recognition Science forcing chain (T5–T8) and the Recognition Composition Law that governs the underlying J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.