pith. machine review for the scientific record. sign in
def definition def or abbrev high

divergence

show as:
view Lean formalization →

The divergence definition computes the discrete divergence of a vector field on a finite lattice by summing forward differences of each velocity component along its axis. Researchers working on discrete Navier-Stokes or lattice approximations to incompressible flow cite this operator when constructing the continuity equation or checking divergence-free conditions. The definition is a direct sum over the three axes using the forwardDiff operator.

claimGiven a lattice topology with neighbor maps on $N$ sites and spacing $h>0$, together with a vector field $u$ assigning a real value to each site and direction, the divergence at site $x$ equals the sum over the three directions $j$ of the forward difference quotient of the $j$-component of $u$ along direction $j$.

background

The module defines concrete discrete operators on a finite three-direction lattice for the incompressible Navier-Stokes equations. LatticeTopology is a structure supplying plus and minus neighbor maps for each axis. VectorField is the type of maps from sites to the three real velocity components. forwardDiff is the one-sided difference quotient along a chosen axis: (value at plus-neighbor minus value at site) divided by $h$ (see its definition at line 44). Axis is the finite set of three directions. The local setting is the construction of a CoreNSOperator whose derived fields (pair budgets, viscous absorption) are built from the flow's own discrete gradients and Laplacians rather than postulated.

proof idea

One-line wrapper that sums the forwardDiff operator applied componentwise over the three axes.

why it matters in Recognition Science

This operator supplies the discrete divergence term required by the continuity equation in the lattice Navier-Stokes setting. It is referenced by more than forty downstream declarations, including H_Convergence and RiemannSum in CoarseGrain, plus divConstraint and coeffBound in the 2D continuum-limit files. The module documentation states that the six previously free fields are now supplied by a DerivedEstimates layer built on top of the core; the divergence definition is the first concrete operator in that layer. It therefore closes the gap between the discrete flow data and the incompressible constraint used in the classical-bridge identifications.

scope and limits

formal statement (Lean)

  60def divergence {siteCount : ℕ} (Λ : LatticeTopology siteCount) (h : ℝ)
  61    (u : VectorField siteCount) (x : Fin siteCount) : ℝ :=

proof body

Definition body.

  62  ∑ j : Axis, forwardDiff Λ h (fun y => u y j) j x
  63

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.