Foundations of the Real Numbers for Analysis

About this page

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.

✓ 35 results · all verified · 30 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

1 · Prerequisites

Real Analysis

Set Theory

2 · Logical flowchart

3 · Items

Definition

Foundations of the Real Numbers for Analysis

3 · Items

Field

Ordered field

Absolute value in an ordered field

Archimedean ordered field

Complete ordered field (least-upper-bound property)

Field homomorphism and embedding

Ordered-field isomorphism

Identities and inverses in a field are unique

Multiplication by zero: 0 · a = 0

Sign rules for products: (-a)b = -(ab) and (-a)(-b) = ab

(-1)(-1) = 1

A field has no zero divisors: ab = 0 ⟹ a = 0 or b = 0

Multiplicative cancellation: c ≠ 0 and ac = bc ⟹ a = b

Order is preserved by adding a constant and by adding inequalities

Sign rules for products and monotonicity of multiplication

Squares of nonzero elements are positive

The multiplicative identity is positive

Inverses of positives are positive, and reciprocation reverses order

Basic properties of the absolute value

The triangle inequality

The reverse triangle inequality

Squaring is monotone on the nonnegatives

Reciprocals and order: 1/r against 1

The sign of a product

Multiplying inequalities of positives

When ab < b for positive a, b

The canonical natural ι(n) = n · 1_F of a field

Canonical naturals are positive and strictly increasing

Every complete ordered field is Archimedean

For every ε > 0 in a complete ordered field there is a natural n ≥ 1 with 1/n < ε

The unique embedding of ℚ into an ordered field

ℚ is dense in every Archimedean ordered field

Square roots exist: a unique √a ≥ 0 with (√a)² = a; the positives are {x² : x ≠ 0}

Field homomorphisms between ordered fields fix ℚ

Homomorphisms out of a complete ordered field are order-preserving

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

The Cauchy-sequence reals are Archimedean

The Cauchy-sequence reals have the least-upper-bound property

Equivalence of the Cauchy and Dedekind constructions of ℝ

√2 exists in every complete ordered field, and is irrational

A field homomorphism of ordered fields need not preserve order

Not every ordered field is Archimedean

FALSE: there exist two non-isomorphic complete ordered fields