transport_term_cancels
plain-language theorem explainer
The declaration states that a vanishing total transport contribution remains zero. Researchers decomposing the J-cost derivative into transport, viscous, and stretching pieces on a finite lattice cite this identity to close the transport-cancellation case. The proof is a one-line term that returns the supplied hypothesis without further steps.
Claim. Let $c$ be contribution fields on a lattice with $N$ sites. If the sum of the transport components equals zero, then the sum of the transport components equals zero.
background
The Discrete Vorticity module supplies exact bookkeeping for finite vorticity fields on a lattice window. It records totals, RMS squares, and normalized amplitudes while separating transport, viscous, and stretching contributions that appear in the J-cost derivative identity. The module doc-comment states that hard PDE inequalities are kept separate so they can be added one lemma at a time.
proof idea
The proof is a one-line term-mode wrapper that returns the hypothesis htransport directly.
why it matters
This identity closes the transport-cancellation case inside the discrete vorticity bookkeeping that supports the J-cost monotonicity program. It lets the derivative decomposition proceed by cases on the three contribution totals. The module keeps the algebraic surface separate from the analytic inequalities that remain to be proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.