Complex_Numbers_cannot_be_Ordered_Compatibly_with_Ring_Structure

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Complex_Numbers_cannot_be_Ordered_Compatibly_with_Ring_Structure is named for, so its Disproved status carries no information about it. Do not import it or use it as a dependency.

Let $\struct {\C, +, \times}$ be the field of complex numbers. There exists no total ordering on $\struct {\C, +, \times}$ which is compatible with the structure of $\struct {\C, +, \times}$.

Why this node was retired

The posted statement is

theorem Complex_Numbers_cannot_be_Ordered_Compatibly_with_Ring_Structure : ¬ ∃ (r : LinearOrder ℂ), True := by sorry

The goal is ¬ ∃ (r : LinearOrder ℂ), True, i.e. that ℂ carries no linear order at all. That is false: every set admits a linear order. What the name asserts — that no linear order on ℂ is compatible with its ring structure — is missing entirely, because the compatibility conditions never appear.

What a faithful statement would require

The order must be required to be compatible with the ring operations (0 < a → 0 < b → 0 < a * b and translation-invariance of <), for instance by ruling out a LinearOrderedField ℂ instance.

No corrected replacement node exists yet.