S_total
plain-language theorem explainer
S_total assembles the total action for the ILG model as the sum of the Einstein-Hilbert term and the ψ-sector contribution. Workers on scalar-tensor or modified-gravity extensions would cite this definition when writing the full variational principle. The definition is a direct algebraic sum of S_EH and PsiAction using the bundled ILGParams record.
Claim. $S(g,ψ,p) := S_{EH}(g) + S_ψ(g,ψ; p.c_{Lag}, p.α)$ where $g$ is a metric tensor, $ψ$ a scalar field, and $p$ is the ILGParams record containing the fine-structure parameter $α$ and the lag constant $C_{Lag}$.
background
The module re-exports geometry and field types for ILG constructions. Metric abbreviates Geometry.MetricTensor while RefreshField abbreviates Fields.ScalarField. ILGParams is the structure bundling alpha : ℝ and cLag : ℝ. PsiAction is the sum of the kinetic and potential terms for the scalar field, parameterized by C_lag and α. S_EH is an alias for the Einstein-Hilbert action EHAction. The local setting is the assembly of the complete ILG action functional from its gravitational and ψ-sector pieces.
proof idea
The definition is a one-line wrapper that directly sums S_EH g with PsiAction g ψ p.cLag p.alpha.
why it matters
This definition supplies the complete action S[g, ψ; C_lag, α] referenced by the downstream theorems gr_limit_zero and gr_limit_on, which recover the pure Einstein-Hilbert dynamics in the GR limit α = 0, C_lag = 0. It realizes the full ILG action as the sum of the gravitational term and the ψ-sector action, supporting the parameter-bundled interface used by S_on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.