A classical comparison field with uniformly confined vorticity cannot agree with the maximal ordinary solution throughout a finite lifespan. The contradiction uses the proved Beale--Kato--Majda integral criterion.

Joint smoothness in the reference bounds spatial derivatives on every fixed compact spatial set and closed finite time interval, including time zero.

theorem Euler.EulerExistenceAndSmoothnessR3.spatial_fderiv_eq_within {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (x : EuclideanSpace ℝ (Fin 3)) (t : ℝ) (ht : 0 ≤ t) : fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) x = fderivWithin ℝ (Function.uncurry v) (Set.univ ×ˢ Set.Ici 0) (x, t) ∘SL ContinuousLinearMap.inl ℝ (EuclideanSpace ℝ (Fin 3)) ℝ

theorem Euler.EulerExistenceAndSmoothnessR3.spatial_fderiv_continuousOn {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) : ContinuousOn (fun (z : EuclideanSpace ℝ (Fin 3) × ℝ) => fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => v x z.2) z.1) (Set.univ ×ˢ Set.Ici 0)

theorem Euler.EulerExistenceAndSmoothnessR3.spatial_fderiv_bounded_on_compact {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (K : Set (EuclideanSpace ℝ (Fin 3))) (hK : IsCompact K) (T : ℝ) : ∃ (C : ℝ), ∀ x ∈ K, ∀ t ∈ Set.Icc 0 T, ‖fderiv ℝ (fun (x : EuclideanSpace ℝ (Fin 3)) => v x t) x‖ ≤ C

Joint smoothness bounds the actual spatial vorticity on every fixed compact spatial set and every closed finite time interval.

theorem Euler.EulerExistenceAndSmoothnessR3.vorticity_bounded_on_compact {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (K : Set EulerSmoothLimit.Space) (hK : IsCompact K) (T : ℝ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ Set.Icc 0 T, ∀ x ∈ K, ‖EulerMeanCutoffCurl.vectorCurl (fun (x : EulerSmoothLimit.Space) => v x t) x‖ ≤ M

theorem Euler.ComparatorBridge.finiteLifespan_contradiction_of_compact_vorticity {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : EulerOrdinarySobolev.FiniteLifespan A) {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 A.field v p) (K : Set EulerSmoothLimit.Space) (hK : IsCompact K) (hmatch : ∀ (t : L.Time), L.maximalVelocity t = fun (x : EulerSmoothLimit.Space) => v x ↑t) (hsupport : ∀ (t : L.Time), ∀ x ∉ K, EulerMeanCutoffCurl.vectorCurl (L.maximalVelocity t) x = 0) : False