monotonicityCert
plain-language theorem explainer
The monotonicityCert definition packages any incompressible Navier-Stokes operator on a finite lattice into a certificate by supplying the operator and confirming its J-cost time derivative is nonpositive. Researchers modeling discrete incompressible flows in Recognition Science would cite this to establish dissipation for lattice operators. The construction is a direct one-line wrapper that invokes the nonpositive derivative theorem for the operator.
Claim. Let $ns$ be an incompressible Navier-Stokes operator on a lattice with $siteCount$ sites. The monotonicity certificate for $ns$ consists of the operator $ns$ together with the assertion that the time derivative of its J-cost satisfies $dJ_{cost}/dt(ns) ≤ 0$.
background
This module closes the bookkeeping part of the monotonicity program for a concrete discrete incompressible Navier-Stokes operator. The IncompressibleNSOperator structure extends EvolutionIdentity with lattice topology, grid spacing $h > 0$, and viscosity $ν > 0$. MonotonicityCert packages such an operator with the property that its $dJdt$ is nonpositive.
proof idea
The definition is a one-line wrapper that applies the theorem dJcost_dt_nonpos_of_operator to the supplied operator $ns$, setting the nonpositive_derivative field of the MonotonicityCert structure.
why it matters
This declaration completes the existence of a monotonicity certificate for the concrete lattice NS operator, closing the bookkeeping part of the monotonicity program. It confirms that the operator-derived pair budget is absorbed by viscosity, leaving open only the PDE question of verifying the operator inequalities packaged in DiscreteNSOperator.IncompressibleNSOperator. In the Recognition framework it supports J-cost monotonicity for discrete fluid models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.