normalized_vorticity_bounded
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove global regularity of the Navier-Stokes equations.
- Does not address whether blowup sequences exist.
- Does not supply convergence rates or compactness arguments beyond the bound.
- Does not extend the normalization to other function spaces or dimensions.
Lean usage
theorem normalized_bounded (M : ℕ → ℝ) (hpos : ∀ n, 0 < M n) : ∀ n, normalized M n ≤ 1 := fun n => normalized_vorticity_bounded M hpos nformal statement (Lean)
130theorem normalized_vorticity_bounded (M : ℕ → ℝ) (hpos : ∀ n, 0 < M n) (n : ℕ) :
131 normalized M n ≤ 1 :=
proof body
Term-mode proof.
132 normalized_le_one M n (hpos n)
133
134/-- The running maximum is the correct normalization: after normalizing,
135 the sequence no longer diverges. -/