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

ScalarField

show as:
view Lean formalization →

A scalar field on four-dimensional spacetime is an abbreviation for maps from points (Fin 4 to reals) to reals. Discrete Navier-Stokes developers and relativistic field modelers cite it when passing fields to difference operators or transport definitions. The declaration is a one-line type abbreviation with no proof obligations or computational body.

claimA scalar field is a function of type $ (Fin 4 → ℝ) → ℝ $, assigning a real value to each point in four-dimensional spacetime.

background

The module is explicitly labeled a scaffold and lies outside the certificate chain. It supplies type abbreviations that connect the relativistic scalar-field structure to discrete operators. Upstream, the Relativity.Fields.Scalar module defines ScalarField as a structure whose sole field ψ has type (Fin 4 → ℝ) → ℝ. The NavierStokes.DiscreteNSOperator module re-exports an analogous but site-count-parameterized abbreviation Fin siteCount → ℝ for lattice fields.

proof idea

Direct abbreviation: ScalarField is defined exactly as the function type (Fin 4 → ℝ) → ℝ, matching the ψ component of the upstream structure without further reduction or lemmas.

why it matters in Recognition Science

The abbreviation is referenced by twenty-nine downstream declarations inside DiscreteNSOperator, including forwardDiff, backwardDiff, conservativeTransportField, CoreNSOperator, and IncompressibleNSOperator. It supplies the common field type that lets lattice difference operators act uniformly on both relativistic and discrete-NS data. Because the module is scaffolded, the abbreviation remains outside the main forcing-chain certificate.

scope and limits

formal statement (Lean)

  14abbrev ScalarField := (Fin 4 → ℝ) → ℝ

used by (29)

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

depends on (2)

Lean names referenced from this declaration's body.