normalized_vorticity_bounded
plain-language theorem explainer
The theorem shows that the normalized vorticity sequence remains bounded by 1 at every index. Researchers extracting ancient solutions from hypothetical Navier-Stokes blowups would cite this when rescaling a diverging sequence of sup-norms. The proof is a direct specialization of the general normalized_le_one lemma to the vorticity sequence under the given positivity assumption.
Claim. Let $M : ℕ → ℝ$ be a sequence of positive real numbers representing successive sup-norms of vorticity. For each $n ∈ ℕ$, the normalized term $M(n) / runningMax(M)(n)$ satisfies $M(n) / runningMax(M)(n) ≤ 1$.
background
The module formalizes running-max normalization for the Navier-Stokes regularity argument. Given a sequence of times $t_n → T^*$ and sup-norms $M_n = ‖ω(·,t_n)‖{L^∞}$ with $M_n → ∞$, the running maximum is the monotone envelope $M̃(t) = sup{s ≤ t} M(s)$. The normalized field is then defined pointwise as the original divided by this envelope, yielding a scale-invariant sequence whose $L^∞$ norm is at most 1 by construction. This step relies only on monotone sequence properties and is standard in the Caffarelli-Kohn-Nirenberg and Escauriaza-Seregin-Šverák literature.
proof idea
The proof is a one-line wrapper that applies the upstream lemma normalized_le_one to the concrete sequence M, instantiating the positivity hypothesis at the index n.
why it matters
This declaration supplies the uniform bound required for the normalized sequence, which is invoked directly by the parent theorem normalized_bounded to assert the bound for all n. It implements the scale-invariant extraction step in the Navier-Stokes paper §3, Step 1, aligning with the Recognition Science forcing chain that reduces regularity questions to self-similar fixed points and bounded ancient elements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.