Complex numbers in physics are both real (quantum states are inherently complex) and unreal (you can't measure them). It's entirely possible unmeasurable sets are the same. You can't create an unmeasurable chunk of a ball, but maybe dark energy is best modeled by a quantum Banach-Tarski process due to (I'm making this up) renormalization space being a nonmeasurable set or something. I think the question is not "is it real", but "is it useful". (From there you could go down the "maybe nothing is real, and useful is all there is" path).

I'm confused why the "mistake" is rejected, if it's a formally meaningful statement. What if you actually intended it? Would you have to find another proof assistant?