The zero datum has a global Leray–Hopf solution

The zero field with zero weak gradient satisfies the source-facing finite-time and global Leray–Hopf predicates.

theorem CKN.isInJ_zero : IsInJ fun (x : Foundation.Parabolic.Vec3) => 0

The zero datum belongs to the source space J.

theorem CKN.isLerayHopfSolution_zero (T : ℝ) (hT : 0 < T) : IsLerayHopfSolution T (fun (x : Foundation.Parabolic.Vec3) => 0) (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) fun (x : Foundation.Parabolic.ParabolicPoint) => 0

The zero fields satisfy the finite-time Leray–Hopf predicate.

theorem CKN.isGlobalLerayHopfSolution_zero : IsGlobalLerayHopfSolution (fun (x : Foundation.Parabolic.Vec3) => 0) (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) fun (x : Foundation.Parabolic.ParabolicPoint) => 0

The zero fields give a global Leray–Hopf solution for zero data.