TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every complex number has a square root, by an explicit Cartesian formula

Statement

Every $z = a + b i \in C$ has a square root. If $b \neq 0$ , one square root is $u + v i, u = \sqrt{\frac{∣ z ∣ + a}{2}}, v = \frac{b}{2 u} .$ If $b = 0$ , one may take $\sqrt{a}$ when $a \geq 0$ , and $i \sqrt{- a}$ when $a < 0$ .

Facts & Assumptions

Given: A complex number $z = a + b i$ .

[F1]

$∣ z ∣ = \sqrt{a^{2} + b^{2}}$ (Real and imaginary parts, complex conjugation, and modulus), and hence $∣ z ∣^{2} = a^{2} + b^{2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F2]

The real numbers are a complete ordered field (The Cauchy-sequence reals have the least-upper-bound property), so every nonnegative real has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[F3]

The real numbers form an ordered field (The reals form a totally ordered field).

[F4]

Squaring is order-preserving and order-reflecting on nonnegative elements (Squaring is monotone on the nonnegatives).

[F5]

Complex multiplication is $(a + b i) (u + v i) = (a u - b v) + (a v + b u) i$ ( $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

Proof

technique · cases

1.1

Suppose $b = 0$ and $a \geq 0$ . Then [F2] gives $(\sqrt{a})^{2} = a = z$ .

assume-case nonnegativeF2

1.2

Suppose $b = 0$ and $a < 0$ . Then [F2] gives $(i \sqrt{- a})^{2} = a = z$ .

assume-case negativeF2F3algebra

1.3

Suppose $b \neq 0$ . Then $b^{2} > 0$ , so [F1] gives $∣ z ∣^{2} > a^{2}$ . If $a \geq 0$ , [F4] yields $∣ z ∣ > a$ ; if $a < 0$ , it yields $∣ z ∣ > - a$ . In either case $∣ z ∣ + a > 0$ .

assume-case nonzeroF1F3F4

2.1

By [F2], $u = \sqrt{(∣ z ∣ + a) / 2}$ exists and is positive; hence $v = b / (2 u)$ is defined.

F2F3step 1.3

3.1

From $4 u^{2} = 2 (∣ z ∣ + a)$ and [F1], $v^{2} = \frac{b^{2}}{4 u^{2}} = \frac{∣ z ∣^{2} - a^{2}}{2 (∣ z ∣ + a)} = \frac{∣ z ∣ - a}{2} .$

F1step 2.1algebra

4.1

Therefore $u^{2} - v^{2} = a$ and $2 u v = b$ , so coordinate multiplication gives $(u + v i)^{2} = a + b i = z$ .

F5step 2.1step 3.1algebra

5.1

The cases $b = 0$ with $a \geq 0$ , $b = 0$ with $a < 0$ , and $b \neq 0$ are exhaustive, so every complex number has a square root.

step 1.1step 1.2step 4.1cases-exhaustive∎

Depends on

Used by

The square roots of i are ±(1+i)/√2 Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 49 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

R. K. Srivastava, Complex Analysis lecture notes (standard reference, not scraped)