LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

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.

Field homomorphisms between ordered fields fix $\mathbb{Q}$

Statement

Let $F$ and $G$ be ordered fields with canonical rational embeddings $\iota_F : \mathbb{Q} \to F$ and $\iota_G : \mathbb{Q} \to G$ (The unique embedding of ℚ into an ordered field). Then every field homomorphism $\varphi : F \to G$ (Field homomorphism and embedding) fixes $\mathbb{Q}$ , meaning $\varphi \circ \iota_F = \iota_G, \qquad \text{i.e. } \varphi(\iota_F(q)) = \iota_G(q) \text{ for all } q \in \mathbb{Q}.$

Facts & Assumptions

Given: Ordered fields $F, G$ , a field homomorphism $\varphi : F \to G$ , and the canonical embeddings $\iota_F, \iota_G$ .

[L1]

The canonical embedding $\iota : \mathbb{Q} \to F$ acts on $\mathbb{Z}$ by $n \mapsto n \cdot 1_F$ and on $\mathbb{Q}$ by $p/q \mapsto (p \cdot 1_F)(q \cdot 1_F)^{-1}$ (likewise for $\iota_G$ ) (The unique embedding of ℚ into an ordered field).

[L2]

The canonical natural $n \cdot 1$ is the $n$ -fold sum $1 + \dots + 1$ ; the integers embed with $q \cdot 1 \ne 0$ for $q \ne 0$ (Canonical naturals are positive and strictly increasing).

[L3]

$\varphi$ is a field homomorphism: $\varphi(1_F) = 1_G$ , $\varphi(x + y) = \varphi(x) + \varphi(y)$ , $\varphi(xy) = \varphi(x)\varphi(y)$ , $\varphi(0_F) = 0_G$ , $\varphi(-x) = -\varphi(x)$ , and $\varphi(x^{-1}) = \varphi(x)^{-1}$ for $x \ne 0$ (Field homomorphism and embedding).

Proof

technique · direct

1.1

By [L3], $\varphi(1_F) = 1_G$ and $\varphi$ preserves sums, products, negation, and inversion of nonzero elements.

1.2

By [L1], $\iota_F$ and $\iota_G$ send each $n \in \mathbb{Z}$ to $n \cdot 1_F$ and $n \cdot 1_G$ , and each $p/q \in \mathbb{Q}$ to $(p \cdot 1)(q \cdot 1)^{-1}$ in the respective field.

1.3

Because $n \cdot 1_F$ is the $n$ -fold sum of $1_F$ ([L2]) and $\varphi$ is additive with $\varphi(1_F) = 1_G$ , we get $\varphi(n \cdot 1_F) = n \cdot 1_G$ for every canonical natural $n$ .

L2L3

2.1

For each integer $n$ this extends by sign: $\varphi(\iota_F(0)) = \varphi(0_F) = 0_G = \iota_G(0)$ and $\varphi(\iota_F(-n)) = \varphi(-(n \cdot 1_F)) = -(n \cdot 1_G) = \iota_G(-n)$ , so $\varphi(\iota_F(m)) = \iota_G(m)$ for all $m \in \mathbb{Z}$ .

step 1.2step 1.3L3

3.1

For a rational $p/q$ with integers $p, q \ne 0$ , $\iota_F(p/q) = (p \cdot 1_F)(q \cdot 1_F)^{-1}$ , so $\varphi(\iota_F(p/q)) = \varphi(p \cdot 1_F)\,\varphi(q \cdot 1_F)^{-1} = (p \cdot 1_G)(q \cdot 1_G)^{-1} = \iota_G(p/q)$ .

step 1.2step 2.1L3

4.1

Since $\varphi \circ \iota_F$ and $\iota_G$ agree on every rational, $\varphi \circ \iota_F = \iota_G$ : the homomorphism $\varphi$ fixes $\mathbb{Q}$ .

step 3.1∎

Depends on

Used by

Uniqueness of the complete ordered field: ℝ up to a unique isomorphism Theorem

Dependency tree · next 3 levels

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

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed. (standard reference, not scraped)
University of Wisconsin Math 521 notes: Real analysis (standard reference, not scraped)

Field homomorphisms between ordered fields fix Q\mathbb{Q}Q