core_dJdt_nonpos
plain-language theorem explainer
The theorem establishes that the time derivative of the J-cost for any discrete incompressible Navier-Stokes flow encoded by a CoreNSOperator on a finite lattice is non-positive. Researchers deriving lattice fluid models or Recognition Science continuum limits from discrete operators would cite this monotonicity to confirm dissipation. The proof is a direct one-line application of the general dJdt non-positivity lemma once the core operator's transport cancellation and stretching absorption are supplied.
Claim. Let $op$ be a CoreNSOperator on a finite lattice with $siteCount$ sites. Then the time derivative of the J-cost of $op$ satisfies $dJ/dt(op) ≤ 0$.
background
CoreNSOperator is the structure carrying only the physical lattice data: a LatticeTopology, grid spacing $h>0$, viscosity $ν>0$, a divergence-free velocity field, and a conservative transport flux. It extends EvolutionIdentity and supplies the state evolution without presupposing pair-budget or absorption fields; those are derived downstream in the module. J-cost is the functional whose monotonicity is under study, built from the Recognition Science J-function that quantifies information or energy cost on the lattice. The result rests on two upstream theorems in the same module: core_transport_zero, which proves total transport vanishes because the flux is conservative on a finite set, and core_stretching_absorbed, which shows stretching is absorbed by viscosity via the derived pair budget.
proof idea
The proof is a one-line term wrapper that applies the lemma dJdt_nonpos_of_transport_cancel_and_absorption to the operator's evolution identity, the transport cancellation fact core_transport_zero, and the absorption fact core_stretching_absorbed.
why it matters
This theorem supplies J-cost monotonicity directly from the minimal CoreNSOperator data, completing a required dissipation step in the discrete Navier-Stokes construction. It aligns with the Recognition Science forcing chain by ensuring the J-functional decreases under the derived transport and stretching rules. No downstream uses are recorded, but the result supports stability arguments and potential passage to the continuous incompressible equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.