lower bound for approximated times;

--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 30 14:02:52 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 30 14:08:21 2023 +0100
@@ -84,7 +84,7 @@
         val t_c =
           Timing_Data.median_time(for ((n, t) <- mono_prefix) yield t - t_p.scale(1.0 / n))
 
-        def model(threads: Int): Time = t_c + t_p.scale(1.0 / threads)
+        def model(threads: Int): Time = Time.ms((t_c + t_p.scale(1.0 / threads)).ms max 0)
 
         if (is_mono || in_prefix) model(threads)
         else {