PsiKinetic
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.
claimThe 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 in Recognition Science
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}.
scope and limits
- Does not incorporate the potential term for the scalar field.
- Does not assign a numerical value to the coupling α.
- Does not perform the variation to obtain equations of motion.
- Does not address quantization or higher-order corrections.
formal statement (Lean)
31noncomputable def PsiKinetic (g : Metric) (ψ : RefreshField) (α : ℝ) : ℝ :=
proof body
Definition body.
32 α * Fields.kinetic_action ψ g default_volume
33
34/-- ψ-sector mass/potential term: (C_lag/2) ∫ √(-g) ψ² d^4x.
35 Now uses actual Fields.potential_action. -/