> the Hilbert space is real-valued and therefore (a vector of) ℵ₁.

But cardinality of real numbers might not be ℵ₁. It's literally unprovable in ZFC.

I had to look this up, and if I understand right: yes, all that's certain is |ℝ| = ℵₖ, k≥1? If so, same point applies.