totalViscous
plain-language theorem explainer
totalViscous sums the viscous component of a contribution field over the finite lattice sites. Researchers proving monotonicity of the J-cost for discrete Navier-Stokes flows cite it when isolating the dissipative term in the derivative identity. The definition is a direct one-line application of the total summation operator to the viscous field.
Claim. Let $c$ be a contribution field on a lattice with $N$ sites. The total viscous contribution is defined by $totalViscous(c) := sum_{i=1}^N c_{viscous}(i)$.
background
The DiscreteVorticity module supplies exact bookkeeping objects for the J-cost monotonicity program on finite lattices. ContributionFields is the structure holding three scalar fields (transport, viscous, stretching) indexed by Fin siteCount. The total operator sums any such field by direct summation over the index set.
proof idea
One-line wrapper that applies total to the viscous component of the input ContributionFields structure.
why it matters
This definition supplies the viscous sum that appears in downstream absorption theorems such as core_pair_budget_absorbed and dJdt_eq_viscous_plus_stretching. It supports the exact decomposition of dJ/dt into transport (canceled), viscous, and stretching pieces, advancing the discrete Navier-Stokes monotonicity argument toward the continuous limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.