ScalarField
plain-language theorem explainer
ScalarField supplies the type of real-valued functions on a finite lattice with a prescribed number of sites. Workers on discrete fluid models cite this abbreviation when constructing difference operators and transport fields for incompressible flows. The definition is a straightforward type alias to the function space from the finite set of sites to the reals.
Claim. A scalar field on a lattice with $N$ sites is a function from the finite index set of size $N$ to the real numbers.
background
The module sets out a concrete surface for discrete incompressible Navier-Stokes operators on a finite lattice. It introduces a three-direction lattice topology together with discrete differential operators, then builds a CoreNSOperator that carries only physical flow data before deriving the remaining fields. ScalarField types the scalar inputs to these operators.
proof idea
The declaration is a direct type abbreviation with no computational body or proof obligations.
why it matters
This type underpins the entire suite of discrete operators, including forwardDiff, backwardDiff, scalarLaplacian, conservativeTransportField, CoreNSOperator and the derived IncompressibleNSOperator. It allows pair-budget and absorption fields to be constructed from the core velocity data rather than postulated. The step closes an earlier modeling gap in the discrete Navier-Stokes surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.