PsiKinetic
plain-language theorem explainer
PsiKinetic supplies the kinetic term in the ψ-sector of the ILG action by scaling the standard kinetic integral with the parameter α. Researchers deriving the full ψ action or proving reduction to Einstein-Hilbert gravity cite it when α vanishes. The definition is a direct one-line scaling of the kinetic_action integral from the Fields module using the default volume element.
Claim. The kinetic contribution is defined by $K(g,ψ,α) := α · (1/2) ∫ √(-g) g^{μν} (∂_μ ψ)(∂_ν ψ) d⁴x$, where $g$ is the metric tensor, $ψ$ the scalar field, and the integral employs the default volume element.
background
The ILG.Action module re-exports geometry and field types for constructing the ILG action. Metric is an abbreviation for the metric tensor from Geometry, and RefreshField is an abbreviation for the scalar field from Fields. Upstream, kinetic_action from Fields.Integration computes the unscaled integral (1/2) ∫ √(-g) g^{μν} (∂_μ φ)(∂_ν φ) d⁴x, while default_volume supplies the integration measure with unit grid spacing.
proof idea
The definition is a one-line wrapper that applies Fields.kinetic_action to the inputs ψ, g and default_volume, then multiplies the result by the parameter α.
why it matters
PsiKinetic supplies the kinetic piece of PsiAction and PsiActionP, which appear in the GR-limit theorems gr_limit_reduces and gr_limit_zero. These theorems recover the Einstein-Hilbert action when α = 0, consistent with the Recognition Science framework that derives gravity from the J-functional, the phi-ladder, and the eight-tick resonance structure with C_lag = φ^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.