VectorField
plain-language theorem explainer
The abbreviation supplies the type of real-valued maps from lattice sites to the three axes for velocity components. Discrete fluid models throughout the module cite this type when defining advection, divergence, and the core operator structure. The declaration is a direct abbreviation that composes the local three-element axis type with the standard function space.
Claim. Let $N$ be a natural number. The space of discrete velocity fields on an $N$-site lattice is the set of all functions assigning to each site and each of the three coordinate directions a real number: maps from the set of sites to the three directions to the reals.
background
The module defines a finite three-direction lattice topology together with discrete differential operators for the incompressible Navier-Stokes equations. Axis is the abbreviation Fin 3 that indexes the coordinate directions. The present abbreviation then types a velocity field by sending each site and each direction to a real component value.
proof idea
The declaration is a one-line abbreviation that directly equates the name to the function type over sites and the three-element axis codomain. No lemmas are invoked.
why it matters
This type is the carrier for velocity data in every subsequent operator, including advection, divergence, vectorLaplacian, and the CoreNSOperator and IncompressibleNSOperator structures. It supplies the concrete velocity field needed to derive pair-budget and viscous-absorption quantities from the flow itself, linking the general tensor geometry (upstream VectorField as Tensor 1 0) to the discrete fluid setting. The declaration thereby supports testing of the Recognition Science forcing chain and D=3 spatial structure inside a fluid model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.