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

Homomorphisms out of a complete ordered field are order-preserving

Statement

Let $F$ be a complete ordered field and $G$ an ordered field, and let $\varphi : F \to G$ be a field homomorphism (Field homomorphism and embedding). Then $\varphi$ is injective and order-preserving: $x > 0$ in $F$ implies $\varphi(x) > 0$ in $G$ , and consequently $a < b$ implies $\varphi(a) < \varphi(b)$ .

Facts & Assumptions

Given: A complete ordered field $F$ , an ordered field $G$ , and a field homomorphism $\varphi : F \to G$ .

[L1]

$\varphi(1_F) = 1_G$ , $\varphi(x + y) = \varphi(x) + \varphi(y)$ , $\varphi(xy) = \varphi(x)\varphi(y)$ , $\varphi(-x) = -\varphi(x)$ ; and every field homomorphism is injective, its kernel being an ideal of the field $F$ with $\varphi(1_F) = 1_G \ne 0_G$ (Field homomorphism and embedding).

[L2]

In a complete ordered field every $a \ge 0$ is a square $a = y^2$ ; the positive elements are exactly the nonzero squares (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ ).

[L3]

In any ordered field a nonzero square is positive: $y \ne 0 \Rightarrow y^2 > 0$ (Squares of nonzero elements are positive).

[L4]

Order via the positive cone: $x > 0$ means $x \in P$ , $a < b$ means $b - a \in P$ ; trichotomy holds (Ordered field).

Proof

technique · direct

1.1

$\varphi$ is injective: by [L1] its kernel is an ideal of the field $F$ , and since $\varphi(1_F) = 1_G \ne 0_G$ the kernel is $\{0_F\}$ .

1.2

Fix $x \in F$ with $x > 0$ ; then $x \ge 0$ , so by [L2] there is $y \in F$ with $x = y^2$ , and $y \ne 0$ since $y = 0$ would give $x = 0$ , against $x > 0$ by [L4].

L2L4

2.1

Applying $\varphi$ , $\varphi(x) = \varphi(y^2) = \varphi(y)^2$ , and $\varphi(y) \ne 0_G$ because $y \ne 0$ and $\varphi$ is injective.

step 1.1step 1.2L1

3.1

By [L3] in $G$ , the nonzero square $\varphi(y)^2$ is positive, so $\varphi(x) = \varphi(y)^2 > 0$ ; as $x > 0$ was arbitrary, $x > 0 \Rightarrow \varphi(x) > 0$ for all $x \in F$ .

step 2.1L3

4.1

If $a < b$ then $b - a > 0$ , so $\varphi(b - a) > 0$ ; since $\varphi(b - a) = \varphi(b) - \varphi(a)$ by [L1], we get $\varphi(b) - \varphi(a) > 0$ , i.e. $\varphi(a) < \varphi(b)$ .

step 3.1L1L4

5.1

Hence $\varphi$ is an injective, order-preserving field homomorphism.

step 1.1step 4.1∎

Depends on

Used by

A field homomorphism of ordered fields need not preserve order Counterexample
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: 13 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)
M. Spivak, Calculus, 4th ed., Ch. 8 (standard reference, not scraped)