Exponentials of iterated-logarithmic budgets

A fixed polynomial in the ceiling logarithm is eventually smaller than its input, by Cslib's natural exponential-versus-polynomial theorem. Applying this at the input's ceiling logarithm shows that exponentiating any fixed iterated-logarithmic polynomial still gives a sublinear function. This keeps the unbounded Gamma candidate count, rather than replacing it by a fixed power of the original logarithm.

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_tendsto_clog : Filter.Tendsto (fun (n : ℕ) => Nat.clog 2 (n + 1)) Filter.atTop Filter.atTop

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_eventually_clog_pow_le (c d : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c * (Nat.clog 2 (n + 1) + 1) ^ d ≤ n

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_iterated_exp_isLittleO (c d : ℕ) : (fun (n : ℕ) => ↑(2 ^ (c * (Nat.clog 2 (Nat.clog 2 (n + 1) + 1) + 1) ^ d))) =o[Filter.atTop] fun (n : ℕ) => ↑n