dJdt_eq_viscous_plus_stretching
plain-language theorem explainer
When the total transport contribution to the J-cost derivative vanishes, the derivative equals the sum of the viscous and stretching contributions. Researchers deriving monotonicity bounds for discrete Navier-Stokes models in the Recognition Science framework cite this identity to simplify derivative expressions before applying absorption conditions. The proof is a one-line algebraic reduction that substitutes the EvolutionIdentity split, cancels the transport term, and applies zero_add.
Claim. Let $e$ be an EvolutionIdentity recording an exact split of the J-cost derivative on a lattice with $siteCount$ sites. If the total transport contribution of $e$ vanishes, then the J-cost derivative equals the sum of the total viscous contribution and the total stretching contribution.
background
The Discrete Vorticity module supplies exact bookkeeping objects for finite vorticity fields on a lattice window. It defines total, RMS, and normalized amplitudes together with separate transport, viscous, and stretching contribution fields. EvolutionIdentity is the structure that packages these fields with the J-cost derivative and the exact decomposition dJdt = totalTransport + totalViscous + totalStretching. The module deliberately isolates this algebraic surface from the hard PDE inequalities so that monotonicity lemmas can be added incrementally. The proof relies on the zero_add theorem from the arithmetic foundations.
proof idea
The proof is a one-line wrapper. It rewrites using the split field of the EvolutionIdentity structure, substitutes the hypothesis that totalTransport equals zero, and applies zero_add to drop the remaining zero term.
why it matters
The identity is invoked directly by dJdt_nonpos_of_transport_cancel_and_absorption to conclude that the derivative is nonpositive once stretching is absorbed by viscosity. It therefore supplies the algebraic step needed for the J-cost monotonicity program inside the discrete vorticity bookkeeping layer. This layer supports the broader Recognition Science effort to obtain Navier-Stokes behavior from exact functional identities rather than from continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.