LatticeTopology
plain-language theorem explainer
LatticeTopology equips a finite set of N sites with forward and backward shift maps along each of three axes. Discrete Navier-Stokes modelers cite it to ground finite-difference operators such as forwardDiff and advection on a periodic lattice. The declaration is a bare structure with two function fields and no additional axioms or proofs.
Claim. Let $N$ be a positive integer. A lattice topology on $N$ sites consists of two maps plus and minus, each sending an axis in Fin 3 and a site in Fin $N$ to another site in Fin $N$.
background
The module supplies concrete finite-difference operators for incompressible Navier-Stokes on a lattice with three spatial directions. Axis is the abbreviation Fin 3. LatticeTopology records the neighbor relations that let forwardDiff compute (f(plus j x) - f x)/h and backwardDiff compute (f x - f(minus j x))/h.
proof idea
Direct structure definition. The declaration introduces the two fields plus and minus with no lemmas, tactics, or reduction steps.
why it matters
LatticeTopology is the base data structure for every discrete operator in the module. It is extended by CoreNSOperator and IncompressibleNSOperator, and is used to define forwardDiff, backwardDiff, divergence, advection, scalarLaplacian and vectorLaplacian. In the Recognition framework it realizes the three-dimensional lattice (T8) on which the discrete Navier-Stokes evolution is built.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.