Zero data and zero force satisfy the forced predicates

The zero force is square integrable on every slab and locally L^q for every exponent, and the zero fields form a forced Leray–Hopf solution with zero datum and zero force.

theorem CKN.isLocallySquareIntegrableForce_zero : IsLocallySquareIntegrableForce fun (x : Foundation.Parabolic.ParabolicPoint) => 0

The zero force is square integrable on every finite positive-time slab.

theorem CKN.isLocallyQIntegrableForce_zero (q : ℝ) : IsLocallyQIntegrableForce q fun (x : Foundation.Parabolic.ParabolicPoint) => 0

The zero force is locally L^q on every CKN local box, for every q.

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

The zero fields form a finite-time forced Leray–Hopf solution with zero datum and zero force.

theorem CKN.isGlobalForcedLerayHopfSolution_zero : IsGlobalForcedLerayHopfSolution (fun (x : Foundation.Parabolic.Vec3) => 0) (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) fun (x : Foundation.Parabolic.ParabolicPoint) => 0

The zero fields form a global forced Leray–Hopf solution.