viscous_term_dissipative
plain-language theorem explainer
The declaration shows that the summed viscous contribution to the J-cost derivative stays nonpositive whenever each local viscous term is nonpositive. Researchers building discrete Navier-Stokes estimates inside the Recognition Science J-cost monotonicity program would cite it to control dissipation signs. The argument is a direct one-line reduction that unfolds the total and totalViscous definitions then applies the finite-sum nonpositivity fact.
Claim. Let $c$ be a contribution field on a finite lattice window of $n$ sites. If $c. viscous(i) ≤ 0$ for every site index $i$, then $∑_i c. viscous(i) ≤ 0$.
background
The DiscreteVorticity module packages exact bookkeeping for the J-cost monotonicity program. It works with finite vorticity fields on a lattice window, records total, RMS, and normalized amplitudes, and decomposes the J-cost derivative into transport, viscous, and stretching pieces. The hard PDE inequalities are kept separate so they can be added one lemma at a time, per the module documentation.
proof idea
The proof is a one-line term-mode wrapper. It unfolds totalViscous and total, then applies Finset.sum_nonpos to the hypothesis that every viscous component is nonpositive.
why it matters
This lemma supplies one sign-control direction required by the J-cost derivative identity inside the discrete vorticity bookkeeping. It ensures the viscous piece cannot raise the J-cost when local contributions are dissipative, supporting monotonicity arguments in the Recognition Science framework. No downstream uses appear yet, so the result functions as a foundational building block for later Navier-Stokes estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.