For the least cutoff $c(n)$ after which every $k$ occurs as the number of homothetic cubes in a decomposition of the unit $n$-cube, is $c(n) \gg n^n$? The Lean proof shows $c(n) = o(n^n)$ along odd dimensions.

What refuting $c(n)\gg n^n$ leaves open: give good bounds for $c(n)$. Asked here on the scale the problem itself sets, $n^n$: does $c$ have a well-defined order $$\lim_{n\to\infty}\frac{\log c(n)}{n\log n}?$$ The refuted conjecture would have forced this limit to be at least $1$.