Arithmetic for the top-down communication exponent

With C = 32768*194^d, the choices epsilon = 1/(32*C) and N = (32*C)^d turn the finite 16*(C*(m+1))^d ≤ n obstruction into an Omega(n^(1/d)) message lower bound.

theorem Complexity.KarchmerWigderson.finite_budget_of_cost_internal {n d : ℕ} (hd : 0 < d) (hlarge : (32 * (32768 * 194 ^ d)) ^ d ≤ n) {m : ℝ} (hm : 0 ≤ m) (hcost : m ≤ ↑n ^ (↑d)⁻¹ / (32 * (32768 * 194 ^ d))) : 16 * (32768 * 194 ^ d * (m + 1)) ^ d ≤ ↑n