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 real numbers
Definition
The real numbers are the quotient ring
of the ring of Cauchy sequences (Cauchy sequences form a commutative ring) by the ideal of null sequences (Null sequences form an ideal). The class of is written . Each rational maps to the class of the constant sequence .
Remarks
- Two Cauchy sequences define the same real exactly when their difference is a null sequence.
- That is a field is The reals form a field ↗; its order is Order on the reals.
Depends on
Used by
- 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
- Limits and Cauchy sequences of reals Definition
- Metric space: d(x,y) = 0 iff x = y, symmetry, and the triangle inequality; pseudometric and ultrametric Definition
- Order on the reals Definition
- Sequences of reals: bounded, eventually, frequently, tails, subsequences Definition
- Series, partial sums, convergence and the sum, divergence, and the tail series Definition
- The complex numbers as ℝ², with their arithmetic, real embedding, and imaginary unit Definition
- The extended real line overlineℝ = ℝ ∪ {-∞, +∞}, its order, and the arithmetic that is left undefined Definition
- The formal Laurent series ℝ((t⁻¹)): support bounded below, valuation, leading coefficient Definition
- The quaternions ℍ: real quadruples with componentwise addition and an explicit multiplication formula matching the table on 1, i, j, k Definition
- ℝ ≈ 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
- The reals are the quotient of rational Cauchy sequences by the maximal ideal of null sequences Example
- The vector (1,2) ∈ ℝ² has coordinate list (1,2) in the standard ordered basis, (2,1) in its reversal, and (2,-1) in the ordered basis ((1,1),(1,0)) Example
- Every convergent sequence is Cauchy Lemma
- The rationals embed densely in the reals Lemma
- ℍ 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
- The reals are complete Theorem
- The reals form a field Theorem
- The reals form a totally ordered field Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 16 results over 12 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.3 (standard reference, not scraped)
- L. S. Krapp, Constructions of the real numbers: a set theoretical approach (Oxford, 2014) (standard reference, not scraped)