total_viscous_nonpos
plain-language theorem explainer
The result shows that any scalar field on a finite lattice that is non-positive at every point has a non-positive sum. Analysts bounding viscous dissipation in discrete Navier-Stokes models cite this when establishing sign control on energy sinks. The proof reduces immediately to the standard non-positivity of finite sums once the total operator is unfolded.
Claim. Let $N$ be a natural number and let $f :$ Fin $N$ $→$ ℝ satisfy $f(i) ≤ 0$ for every site $i$. Then the sum of $f$ over all sites is ≤ 0.
background
The module supplies zero-sorry estimates for vortex stretching and viscous dissipation in a discrete Navier-Stokes setting, drawing on finite-volume rigidity results from Thapa & Washburn (J. Math. Phys. 2026) and related uniqueness and comparison papers. The total operator is defined as the sum of a scalar field over the finite lattice window of sites. The theorem applies this operator to a viscous field whose pointwise values are controlled by the non-positivity hypothesis.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the total definition to a Finset sum and applies the library fact that a pointwise non-positive function on a finite set has non-positive sum.
why it matters
This supplies the sign control on the integrated viscous term required by the sub-Kolmogorov domination arguments that follow in the same module. It closes one of the three analytic gaps listed in the module header and supports the discrete energy estimates feeding the finite-volume rigidity claims of the cited 2026 papers. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.