velocityGradientMag
plain-language theorem explainer
The velocityGradientMag definition returns the largest absolute forward difference of any velocity component in any lattice direction at a given site on a finite lattice. Discrete Navier-Stokes modelers working inside the Recognition Science framework cite it when extracting local strain rates from lattice velocity data to derive pair budgets. It is realized directly as the supremum of absolute forwardDiff values over the Cartesian product of all components and directions.
Claim. Let $N$ be a positive integer, let $Λ$ be a lattice topology on $N$ sites, let $h>0$ be the lattice spacing, let $u$ assign a real value to each site and each axis (the three velocity components), and let $x$ be a site. Then velocityGradientMag$(Λ,h,u,x)$ equals the supremum over all component-direction pairs $(c,d)$ of the absolute forward difference of the scalar field for component $c$ taken in direction $d$ and evaluated at site $x$.
background
The DiscreteNSOperator module supplies a concrete surface for discrete incompressible Navier-Stokes on a finite three-direction lattice. LatticeTopology is the structure recording plus and minus neighbor maps for each axis. VectorField is the abbreviation for maps from sites to axis-indexed reals that encode the three velocity components at every lattice point. ForwardDiff is the sibling operator that realizes the scaled one-sided difference using the topology's plus map.
proof idea
The definition is a direct one-line wrapper. It forms the Cartesian product of the universe of axes with itself, proves the product is nonempty, and takes the supremum of the absolute value of forwardDiff applied to the component scalar field in the chosen direction at the target site.
why it matters
velocityGradientMag supplies the local strain measure that corePairStretchFactor uses to construct the pair stretch factor from core data alone. This closes the DerivedEstimates layer that turns the CoreNSOperator (which carries only physical flow data) into the full IncompressibleNSOperator whose pair budgets are no longer free parameters. The construction sits inside the module's program of deriving all auxiliary fields from the velocity field itself, consistent with the Recognition Science emphasis on self-consistent lattice operators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.