Square roots in the complexification of a real closed field

The usual algebraic square-root formula uses only square roots of nonnegative elements of the base field. No completeness or Archimedean property is used.

Use open scoped TauCeti.RealClosure to synthesize the field instance on QuadraticAlgebra R (-1) 0 outside this namespace. The scope supplies Fact (¬ IsSquare (-1 : R)) from IsSemireal R, which activates Mathlib's quadratic-algebra field instance.

theorem TauCeti.RealClosure.instFactNotIsSquareNegOfNat_tauCeti {R : Type u_1} [Ring R] [IsSemireal R] : Fact ¬IsSquare (-1)

In a formally real ring, -1 is not a square. This supplies the square obstruction used by the quadratic-algebra field instance.

theorem TauCeti.RealClosure.exists_nonneg_sq {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {a : R} (ha : 0 ≤ a) : ∃ (r : R), 0 ≤ r ∧ r ^ 2 = a

Every nonnegative element of an ordered real closed field has a nonnegative square root.

theorem QuadraticAlgebra.isSquare {R : Type u_1} [Field R] [IsRealClosed R] (z : QuadraticAlgebra R (-1) 0) : IsSquare z

Every element of R[i] is a square when R is real closed, without choosing an order.