ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.

The square roots of $i$ are $\pm (1 + i) / \sqrt{2}$

Example

The two square roots of $i$ are $\frac{1 + i}{\sqrt{2}} and - \frac{1 + i}{\sqrt{2}} .$

Facts & Assumptions

Given: The imaginary unit $i \in C$ .

[F1]

Complex multiplication satisfies $(a + b i)^{2} = (a^{2} - b^{2}) + 2 a b 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})$ ).

[F2]

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

[F3]

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

Verification

technique · direct

1.1

By [F1] and [F2], $((1 + i) / \sqrt{2})^{2} = i$ ; its negative has the same square.

F1F2algebra

1.2

Conversely, if $(a + b i)^{2} = i$ , [F1] gives $a^{2} = b^{2}$ and $2 a b = 1$ . Consequently $a, b \neq 0$ , they have the same sign, and $a = b$ .

F1algebra

2.1

Then $2 a^{2} = 1$ , so [F2] gives $a = b = 1 / \sqrt{2}$ or $a = b = - 1 / \sqrt{2}$ . These are exactly the two values in step 1.1.

F2step 1.2algebra

3.1

Thus the existence guaranteed abstractly by [F3] is realized by exactly the two displayed roots.

F3step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

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

The square roots of ii are ±(1+i)/2±(1+i)/2​