dJcost_dt_nonpos_of_operator
plain-language theorem explainer
The theorem shows that any concrete discrete incompressible Navier-Stokes operator on a finite lattice has nonincreasing total J-cost. Lattice fluid modelers in the Recognition Science program cite it to obtain packaged monotonicity certificates. The proof is a one-line term that feeds the operator's evolution identity, its zero-transport property, and its stretching-absorption bound into the general nonpositivity lemma for the J-cost derivative.
Claim. Let $ns$ be an incompressible Navier-Stokes operator on a lattice with $N$ sites. Then the time derivative of the total J-cost satisfies $ns.dJdt ≤ 0$.
background
The module closes the bookkeeping for J-cost monotonicity against a concrete discrete incompressible Navier-Stokes operator. An IncompressibleNSOperator extends EvolutionIdentity and carries lattice topology, grid spacing $h > 0$, and viscosity $ν > 0$. The total J-cost is assembled from the J-function applied to sitewise pair contributions, where J obeys the Recognition Composition Law. Upstream, dJdt_nonpos_of_transport_cancel_and_absorption states that if total transport vanishes and stretching is absorbed by viscosity then the derivative is nonpositive. operator_transport_zero confirms that conservative transport sums to zero, while stretching_absorbed_by_viscosity shows the lattice stretching contribution is bounded by the viscous budget via summed RCL pair bounds.
proof idea
The proof is a direct term application of dJdt_nonpos_of_transport_cancel_and_absorption. It supplies the evolution identity extracted from the operator via ns.toEvolutionIdentity, the zero total transport from operator_transport_zero ns, and the absorption inequality from stretching_absorbed_by_viscosity ns.
why it matters
This theorem supplies the nonpositive derivative component required by the monotonicityCert definition, which packages any such operator into a MonotonicityCert. It completes the three bookkeeping steps listed in the module documentation: transport cancellation from incompressible flux, stretching bounded by the operator's RCL pair budget, and absorption by viscosity. The remaining open question is verification of the concrete operator inequalities for the real lattice flow. It supplies a discrete analog of energy dissipation consistent with J-cost monotonicity in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.