normalized_vorticity_bounded
plain-language theorem explainer
The theorem shows that for any positive sequence M the normalized version obtained by dividing each term by the running maximum up to that index stays at most 1. Navier-Stokes analysts working on blow-up criteria cite it to guarantee that rescaled vorticity fields remain bounded after running-max normalization. The proof is a direct one-line application of the general normalized_le_one lemma to the given sequence and index.
Claim. Let $M : ℕ → ℝ$ satisfy $M(n) > 0$ for every $n$. Let runningMax$(M)(n)$ denote the supremum of $M(k)$ for $k ≤ n$. Define the normalized sequence by normalized$(M,n) = M(n) /$ runningMax$(M)(n)$. Then normalized$(M,n) ≤ 1$ for all $n$.
background
The module formalizes the running-max normalization step in the Navier-Stokes regularity argument (NS Paper §3, Step 1). Given a hypothetical blow-up sequence of sup-norms $M_n = ‖ω(·,t_n)‖{L^∞}$ with $M_n → ∞$, the running maximum runningMax$(M)(n) = sup{k≤n} M(k)$ produces the normalized fields normalized$(M,n) = M(n) /$ runningMax$(M)(n)$. By construction these satisfy the scale-invariant bound ‖ω̃_n‖ ≤ 1. The upstream lemma normalized_le_one states that normalized$(a,n) ≤ 1$ whenever $0 < a(n)$, proved by unfolding the definition and applying the inequality runningMax$(a,n) ≥ a(n)$ together with positivity of the running maximum.
proof idea
Term-mode one-line wrapper. It instantiates the upstream theorem normalized_le_one on the concrete sequence M at index n, supplying the positivity witness hpos n directly as the required hypothesis.
why it matters
The result is invoked by the downstream theorem normalized_bounded, which lifts the pointwise bound to a uniform statement ∀n, normalized M n ≤ 1. It completes the first step of the running-max construction used to extract ancient solutions from a blowing-up sequence. Within the Recognition Science framework this supports the scale-invariant analysis required for the Navier-Stokes regularity claim, consistent with the standard Caffarelli-Kohn-Nirenberg approach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.