MonotonicityCert
plain-language theorem explainer
MonotonicityCert packages a concrete incompressible Navier-Stokes operator on a finite lattice together with the guarantee that its J-cost time derivative is nonpositive. Researchers working on discrete fluid models in Recognition Science cite this structure to certify monotonicity once viscosity absorbs the operator-derived stretching budget. The definition directly assembles the operator and the nonpositive derivative bound as a bookkeeping object.
Claim. A monotonicity certificate for a lattice with $N$ sites consists of an incompressible Navier-Stokes operator on that lattice together with the assertion that the time derivative of its J-cost satisfies $dJ/dt ≤ 0$.
background
The module closes bookkeeping for J-cost monotonicity on a concrete discrete incompressible Navier-Stokes operator. Transport cancellation follows from conservative incompressible flux; the stretching term is bounded by the operator's Recognition Composition Law pair budget; viscosity absorbs that budget, so the total J-cost derivative is nonpositive. What remains open is verification of the operator inequalities for the real lattice flow. IncompressibleNSOperator siteCount extends EvolutionIdentity siteCount with lattice topology, grid spacing h > 0 and viscosity ν > 0.
proof idea
This is a structure definition that packages the operator field and the nonpositive derivative property. It functions as a direct wrapper for downstream construction via dJcost_dt_nonpos_of_operator, with no additional lemmas or tactics required inside the structure itself.
why it matters
The structure closes the bookkeeping portion of the monotonicity program for the concrete lattice NS operator and feeds directly into the monotonicityCert definition. It implements the step in which viscosity absorbs the RCL-derived pair budget, leaving only the PDE question of operator inequalities. The construction aligns with Recognition Science landmarks on the Recognition Composition Law and J-cost monotonicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.