totalTransport
plain-language theorem explainer
totalTransport sums the transport field of a ContributionFields record over the finite lattice sites. Workers on discrete Navier-Stokes J-cost monotonicity cite it when isolating the conservative flux term before cancellation arguments. The definition is a direct one-line application of the lattice summation operator to the transport component.
Claim. Let $c$ be a ContributionFields structure on a lattice with $N$ sites, containing transport, viscous, and stretching scalar fields. The total transport contribution is defined as the sum of the transport field: $T = ∑_{i=1}^N c.transport_i$.
background
ContributionFields packages three scalar fields (transport, viscous, stretching) on a finite lattice of siteCount sites; these fields appear in the exact decomposition of the J-cost time derivative. The total operator sums any such field over the Fin siteCount indices. The module supplies exact bookkeeping for discrete vorticity so that the J-cost derivative splits cleanly into the three pieces, with the hard inequalities deferred to later lemmas.
proof idea
one-line wrapper that applies the total summation operator to the transport component of the input ContributionFields structure.
why it matters
This supplies the transport total required by EvolutionIdentity and its consequences, including dJdt_eq_viscous_plus_stretching and dJdt_nonpos_of_transport_cancel_and_absorption. It isolates the structural cancellation of conservative transport flux, a prerequisite for showing nonpositive J-cost evolution once stretching is absorbed by viscosity. The bookkeeping supports the larger discrete Navier-Stokes monotonicity program before continuous limits are taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.