S
plain-language theorem explainer
The definition S assembles the complete ILG action by adding the Einstein-Hilbert term to the scalar-field sector. Researchers deriving Noether currents or checking convexity of the action functional would reference this expression. It is assembled as a direct sum of the two component actions S_EH and PsiAction.
Claim. $S(g, ψ; C_{lag}, α) := S_{EH}(g) + S_ψ(g, ψ; C_{lag}, α)$, where $g$ is a metric tensor, $ψ$ a scalar field, and $C_{lag}, α$ are real parameters.
background
In the ILG module, Metric is an abbreviation for the metric tensor from the geometry library, while RefreshField stands for the scalar field type. The Einstein-Hilbert action S_EH is aliased to EHAction, and PsiAction combines the kinetic and potential contributions of the scalar field, with the lag parameter C_lag fixed to φ^{-5} in the Recognition Science setting. The module re-exports these types to support the full action functional for the induced low-energy gravity model. The upstream C_lag definition supplies the RS-native value φ^{-5} ≈ 0.09 that controls the coupling strength in the potential term.
proof idea
The definition is a one-line wrapper that adds the Einstein-Hilbert action S_EH g to the scalar sector PsiAction g ψ C_lag α.
why it matters
This action serves as the input to the Noether invariance checks in the Action.Noether module, where it establishes time-translation invariance implying energy conservation and space-translation invariance implying momentum conservation. It also supports the convexity arguments in FunctionalConvexity. Within the Recognition framework it encodes the full dynamics whose J-cost structure is analyzed downstream, linking the eight-tick resonance (via C_lag) to the classical limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.