PsiActionP
plain-language theorem explainer
The declaration defines the ψ-sector action as the sum of its kinetic and potential contributions, taking a metric, scalar field, and the ILG parameter bundle. Model builders assembling the full ILG action functional cite this when separating the ψ dynamics from the Einstein-Hilbert sector. It is a one-line wrapper that forwards the alpha and cLag components to the pre-defined kinetic and potential terms.
Claim. Let $S_ψ(g, ψ, p)$ be the ψ-sector action for metric tensor $g$, scalar field $ψ$, and parameter bundle $p = (α, c_{Lag})$. Then $S_ψ(g, ψ, p) = K(g, ψ, α) + V(g, ψ, c_{Lag})$, where $K$ is the kinetic term scaled by the fine-structure constant and $V$ is the potential term scaled by the lag coefficient.
background
The module re-exports geometry and field types for ILG use. Metric is the abbreviation for Geometry.MetricTensor. RefreshField is the abbreviation for Fields.ScalarField. ILGParams is the structure holding the two real parameters alpha and cLag. Upstream, alpha is the fine-structure constant defined as 1/alphaInv. PsiKinetic implements the kinetic contribution (α/2) ∫ √(-g) g^{μν} (∂_μ ψ)(∂_ν ψ) d⁴x via Fields.kinetic_action, while PsiPotential supplies the corresponding mass term.
proof idea
One-line wrapper that adds the results of PsiKinetic (passing p.alpha) and PsiPotential (passing p.cLag). No further tactics or reductions are applied.
why it matters
This bundles the ψ-sector pieces so they can be inserted into the consolidated ILG action alongside the Einstein-Hilbert term. It supports later construction of observables and variation equations in the Relativity.ILG module. The definition incorporates the fine-structure constant drawn from the universal forcing self-reference chain and keeps the action functional ready for the eight-tick octave and D=3 geometry of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.