PsiAction
plain-language theorem explainer
PsiAction assembles the scalar-field contribution to the ILG action as the sum of an α-scaled kinetic term and a C_lag-scaled potential term on a given metric. Workers constructing the total action before taking GR limits cite this definition when separating the Einstein-Hilbert piece from the ψ-sector. The definition is realized by direct addition of the separately defined PsiKinetic and PsiPotential expressions.
Claim. The ψ-sector action is the sum of the kinetic term scaled by α and the potential term scaled by C_lag: $S_ψ[g,ψ;C_lag,α] = K[g,ψ;α] + V[g,ψ;C_lag]$, where $g$ is the metric tensor, $ψ$ a scalar field, $K$ the integral of $g^{μν}∂_μψ∂_νψ$, and $V$ the integral of $ψ²$.
background
In this module the metric is re-exported as Geometry.MetricTensor and the field as Fields.ScalarField. C_lag is supplied by the EightTickResonance definition as φ^{-5} ≈ 0.09, the RS-derived lag coupling. PsiKinetic invokes Fields.kinetic_action scaled by α while PsiPotential invokes Fields.potential_action with argument C_lag², both integrated against the default volume element.
proof idea
One-line wrapper that adds the outputs of PsiKinetic g ψ α and PsiPotential g ψ C_lag.
why it matters
PsiAction supplies the ψ-sector to the total actions S and S_total. It is invoked by the GR-limit theorems gr_limit_reduces and gr_limit_zero, which recover S_EH when C_lag = α = 0. Within the Recognition framework this implements the scalar sector consistent with the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.