backwardDiff
backwardDiff defines the backward finite difference of a scalar field along one lattice axis on a finite three-directional grid. Discrete fluid modelers cite it when building finite-difference discretizations of the Navier-Stokes equations. The definition is a direct one-line algebraic quotient that subtracts the value at the minus-neighbor and divides by grid spacing h.
claimThe backward difference operator is given by $ (f(x) - f(Λ.minus(j,x))) / h $, where $Λ$ is a lattice topology supplying neighbor maps, $h$ is the uniform spacing, $f$ is a scalar field on the sites, $j$ is an axis in Fin 3, and $x$ is a site index.
background
In the DiscreteNSOperator module a LatticeTopology is a structure that equips a finite set of sites with plus and minus maps from each of the three axes (Axis := Fin 3) to neighboring site indices. ScalarField is the type Fin siteCount → ℝ. These objects sit inside the module's construction of concrete discrete operators for incompressible Navier-Stokes, where previously free pair-budget and stretching data are now derived from the core velocity field and its gradients.
proof idea
The definition is a direct algebraic expression: subtract the field value at the backward neighbor supplied by Λ.minus j x from the value at x, then divide by the supplied spacing h. No lemmas or tactics are invoked; it is the primitive definition of the backward difference quotient.
why it matters in Recognition Science
backwardDiff supplies the backward leg of the centered difference used inside scalarLaplacian, which computes the discrete Laplacian for the viscous term. This feeds the DerivedEstimates layer that replaces assumed pair-budget fields with quantities constructed from the flow's own velocity gradient and Laplacian, completing the IncompressibleNSOperator. The construction discretizes the differential operators required for the three-dimensional incompressible flow equations on a periodic lattice.
scope and limits
- Does not enforce positivity or boundedness of the resulting difference.
- Does not extend to vector fields or incorporate boundary conditions.
- Does not prove consistency or convergence to the continuous Navier-Stokes operator.
- Does not reference Recognition Science constants, the phi-ladder, or the J-cost function.
Lean usage
def laplacianStep {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ) (f : ScalarField siteCount) (x : Fin siteCount) : ℝ := ∑ j : Axis, forwardDiff Λ h (backwardDiff Λ h f j) j xformal statement (Lean)
48def backwardDiff {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
49 (f : ScalarField siteCount) (j : Axis) (x : Fin siteCount) : ℝ :=
proof body
Definition body.
50 (f x - f (Λ.minus j x)) / h
51