TheoremStatement: AI-adaptedProof: 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.

The only real-field automorphisms of $C$ are the identity and complex conjugation

Statement

Every field automorphism of $C$ that fixes $R$ pointwise is either the identity or complex conjugation, and these two automorphisms are distinct.

Facts & Assumptions

Given: A real-field automorphism $σ$ of $C$ .

[F1]

Every complex number has a unique form $a + b i$ , and $C$ is a field ( $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})$ ); $i^{2} = - 1$ (The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ ).

[F2]

Complex conjugation is an involutive real-field automorphism (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F3]

A square root of $- 1$ determines a unique real-field homomorphism from $C$ by the image of $i$ (A square root of $- 1$ in a real field extension determines a unique real-field homomorphism from $C$ ).

Proof

technique · direct

1.1

By [F1], $i^{2} = - 1$ ; since $σ$ is a field homomorphism fixing $- 1$ , applying it gives $σ (i)^{2} = - 1$ .

F1algebra

2.1

In the complex field, $t^{2} + 1 = (t - i) (t + i)$ ; hence a root has $t = i$ or $t = - i$ . Thus $σ (i) \in {i, - i}$ .

F1step 1.1algebra

3.1

If $σ (i) = i$ , uniqueness in [F3] makes $σ$ the identity. If $σ (i) = - i$ , [F2] and uniqueness in [F3] make $σ$ conjugation.

F2F3step 2.1

4.1

The two maps are distinct because they send $i$ to the distinct elements $i$ and $- i$ .

F1step 3.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 48 results over 9 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

J. S. Milne, Fields and Galois Theory (standard reference, not scraped)

The only real-field automorphisms of CC are the identity and complex conjugation