Thank you apeiron for your interest. I'll try and give a brief overview.
I see QM as an applied mathematics which is a semantic theory. I set formalism of Wave Mechanics within Mathematical Logic by making it a first-order theory [nothing to do with approximation methods].
This places the Field Axioms as axiomatic over all scalar components of all mathematical objects in the theory. Due to Soundness and Completeness, theorems of Model Theory, there is an excluded middle of propositions that are mathematically undecidable with respect to the Field Axioms. If the square root of minus one is logically independent of the Field Axioms, the proposition of this square root's existence falls into this excluded middle.
In re-writing formalism of Wave Mechanics as a first order theory, introduction of the imaginary unit can be postponed by replacing it by a bound variable until a certain step in the derivation of the theory. That point is normalisation; and the reason that the imaginary unit is needed there is that the theory requires products between vectors in an orthogonal space. In fact, it is these products that assume existence of the square root of minus one. [ Baylis, W.E., Huschilt, J. and Jiansu Wei (1991) Why i?
American Journal of Physics 1992 60/9, pp788-797 ] Baylis et.al demonstrate this for 3space but do not seem to realize it applies to infinite dimensional spaces.
Requiring the introduction of the square root's existence at this stage establishes its logical independence of the Field Axioms. The fundamental mathematical undecidability, here, is the existence of the products of orthogonal vectors, rather than existence of the imaginary unit.
Such undecidabilty is within any theory of quantum physics that relies on such products, not only Wave Mechanics.