exponential_vorticity_decay
plain-language theorem explainer
Exponential vorticity decay shows that any vorticity function omega obeying an upper bound with a decaying exponential factor stays below its initial amplitude w0 at all later times, provided viscosity exceeds the mu threshold. Researchers modeling incompressible flows with vortex stretching would invoke this to close energy estimates. The argument is a short comparison: the exponential term is at most one, so the bound collapses to the initial value via order transitivity.
Claim. Let $nu, h, mu, w_0 in mathbb{R}$ with $w_0 geq 0$ and $mu leq nu / h^2$. Let $omega : mathbb{R} to mathbb{R}$. If $omega(t) leq w_0 exp(-(nu/h^2 - mu) t)$ for all $t geq 0$, then $omega(t) leq w_0$ for all $t geq 0$.
background
In the Navier-Stokes module on vortex stretching and viscous dissipation, mu is the scalar coefficient in the quadratic relation A squared equals mu A, drawn from the normalized projector in Cost.Ndim.Projector. The local theoretical setting replaces prior sorry markers with complete proofs that close analytic gaps from three papers: finite-volume rigidity, uniqueness of the canonical reciprocal cost, and coherent comparison. The proof applies the arithmetic transitivity result le_trans from Foundation.ArithmeticFromLogic, which establishes that if a leq b and b leq c then a leq c.
proof idea
The tactic proof introduces the time t and nonnegativity hypothesis, derives the gap nu over h squared minus mu nonnegative by linarith, shows the exponential is at most one by exp_le_one_iff and nlinarith on the product of the gap and t, then applies le_trans to the given ODE bound and the product inequality mul_le_of_le_one_right.
why it matters
This bound supports control of vorticity growth in the master absorption theorem, where the J-cost derivative is shown nonpositive when transport cancels and stretching is absorbed by viscosity. It fills an exponential decay step in the Navier-Stokes estimates referenced by the module's papers on finite-volume rigidity and canonical reciprocal cost. No open questions are directly touched as the result is fully proved with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.