ActionInputs
plain-language theorem explainer
ActionInputs bundles the metric tensor with the scalar field into a single product type for the ILG action. Researchers stating the GR limit or defining the total action functional cite this abbreviation to handle the input pair without repetition. The declaration is a direct one-line type alias with no computation or additional structure.
Claim. The bundled input type for the action is the Cartesian product of the metric tensor type and the scalar field type.
background
The module re-exports geometry and field types for ILG use. Metric is the metric tensor re-exported from the geometry module, while RefreshField is the scalar field re-exported from the fields module. Upstream results supply summation operations: the total function from discrete vorticity sums a scalar field over a finite lattice window, and the total from the error budget sums its three error components.
proof idea
The declaration is a one-line type abbreviation that directly forms the product of the metric tensor and scalar field re-exports.
why it matters
This abbreviation is referenced by the total action definition S_on and by the GR limit theorem gr_limit_on, which shows that the ILG action reduces to the Einstein-Hilbert term when the lag and alpha parameters vanish. It packages inputs for the functional S[g, ψ; C_lag, α] := S_EH[g] + S_ψ[g,ψ] and supports the Recognition Science treatment of the action principle in the relativity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.