ScalarField
plain-language theorem explainer
ScalarField equips a real-valued map on 4D spacetime with a structure wrapper for use in relativistic and discrete fluid models. Researchers constructing tensor fields or Navier-Stokes operators cite this type to represent assignments of reals to spacetime points. The declaration is a direct structure definition containing only the field ψ of type (Fin 4 → ℝ) → ℝ.
Claim. A scalar field is a map $ψ : (ℝ^4 → ℝ)$ that assigns a real number to each point in four-dimensional spacetime.
background
The Relativity.Fields.Scalar module defines ScalarField as a structure whose single field ψ has type (Fin 4 → ℝ) → ℝ. This matches the abbrev ScalarField := (Fin 4 → ℝ) → ℝ declared in Relativity.Geometry.Tensor. The discrete counterpart in NavierStokes.DiscreteNSOperator is the abbrev ScalarField (siteCount : ℕ) := Fin siteCount → ℝ, used for lattice sites. The module doc-comment states that a scalar field assigns a real value to each spacetime point.
proof idea
The declaration is a structure definition that directly introduces the component ψ of type (Fin 4 → ℝ) → ℝ. No lemmas are applied and no tactics are invoked; it is a pure type declaration.
why it matters
ScalarField supplies the continuous scalar-field type referenced by 29 downstream declarations, chiefly the difference operators and CoreNSOperator structures in NavierStokes.DiscreteNSOperator. It realizes the scalar-field notion required by the Recognition framework in the 4D spacetime setting that follows from T8 (D = 3 spatial dimensions). The definition closes the interface between the Geometry.Tensor abbrev and the discrete lattice operators without introducing additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.