pith. machine review for the scientific record. sign in
structure definition def or abbrev high

ScalarField

show as:
view Lean formalization →

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 → ℝ) → ℝ.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  11structure ScalarField where
  12  ψ : (Fin 4 → ℝ) → ℝ
  13
  14/-- Evaluate scalar field at a point. -/

used by (29)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.