VectorField
plain-language theorem explainer
VectorField siteCount is the type of real-valued velocity fields on a finite lattice with siteCount sites, each site carrying a three-component vector indexed over the coordinate axes. Discrete fluid modelers cite it when supplying velocity data to lattice Navier-Stokes operators. The declaration is a one-line abbreviation that reindexes the general tensor vector field to site-wise real triples via the local Axis definition.
Claim. A vector field on a lattice with $N$ sites is a function $u$ from the set of sites to the three real components indexed by the coordinate axes, i.e., $u : [N] → ℝ^3$.
background
The DiscreteNSOperator module constructs a concrete surface for discrete incompressible Navier-Stokes on a finite three-direction lattice. Axis is the sibling abbreviation Fin 3 that labels the three spatial directions. The upstream VectorField from Relativity.Geometry.Tensor is the general tensor abbreviation Tensor 1 0; the present declaration specializes it to site-indexed real vectors for velocity data.
proof idea
The declaration is a one-line abbreviation that composes the site-indexed function type with the Axis indexing from the sibling definition.
why it matters
VectorField supplies the velocity type for CoreNSOperator and IncompressibleNSOperator, which in turn feed the advection, divergence, vectorLaplacian and velocityGradientMag definitions. It supplies the concrete data layer for lattice Navier-Stokes modeling inside the Recognition Science framework, consistent with the three-dimensional spatial structure fixed by the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.