Exact leading term for the dimension root of the homogeneous Hilbert rank.

theorem CCDN.hypersurface_rank_root_bounds {r d M s : ℕ} (hrpos : 0 < r) (hdM : d ≤ M) (hr : s + (r + 1 + (M - d)).choose (M - d) = (r + 1 + M).choose M) : ↑d ^ (1 / ↑r) * (↑M - ↑d + 1) ≤ ↑r.factorial ^ (1 / ↑r) * ↑s ^ (1 / ↑r) ∧ ↑r.factorial ^ (1 / ↑r) * ↑s ^ (1 / ↑r) ≤ ↑d ^ (1 / ↑r) * (↑M + ↑r)

Taking the dimension root preserves the factorial leading coefficient.