RefreshField
plain-language theorem explainer
RefreshField provides a type alias for scalar fields in the ILG action module. Researchers deriving the general relativity limit of the ILG action would cite this abbreviation when specifying the scalar component ψ in action functionals. The definition is a direct re-export of the scalar field structure from the Fields module with no additional steps required.
Claim. RefreshField is the type of scalar fields, where each scalar field assigns a real value to every spacetime point via a map from functions of type $(Fin 4 → ℝ)$ to $ℝ$.
background
The module re-exports geometry and field types for ILG use. A scalar field assigns a real value to each spacetime point, as stated in the upstream Fields.Scalar definition: structure ScalarField where ψ : (Fin 4 → ℝ) → ℝ. Parallel aliases exist in the Navier-Stokes discrete operator and the geometry tensor module to support compatibility across discrete and continuous settings.
proof idea
This is a one-line abbreviation that directly equates RefreshField to the scalar field type from the Fields module.
why it matters
The alias feeds ActionInputs as Metric × RefreshField and supports the GR-limit theorems gr_limit_cov, gr_limit_reduces, and gr_limit_zero, which establish that the total action reduces to the Einstein-Hilbert action S_EH when ILG parameters alpha and cLag are set to zero. It enables the covariant scalar Lagrangian L_cov in the relativity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.