Conditional blow-up and obstruction to continuous extension

The terminal inference of Proposition 11.7, independently of the claimed Navier--Stokes construction. Positive scales approaching zero and a nonzero limiting profile force divergent velocity norm under a negative real power. The resulting field cannot be bounded near, or continuously extended to, the endpoint. No existence theorem for the manuscript's profiles is assumed here.

theorem NavierStokes.BlowupImplication.negative_power_tendsto_atTop {ι : Type u_1} {l : Filter ι} {q : ι → ℝ} {A : ℝ} (hA : 0 < A) (hq : Filter.Tendsto q l (nhdsWithin 0 (Set.Ioi 0))) : Filter.Tendsto (fun (t : ι) => q t ^ (-A)) l Filter.atTop

A positive scale tending to zero has a divergent negative real power.

theorem NavierStokes.BlowupImplication.positive_profile_tendsto_atTop {ι : Type u_1} {l : Filter ι} {q error : ι → ℝ} {A E : ℝ} (hA : 0 < A) (hE : 0 < E) (hq : Filter.Tendsto q l (nhdsWithin 0 (Set.Ioi 0))) (herror : Filter.Tendsto error l (nhds 0)) : Filter.Tendsto (fun (t : ι) => q t ^ (-A) * (E + error t)) l Filter.atTop

The manuscript's positive scalar profile remains divergent with a vanishing relative error. The error is inside the factor multiplied by q ^ (-A).

theorem NavierStokes.BlowupImplication.norm_tendsto_atTop_of_profile_lower_bound {ι : Type u_1} {V : Type u_2} [NormedAddCommGroup V] {l : Filter ι} {q error : ι → ℝ} {v : ι → V} {A E : ℝ} (hA : 0 < A) (hE : 0 < E) (hq : Filter.Tendsto q l (nhdsWithin 0 (Set.Ioi 0))) (herror : Filter.Tendsto error l (nhds 0)) (hlower : ∀ᶠ (t : ι) in l, q t ^ (-A) * (E + error t) ≤ ‖v t‖) : Filter.Tendsto (fun (t : ι) => ‖v t‖) l Filter.atTop

A velocity norm bounded below by the positive leading profile diverges. This directly applies when the angular component has that leading term.

theorem NavierStokes.BlowupImplication.nonzero_profile_norm_tendsto_atTop {ι : Type u_1} {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter ι} {q : ι → ℝ} {error : ι → V} {profile : V} {A : ℝ} (hA : 0 < A) (hprofile : profile ≠ 0) (hq : Filter.Tendsto q l (nhdsWithin 0 (Set.Ioi 0))) (herror : Filter.Tendsto error l (nhds 0)) : Filter.Tendsto (fun (t : ι) => ‖q t ^ (-A) • (profile + error t)‖) l Filter.atTop

A vector-valued nonzero profile with a perturbation tending to zero also has divergent norm. This theorem needs no sign choice for a component.

theorem NavierStokes.BlowupImplication.no_eventual_bound_of_profile {ι : Type u_1} {V : Type u_2} [NormedAddCommGroup V] {l : Filter ι} [l.NeBot] {q error : ι → ℝ} {v : ι → V} {A E : ℝ} (hA : 0 < A) (hE : 0 < E) (hq : Filter.Tendsto q l (nhdsWithin 0 (Set.Ioi 0))) (herror : Filter.Tendsto error l (nhds 0)) (hlower : ∀ᶠ (t : ι) in l, q t ^ (-A) * (E + error t) ≤ ‖v t‖) : ¬∃ (M : ℝ), ∀ᶠ (t : ι) in l, ‖v t‖ ≤ M

Divergence rules out any eventual finite bound, not only a global bound.

theorem NavierStokes.BlowupImplication.no_continuous_extension_of_profile {ι : Type u_1} {X : Type u_2} {V : Type u_3} [TopologicalSpace X] [NormedAddCommGroup V] {l : Filter ι} [l.NeBot] {q error : ι → ℝ} {v : ι → V} {path : ι → X} {endpoint : X} {A E : ℝ} (hA : 0 < A) (hE : 0 < E) (hq : Filter.Tendsto q l (nhdsWithin 0 (Set.Ioi 0))) (herror : Filter.Tendsto error l (nhds 0)) (hlower : ∀ᶠ (t : ι) in l, q t ^ (-A) * (E + error t) ≤ ‖v t‖) (hpath : Filter.Tendsto path l (nhds endpoint)) : ¬∃ (extension : X → V), ContinuousAt extension endpoint ∧ ∀ᶠ (t : ι) in l, extension (path t) = v t

