forwardDiff
plain-language theorem explainer
forwardDiff supplies the forward finite-difference operator on a finite lattice equipped with a three-axis topology. Discrete Navier-Stokes constructions cite it to assemble advection, divergence, and Laplacian terms from scalar and vector fields. Its body consists of a single arithmetic expression that subtracts the field value at the current site from the forward neighbor and divides by the grid spacing h.
Claim. The forward difference of a scalar field $f$ on a lattice with topology $Λ$ and spacing $h$ in direction $j$ at site $x$ is given by $(f(Λ.plus j x) - f(x))/h$.
background
The module constructs a concrete discrete incompressible Navier-Stokes operator surface on a finite lattice. Axis is the type Fin 3 indexing the three spatial directions. LatticeTopology is a structure supplying plus and minus neighbor functions for each axis. ScalarField is the abbreviation Fin siteCount → ℝ assigning a real value to each lattice site. This setting provides the finite three-direction lattice topology and the discrete differential operators needed for the CoreNSOperator and DerivedEstimates layers.
proof idea
The definition is realized as a direct one-line arithmetic expression: subtract the field value at site x from its image under the plus neighbor map in direction j, then divide by the grid spacing h.
why it matters
This definition is the foundational operator for the discrete differential calculus in the module. It is used directly by the advection, divergence, scalarLaplacian, and velocityGradientMag definitions. These in turn populate the pair-budget and viscous-absorption fields in the DerivedEstimates layer for the incompressible Navier-Stokes system. Within Recognition Science it discretizes the continuum operators while preserving constructivity on a finite site set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.