vectorLaplacian
plain-language theorem explainer
The vectorLaplacian supplies the componentwise discrete Laplacian for vector fields on a finite lattice with given topology and spacing. Researchers deriving discrete incompressible Navier-Stokes schemes would cite it when assembling the viscous term from lattice differences. It is realized as a one-line wrapper delegating directly to the scalar Laplacian applied to each velocity component.
Claim. For lattice topology $Λ$ on $N$ sites with spacing $h$ and vector field $u : Fin N → Axis → ℝ$, the vector Laplacian at site $x$ along axis $i$ is defined by applying the scalar Laplacian to the $i$-th component: $Δ_h u_i(x)$, where $Δ_h f(x) = ∑_{j:Axis} forwardDiff(Λ,h,backwardDiff(Λ,h,f,j),j,x)$.
background
This module defines concrete discrete operators for the incompressible Navier-Stokes equations on a finite three-direction lattice. LatticeTopology encodes nearest-neighbor maps plus and minus along each axis. VectorField is the type Fin siteCount → Axis → ℝ. scalarLaplacian computes the discrete second derivative as the sum over axes of forwardDiff composed with backwardDiff.
proof idea
One-line wrapper that applies scalarLaplacian to the function extracting the i-th component of u.
why it matters
It supplies the viscous operator inside the CoreNSOperator and DerivedEstimates layer of the discrete incompressible NS construction. The module builds the full IncompressibleNSOperator whose pair-budget fields are derived from velocity gradients and Laplacians rather than assumed. This step closes part of the scaffolding toward a lattice realization of the Recognition Science forcing chain for fluid dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.