totalViscous
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove any inequality or sign property of the sum.
- Does not incorporate lattice spacing, viscosity coefficient, or topology.
- Does not address continuous limits or error budgets.
formal statement (Lean)
61def totalViscous {siteCount : ℕ} (c : ContributionFields siteCount) : ℝ :=
proof body
Definition body.
62 total c.viscous
63