Very sound. One formal model of complex numbers is R[i]/(i^2 + 1), which means all real polynomials in the variable i (R[i]) after "simplifying" (/) by taking

Very sound. One formal model of complex numbers is R[i]/(i^2 + 1), which means all real polynomials in the variable i (R[i]) after "simplifying" (/) by taking i^2 + 1 = 0 (equivalently i^2 = -1)... which is exactly the process you are describing.