scalarLaplacian
plain-language theorem explainer
scalarLaplacian supplies the discrete second-difference operator for a scalar field on a finite 3D lattice. Researchers simulating incompressible flows or deriving viscous terms in discrete Navier-Stokes would cite it. The definition is a direct one-line composition that sums the forward difference of the backward difference along each of the three axes.
Claim. For a scalar field $f$ on a lattice with neighbor map given by a topology structure and spacing $h$, the Laplacian at site $x$ is the sum over the three axes $j$ of the forward difference (at spacing $h$) applied to the backward difference of $f$ along axis $j$, evaluated at $x$.
background
The module constructs concrete operators for a discrete incompressible Navier-Stokes flow on a finite lattice. LatticeTopology is a structure supplying, for each of the three axes, a plus and minus neighbor map on the set of sites. ScalarField is simply the type of real-valued functions on those sites. forwardDiff and backwardDiff are the first-order central-difference operators: forwardDiff computes $(f(y^+) - f(y))/h$ and backwardDiff computes $(f(y) - f(y^-))/h$ where $y^+$ and $y^-$ are the lattice neighbors along the chosen axis.
proof idea
The definition is a one-line wrapper that sums, over the three axes, the forwardDiff operator applied to the result of the backwardDiff operator on the input field.
why it matters
scalarLaplacian is invoked by vectorLaplacian and supplies the viscous Laplacian term inside CoreNSOperator and IncompressibleNSOperator. These structures in turn furnish the full discrete operator surface whose pair-budget and absorption fields are derived rather than postulated. The construction sits inside the concrete discrete Navier-Stokes layer that realizes the Recognition Science forcing chain on a lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.