dJdt_nonpos_of_transport_cancel_and_absorption
plain-language theorem explainer
This theorem shows that the J-cost time derivative is nonpositive when the transport contribution vanishes exactly and stretching is absorbed by viscosity. Discrete Navier-Stokes analysts cite it to close the monotonicity argument for the discrete operator. The proof is a one-line wrapper that invokes the upstream viscous-plus-stretching identity and finishes with linear arithmetic.
Claim. Let $e$ be an EvolutionIdentity on a lattice of $siteCount$ sites whose split records $dJdt$ as the sum of total transport, total viscous, and total stretching contributions. If total transport equals zero and total stretching satisfies totalStretching$(e.contributions) ≤ -$totalViscous$(e.contributions)$, then $e.dJdt ≤ 0$.
background
The DiscreteVorticity module supplies exact bookkeeping for finite vorticity fields on a lattice window. It introduces ContributionFields together with the three total maps (totalTransport, totalViscous, totalStretching) and the EvolutionIdentity structure whose split axiom states that dJdt equals the sum of those three totals. The local setting isolates this algebraic decomposition so that PDE inequalities can be added later without disturbing the exact split.
proof idea
The proof applies the upstream theorem dJdt_eq_viscous_plus_stretching to the given EvolutionIdentity and the transport-zero hypothesis, replacing dJdt by the sum of viscous and stretching totals. It then invokes linarith on the absorption inequality to obtain nonpositivity.
why it matters
The declaration is called directly by core_dJdt_nonpos in DiscreteNSOperator and by dJcost_dt_nonpos_of_operator in JcostMonotonicity, both of which conclude that the discrete NS operator has nonincreasing J-cost once its pair budget is absorbed by viscosity. It therefore supplies the final bookkeeping step that converts the exact derivative split into a monotonicity statement, advancing the discrete approximation inside the Recognition Science J-cost program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.