dS_dx
plain-language theorem explainer
dS_dx supplies the ordinary derivative of an action functional S_func at a point x0. Physicists deriving Euler-Lagrange equations from the ILG action would cite it when reducing a one-variable variation to a concrete rate of change. The definition is a direct one-line wrapper around Mathlib's deriv operator.
Claim. The derivative of the action functional $S$ with respect to the state variable $x$ at the point $x_0$ is given by $dS/dx(x_0)$ where $S$ is represented by the scalar function $S:ℝ→ℝ$.
background
The sibling definition S constructs the full ILG action as $S[g,ψ;C_{lag},α]:=S_{EH}[g]+S_ψ[g,ψ]$, with the Einstein-Hilbert term plus the scalar-field contribution. The module re-exports geometry and field types to support such constructions. The listed upstream results supply auxiliary constants and structures (alpha, L) that appear in the broader ILG Lagrangian but are not invoked inside this definition.
proof idea
The definition is a one-line wrapper that applies the deriv operator to the supplied function S_func at the evaluation point x0.
why it matters
This supplies the basic variation operator required to obtain equations of motion from the ILG action S. It occupies the interface between the action definition and subsequent field equations inside the Relativity.ILG.Action module. No downstream uses are recorded, leaving open its concrete insertion into full variational derivations of the ILG field equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.