Growth: the three prime ranges K/400 < p ≤ K/20, K/20 < p ≤ K/3, K/3 < p ≤ 2h

theorem Zeta5Irrational.floor_Kr_div (n d : ℕ) (_hd : 0 < d) : ⌊Kr n / ↑d⌋₊ = 40 * n / d

theorem Zeta5Irrational.floor_Kr_outer (n : ℕ) : ⌊Kr n / (20 / 37)⌋₊ = 74 * n

Bounds on the additive constants

theorem Zeta5Irrational.Bmax_le {n p Q : ℕ} (hq : 40 * n / p ≤ Q) : Bmax n p ≤ (5 * ↑Q + 10) * (3 * ↑Q + 6)

theorem Zeta5Irrational.ktop_sub_klo (n p : ℕ) : ↑(ktopI n p - kloI n p) = 10 * ↑(40 * n / p) + 26

theorem Zeta5Irrational.Ctail_le {n p : ℕ} (hp : 0 < p) (hq : 40 * n / p < 400) (hn : ↑n ≤ 10 * ↑p) : Ctail n p ≤ 10 ^ 7

theorem Zeta5Irrational.Ctab_le {n p : ℕ} (hq : 40 * n / p ≤ 20) {k : ℤ} (hk1 : kloI n p ≤ k) (hk2 : k ≤ ktopI n p) : Ctab n p k ≤ 10 ^ 8

theorem Zeta5Irrational.Cout_le {n p : ℕ} (hq : 40 * n / p ≤ 2) : Cout n p ≤ 10 ^ 5