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 reals form a totally ordered field
Statement
The relation of Order on the reals is well defined and makes (The reals form a field) a totally ordered field.
Facts & Assumptions
Given: Reals with representatives .
A sequence of rational numbers is null if, for every rational , there is such that for every (Null sequence).
Ordered-field arithmetic in : ; sums and products of eventual lower bounds (The rationals form a totally ordered field).
Dichotomy for non-null Cauchy sequences: eventually or eventually (A non-null Cauchy sequence is eventually bounded away from zero, with constant sign).
is a field (The reals form a field).
In , iff a representative is null; so iff every representative is non-null (The real numbers).
Proof
Positivity is independent of the representative: if for and is null, then beyond some also , so : the defining property holds for with .
Trichotomy: if , any representative is non-null, so by the dichotomy either eventually ( positive) or eventually ( positive); the two exclude each other, and exactly one of positive, , positive holds.
Positives are closed under and : from and eventually, and eventually, with .
Consequently is a total order (trichotomy plus transitivity from closure under sums), compatible with addition (translation preserves the difference) and with multiplication by positives: is a totally ordered field.
Depends on
Used by
- ℝ((t⁻¹)) does not have the least-upper-bound property; its canonical naturals have no supremum Corollary
- The Cauchy-sequence reals have the least-upper-bound property Corollary
- Not every ordered field is Archimedean Counterexample
- The first quadrant of ℝ² contains 0 and is closed under addition and is not a linear subspace, since it is not closed under multiplication by -1 Counterexample
- The unrestricted nested interval property fails in ℝ((t⁻¹)) Counterexample
- For n≥1, the determinant over a commutative ring by the Leibniz formula, and |det A| for a real matrix Definition
- Real edge-weighted graphs, total tree weight and minimum spanning trees Definition
- The formal Laurent series ℝ((t⁻¹)): support bounded below, valuation, leading coefficient Definition
- Assuming the Axiom of Choice, compactness of [0,1] derived from the subbase lemma alone, using only the rays as a subbasis and the least upper bound property Example
- ℚ and ℝ are fields, hence commutative rings, integral domains and ordered rings, all of characteristic 0 Example
- ℚ(√2) carries exactly two distinct field orders, exchanged by the conjugation √2 ↦ -√2 Example
- ℝ ≈ P(ℕ) in ZF, by the Cantor set for one injection and by the cuts {q ∈ ℚ : q < x} for the other; so | ℝ | = 2^ℵ₀ under the Axiom of Choice Example
- ℝ as a vector space over ℚ has a basis, and every such basis is infinite; the existence proof exhibits none Example
- ℝ is a vector space over itself, over the embedded copy of ℚ by restriction of scalars, and over ℚ itself via the embedding Example
- ℝ with the half-open intervals [a,b) as a basis is not compact and, assuming the Axiom of Countable Choice, is Lindel"of, while its square is not Lindel"of, the antidiagonal being an uncountable closed discrete subspace Example
- The polynomial x²+1 is irreducible over ℝ Example
- The rational function field ℝ(t) ordered by the eventual sign is an ordered field, worked out Example
- ℝ((t⁻¹)) is a commutative ring: the product is a finite sum and both operations preserve support bounded below Lemma
- The Cauchy-sequence reals are Archimedean Lemma
- The rationals embed densely in the reals Lemma
- Valuation and leading coefficient in ℝ((t⁻¹)): v(fg) = v(f) + v(g), and the behaviour of v under sums Lemma
- A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism Theorem
- Equivalence of the Cauchy and Dedekind constructions of ℝ Theorem
- ℍ is a division ring that is not commutative, hence not a field: q⁻¹ = bar q / N(q) for q ≠ 0, while ij = k and ji = -k Theorem
- ℝ((t⁻¹)) is a field: every nonzero formal Laurent series is invertible Theorem
- ℝ((t⁻¹)) is an ordered field, ordered by the sign of the leading coefficient Theorem
- The complex numbers form a field, and every nonzero x+iy has inverse (x-iy)/(x²+y²) Theorem
- The reals are complete Theorem
Cited to discharge well-definedness by Order on the reals.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 34 results over 17 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
- T. Tao, Analysis I, 3rd ed., §5.4 (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
- L. S. Krapp, Constructions of the real numbers: a set theoretical approach (Oxford, 2014) (standard reference, not scraped)