RefreshField
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.
claimRefreshField 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 in Recognition Science
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.
scope and limits
- Does not specify dynamics or equations of motion for the field.
- Does not include the metric tensor or volume element.
- Does not enforce normalization or boundary conditions on ψ.
formal statement (Lean)
11abbrev RefreshField := Fields.ScalarField