The unconditional upper bound

The Chebyshev estimates discharge every field of the prime-counting input.

theorem RunsOfMultiples.primeInput : ∃ (C₁ : ℝ) (q₀ : ℕ), PrimeInput 4 (Real.log 2 / 2) C₁ q₀

The prime-number input for the upper bound, with K = 4.

theorem RunsOfMultiples.upper_bound : ∃ (C : ℝ) (N : ℕ), ∀ (S : Finset ℕ), (∀ a ∈ S, 0 < a) → N ≤ S.card → ↑(∑ a ∈ S, kVal S a) ≤ C * ↑S.card * Real.log ↑S.card * Real.log (Real.log ↑S.card)

Upper bound. ∑_{a ∈ S} k(a) = O(n log n log log n) for sets S of n positive integers.