totalStretching
plain-language theorem explainer
The total stretching contribution sums the stretching vector of a contribution field over the finite lattice sites. Discrete Navier-Stokes monotonicity proofs cite this when splitting the J-cost time derivative after transport cancellation. It is realized as a direct one-line wrapper around the total summation operator applied to the stretching component.
Claim. For a contribution field $c$ on $N$ sites, the total stretching equals the sum over all sites of the stretching component: $c = (c_1, c_2, c_3)$ where $c_3$ is the stretching vector, then total stretching is $c_3$ summed over the $N$ sites.
background
The DiscreteVorticity module supplies exact bookkeeping for finite vorticity fields on a lattice window, separating totals of transport, viscous, and stretching contributions that decompose the J-cost derivative. ContributionFields is the structure holding three vectors (transport, viscous, stretching), each a map from Fin siteCount to reals. The total function sums any scalar field over the finite set of sites.
proof idea
One-line wrapper that applies the total summation operator to the stretching field of the input ContributionFields structure.
why it matters
This supplies the stretching total used in downstream results such as core_stretching_absorbed and dJdt_nonpos_of_transport_cancel_and_absorption, which establish absorption by viscosity and nonpositive J-cost evolution. It fills the bookkeeping role in the Navier-Stokes monotonicity program, separating exact identities from inequalities. In the Recognition framework it supports the J-cost derivative split that feeds monotonicity arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.