advection
plain-language theorem explainer
The advection definition supplies the discrete convective term for each velocity component on a finite lattice with three axes. Researchers proving discrete maximum principles or J-cost bounds for lattice Navier-Stokes models cite this operator when assembling the momentum update. It is realized as a direct sum over the three axes that weights the forward difference of the target component by the local velocity.
Claim. Let $N$ be the number of lattice sites, let $h>0$ be the spacing, let $u$ assign a velocity vector in each of the three directions to every site, and let $x$ be a site. The advection contribution to the $i$-th momentum equation at $x$ is $sum_{j=1}^3 u(x,j)cdotfrac{u(plus_j(x),i)-u(x,i)}{h}$, where $plus_j$ is the forward-neighbor map in direction $j$.
background
The module builds concrete finite-difference operators for the incompressible Navier-Stokes system on a lattice whose topology is given by a LatticeTopology structure containing plus and minus maps for each axis. VectorField is the type of maps from sites to three-component velocities. forwardDiff computes the one-sided difference quotient of a scalar field along a chosen axis. The module doc states that these operators are used to derive pair-budget and viscous-absorption fields from the velocity gradient and Laplacian rather than treating them as free data.
proof idea
The definition is a one-line wrapper that applies the forwardDiff operator componentwise: it sums, over the three axes, the product of the local velocity component with the forward difference of the target velocity component.
why it matters
Advection is invoked inside the construction of OneStepData and inside the proof of Jcost_nonincreasing, which establishes that the cumulative J-cost is non-increasing along discrete evolution steps. This places the operator inside the chain that converts the Recognition Science J-functional into a discrete maximum principle for the Navier-Stokes system on the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.