Why the unrestricted complete-metric Baire theorem would overstate the choice cost here

The proof of A Banach space has no countably infinite Hamel basis does not need the full statement "every complete metric space is Baire". It only needs the separable complete-metric route, and that is exactly the distinction recorded in The Baire category theorem is four inequivalent statements over ZF ‡: over ZF, the separable theorem is choice free, whereas the unrestricted complete-metric theorem is equivalent to Dependent Choice.

That matters here because the countable Hamel basis already supplies an explicit countable dense set, namely the rational span of the basis. Using the sharper argument records the actual cost of the theorem proved on this page. Invoking the unrestricted theorem would still yield a correct proof of the Banach-space claim, but it would advertise a stronger choice principle than the written argument spends.