ContributionFields
plain-language theorem explainer
ContributionFields packages three real-valued maps on a finite index set of size siteCount to separate transport, viscous, and stretching pieces in the J-cost derivative. Researchers on the discrete vorticity bookkeeping layer cite it when splitting dJ/dt exactly before applying sign lemmas. The declaration is a bare structure definition that introduces the three component fields with no further computation.
Claim. Let $N$ be a natural number. A ContributionFields structure on $N$ sites consists of three maps $T, V, S :$ Fin$(N) → ℝ$ that record the transport, viscous, and stretching contributions at each lattice site.
background
The DiscreteVorticity module supplies the discrete objects required for the J-cost monotonicity program. It isolates finite vorticity fields on a lattice window together with total, RMS, and normalized amplitudes. The three contribution fields allow an exact decomposition of the J-cost time derivative into transport, viscous, and stretching pieces, keeping the hard PDE inequalities separate for later lemmas.
proof idea
The declaration is a direct structure definition that introduces the three fields transport, viscous, and stretching without any further computation or proof obligations.
why it matters
This structure supplies the data type used by EvolutionIdentity to record an exact J-cost derivative split. It supports the subsequent lemmas that establish nonnegativity of the stretching term and cancellation properties of the transport and viscous terms. In the Recognition framework it advances the bookkeeping layer that isolates the monotonicity argument for the discrete Navier-Stokes system, consistent with the convex J-cost minimization and the eight-tick local dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.