I now actually read this proof, and it sounds right to me, though I don't guarantee I haven't missed some exception.What confused me in the pub is, you use the axiom of choice to get a basis for R over Q. But don't you just need a basis over Q for the vector space generated by the fragment lengths you actually have, not over any possible irrationals? Isn't that just some subset of the fragment lengths, throwing away any non-linearly-independent ones?
Ah! Yes, good thought. And that vector space is finite-dimensional, because we have at most finitely many frag lengths, and hence we don't need AC to conclude that it has a basis. Well done.