conservativeTransportField
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.
claimGiven 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 in Recognition Science
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.
scope and limits
- Does not encode any specific lattice topology or spatial dimension.
- Does not impose positivity, boundedness or incompressibility on the output field.
- Does not incorporate viscous or stretching contributions.
- Does not address the continuum limit or convergence to classical Navier-Stokes.
formal statement (Lean)
68def conservativeTransportField {siteCount : ℕ}
69 (flux : ScalarField siteCount) (perm : Equiv.Perm (Fin siteCount)) :
70 ScalarField siteCount :=
proof body
Definition body.
71 fun i => flux i - flux (perm i)
72