S_on
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.
claimLet $(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 in Recognition Science
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.
scope and limits
- Does not evaluate the action for concrete metrics or fields.
- Does not derive the numerical value of C_lag or alpha.
- Does not expand the explicit integrand of the PsiAction term.
Lean usage
S_on inp { alpha := 0, cLag := 0 }formal statement (Lean)
129noncomputable def S_on (inp : ActionInputs) (p : ILGParams) : ℝ :=
proof body
Definition body.
130 S_total inp.fst inp.snd p
131
132/-- Full ILG action: S[g, ψ; C_lag, α] := S_EH[g] + S_ψ[g,ψ]. -/