conservativeTransportField
plain-language theorem explainer
conservativeTransportField defines a scalar field on a finite lattice by pointwise subtraction of a permuted flux from the original flux. Discrete fluid dynamics researchers cite this construction when assembling conservative advection terms in lattice Navier-Stokes models. The definition is a direct lambda abstraction that computes the difference at each site index without further structure.
Claim. Given a scalar field $f : [N] → ℝ$ and a permutation $σ$ of the finite set of sites, the conservative transport field is the scalar field $g$ defined by $g(i) = f(i) - f(σ(i))$ for each site $i$.
background
In the DiscreteNSOperator module a ScalarField on siteCount sites is the type Fin siteCount → ℝ, i.e., any real-valued assignment to the lattice points. The module supplies concrete discrete differential operators on a finite three-direction lattice topology so that an incompressible Navier-Stokes flow can be realized with only physical data in the CoreNSOperator structure; pair-budget and absorption fields are then derived rather than postulated. Upstream scalar-field notions appear in the Relativity modules as maps from spacetime points to reals, supplying the general field concept specialized here to the discrete lattice.
proof idea
The definition is a one-line wrapper that applies pointwise subtraction: the returned function maps each site index i to flux i minus flux evaluated at the image of i under the supplied permutation.
why it matters
This definition supplies the transport term used inside CoreNSOperator and IncompressibleNSOperator, which extend EvolutionIdentity with lattice topology, spacing h and viscosity ν. It is the direct input to the theorem total_conservativeTransportField_zero that proves the sum of the resulting field vanishes, thereby enforcing discrete conservation. Within the Recognition Science framework the construction supports the lattice realization of the Navier-Stokes equations that follows from the forcing chain (T0–T8) and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.