ScalarField
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.