Nice work including the axiom of choice in there.

FWIW it's hard to imagine the mind that wouldn't believe in the axiom of choice but would believe in .999 == 1 being a good phrase to use; that person would probably say

- 'I have a procedure for constructing a # arbitrarily close to 1, and if you tell me how close to 1 you want it i'll tell you how many steps of my procedure you need to execute'