backwardDiff
plain-language theorem explainer
backwardDiff supplies the backward finite-difference operator on a scalar field over a finite lattice with three axes. Discrete Navier-Stokes modelers cite it when constructing the viscous term via the Laplacian. The definition is a direct one-line expression using the lattice's minus neighbor map.
Claim. The backward difference of scalar field $f$ on lattice topology $Λ$ with spacing $h$ along axis $j$ at site $x$ equals $(f(x) - f(Λ.minus(j,x)))/h$.
background
Axis is the type Fin 3 indexing the three spatial directions. LatticeTopology is the structure supplying plus and minus neighbor maps for each axis on a finite set of sites. ScalarField is the abbreviation for real-valued functions on Fin siteCount. This module builds concrete discrete differential operators for the incompressible Navier-Stokes equations on a lattice, with the six previously free fields now derived from the core flow data. The continuous ScalarField from Relativity.Fields.Scalar assigns a real to each spacetime point, but the discrete version here supports the finite-site model.
proof idea
One-line definition that subtracts the value at the minus-neighbor site and divides by the spacing h.
why it matters
backwardDiff is invoked inside scalarLaplacian to build the discrete Laplacian as the sum over axes of forwardDiff applied to backwardDiff. It forms part of the concrete DiscreteNSOperator layer that supplies the pair-budget fields from the flow's own gradients rather than as free data, closing the IncompressibleNSOperator construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.