A continuous extension along a convergent path contradicts the profile lower bound. X may be spacetime and path may move towards the singular point.

theorem NavierStokes.BlowupImplication.remaining_time_tendsto (T : ℝ) : Filter.Tendsto (fun (t : ℝ) => T - t) (nhdsWithin T (Set.Iio T)) (nhdsWithin 0 (Set.Ioi 0))

The remaining-time scale T - t tends to zero through positive values as t approaches T from below.

theorem NavierStokes.BlowupImplication.finite_time_profile_tendsto_atTop {T A E : ℝ} {error : ℝ → ℝ} (hA : 0 < A) (hE : 0 < E) (herror : Filter.Tendsto error (nhdsWithin T (Set.Iio T)) (nhds 0)) : Filter.Tendsto (fun (t : ℝ) => (T - t) ^ (-A) * (E + error t)) (nhdsWithin T (Set.Iio T)) Filter.atTop

Finite-time version of the scalar asymptotic in Proposition 11.7.

theorem NavierStokes.BlowupImplication.controlling_quantity_tendsto_atTop {ι : Type u_1} {V : Type u_2} [NormedAddCommGroup V] {l : Filter ι} {q error quantity : ι → ℝ} {v : ι → V} {A E C : ℝ} (hA : 0 < A) (hE : 0 < E) (hC : 0 < C) (hq : Filter.Tendsto q l (nhdsWithin 0 (Set.Ioi 0))) (herror : Filter.Tendsto error l (nhds 0)) (hlower : ∀ᶠ (t : ι) in l, q t ^ (-A) * (E + error t) ≤ ‖v t‖) (hcontrol : ∀ᶠ (t : ι) in l, ‖v t‖ ≤ C * quantity t) : Filter.Tendsto quantity l Filter.atTop

Any size which controls the velocity norm by a fixed positive multiplicative constant must diverge as well. An actual Sobolev embedding estimate may be supplied as hcontrol; it is not proved here.

theorem NavierStokes.BlowupImplication.arbitrarily_large_near_time {V : Type u_1} [NormedAddCommGroup V] {v : ℝ → V} {error : ℝ → ℝ} {T A E : ℝ} (hA : 0 < A) (hE : 0 < E) (herror : Filter.Tendsto error (nhdsWithin T (Set.Iio T)) (nhds 0)) (hlower : ∀ᶠ (t : ℝ) in nhdsWithin T (Set.Iio T), (T - t) ^ (-A) * (E + error t) ≤ ‖v t‖) (δ : ℝ) (hδ : 0 < δ) (M : ℝ) : ∃ (t : ℝ), T - δ < t ∧ t < T ∧ M < ‖v t‖

Arbitrarily large velocities occur in every left neighborhood of the singular time, expressed without limit or boundedness notation.

theorem NavierStokes.BlowupImplication.concentrating_path_tendsto (T X : ℝ) : Filter.Tendsto (fun (t : ℝ) => (t, √(2 * X * (T - t)))) (nhdsWithin T (Set.Iio T)) (nhds (T, 0))

The manuscript's radial sampling curve reaches the singular spacetime point. The zero axial coordinate is suppressed from this pair.

theorem NavierStokes.BlowupImplication.not_continuousAt_concentrating_profile {V : Type u_1} [NormedAddCommGroup V] {T X A E : ℝ} {error : ℝ → ℝ} {field : ℝ × ℝ → V} (hA : 0 < A) (hE : 0 < E) (herror : Filter.Tendsto error (nhdsWithin T (Set.Iio T)) (nhds 0)) (hlower : ∀ᶠ (t : ℝ) in nhdsWithin T (Set.Iio T), (T - t) ^ (-A) * (E + error t) ≤ ‖field (t, √(2 * X * (T - t)))‖) : ¬ContinuousAt field (T, 0)

A field satisfying the profile lower bound along the explicit shrinking radial curve is discontinuous at the terminal spacetime point.