Logarithmic remainders in the cutwidth argument

Fixed logarithmic terms, including the integral ceiling logarithm in the finite graph bounds, can be absorbed in every positive linear slack.

theorem Algebraic.Cutwidth.eventually_mul_logb_add_lt (A B : ℝ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, A * Real.logb 2 ↑n + B < δ * ↑n

Every fixed multiple of the binary logarithm, plus a constant, is eventually below every positive multiple of the input.

theorem Algebraic.Cutwidth.eventually_clog_add_lt (B : ℝ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Nat.clog 2 n) + B < δ * ↑n

The ceiling binary logarithm plus a constant is eventually smaller than every positive linear function.