S_on
plain-language theorem explainer
S_on is a convenience definition that applies the total ILG action to a bundled pair of metric and refresh field together with the ILG parameter structure. Researchers reducing the ILG theory to its GR limit or evaluating actions on concrete inputs would cite this wrapper. The definition is a one-line delegation to S_total after unpacking the ActionInputs pair.
Claim. Let $(g,ψ)$ be an action input pair consisting of a metric and a refresh field, and let $p$ be the ILG parameter structure containing $α$ and $C_{lag}$. Then $S_{on}((g,ψ),p)$ equals the total action $S_{total}(g,ψ,p)$.
background
The module re-exports geometry and field types for ILG use. ActionInputs is the abbreviation Metric × RefreshField that bundles the metric $g$ and refresh field $ψ$ for downstream convenience. ILGParams is the structure holding the coupling constants alpha and cLag, where cLag is supplied by the upstream definition C_lag = φ^{-5} from EightTickResonance. The upstream S_total expands to S_EH g + PsiAction g ψ p.cLag p.alpha, and S_EH is an alias for the Einstein-Hilbert action.
proof idea
The definition is a one-line wrapper that applies S_total to the first and second components of the input pair together with the parameter bundle.
why it matters
This definition supplies the bundled form of the full ILG action S[g, ψ; C_lag, α] := S_EH[g] + S_ψ[g,ψ] required by the GR-limit theorem gr_limit_on. It closes the interface between the parameter structure and the action computation, allowing the reduction when alpha = 0 and cLag = 0 to recover the pure Einstein-Hilbert term. The construction sits inside the Recognition Science derivation of the ILG action from the eight-tick resonance and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.