This is really interesting. I'm not surprised by axiom of choice being based on real numbers. I've been thinking about that lately but I don't have a good intuition why. Do you have a link?
I'd be very surprised if it were true in general. But there certainly has to be some non-computational component to the reals being a complete totally ordered Archimedean field, because the question of deciding the equality of two reals is uncomputable, so there is no procedure to decide the total order.
