viscous_dominates_of_product_bound
plain-language theorem explainer
The inequality mu ≤ nu / h² holds for real parameters whenever h exceeds zero and the product mu h² stays at most nu. Discrete Navier-Stokes modelers cite the bound to guarantee viscous dissipation outpaces stretching in vortex estimates. The tactic proof unfolds the rate definition, records positivity of h squared, and rewrites via the division lemma.
Claim. Let ν, h, μ ∈ ℝ with h > 0 and μ h² ≤ ν. Then μ ≤ ν / h².
background
The NavierStokes.VortexStretching module supplies analytic controls that close three gaps left by earlier sorry markers, drawing on finite-volume rigidity results and the uniqueness of the canonical reciprocal cost. Here viscousRate is the dissipation scale ν / h² for mesh length h. The coefficient mu enters as the scalar in the quadratic projector relation A² = μ A from the Cost.Ndim.Projector definition.
proof idea
The tactic unfolds viscousRate, adds the positivity fact (0 : ℝ) < h², and applies rwa with le_div_iff₀ to rearrange the product bound directly into the target inequality.
why it matters
The result anchors the sub-Kolmogorov absorption step in the vortex-stretching chain, ensuring the viscous term dominates under the stated product constraint. It forms part of the zero-sorry replacement for earlier analytic gaps referenced in the module header and feeds sibling statements on total viscous nonpositivity and exponential vorticity decay. The bound aligns with the Recognition Science treatment of dissipation scales in the eight-tick octave setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.