This is very interesting. What happens if you keep pulling the thread and construct large theories on such abstraction-layer-breaking theorems? Would we arrive at interesting things like pulling the thread on sqrt(-1) for imaginary numbers? Or is it somehow “undefined behavior”, quirks of the various implementation substrates of abstract mathematics that should be (informally) ignored? My gut says the former.

Are the various alternative axiomatic foundations also equivalent at this level or not? I suppose they are since they can implement/emulate each other, not sure.