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 rationals form a field
Statement
with the operations of Arithmetic on the rationals is a field: a commutative ring with in which every nonzero element has a multiplicative inverse.
Facts & Assumptions
Given: Rationals with representatives , second components nonzero.
The operations are independent of representatives (Rational arithmetic is well defined).
is a commutative ring in which (The integers form a commutative ring; because in ).
has no zero divisors and admits cancellation (The integers have no zero divisors; multiplicative cancellation).
Proof
By [L1], each axiom may be verified on fixed representatives.
Associativity of : both and have representative .
Commutativity of : and are equal pairs.
Additive identity: .
Additive inverses: .
Associativity and commutativity of : and .
Multiplicative identity: ; and since .
Distributivity: has representative , while has representative ; cancelling the common nonzero factor these are equivalent.
Inverses: iff iff ; for , .
All field axioms hold: is a field.
Depends on
Used by
- A rational root of xᵏ = m is an integer: if k ≥ 1, m ∈ ℤ, x ∈ ℚ and xᵏ is the image of m, then x is the image of an integer Corollary
- A degree-four polynomial can be reducible over ℚ without having a rational root Counterexample
- An integer matrix of determinant 2 is invertible over ℚ but not over ℤ Example
- For any field F, (F, +) and (F ∖ {0}, ·) are abelian groups; in particular (ℚ, +), (ℚ ∖ {0}, ·), (ℝ, +) and (ℝ ∖ {0}, ·) Example
- Long division, the Euclidean algorithm and a Bézout identity in ℚ[x] Example
- No rational squares to 3 or to 6, and none cubes to 2: three instances of the rational-root corollary Example
- ℚ and ℝ are fields, hence commutative rings, integral domains and ordered rings, all of characteristic 0 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 2-adic absolute value gives an ultrametric on ℚ, in which every triangle is isosceles and every point of a ball is a centre Example
- The Cauchy sequences of rationals form a commutative ring that is not an integral domain: two eventually-constant sequences with disjoint supports multiply to zero Example
- The polynomial x²-2 is irreducible over ℚ Example
- Translation turns x⁴+1 into an Eisenstein polynomial Example
- ℤ sits inside ℚ as a subring that is not a subfield, so the inverse-closure clause of the subfield definition is doing work Example
- FALSE: in every ordered field a closed bounded set is compact, so Heine-Borel needs no completeness False statement
- FALSE: some rational number squares to 2 False statement
- For a positive cut A, the reciprocal A⁻¹ satisfies A · A⁻¹ = 1^* Lemma
- Null sequences are Cauchy Lemma
- The p-adic valuation extends to the nonzero rationals by vₚ(a/b) := vₚ(a) - vₚ(b) ∈ ℤ, independently of the representation; it satisfies vₚ(xy) = vₚ(x) + vₚ(y), and vₚ(x+y) ≥ min{vₚ(x), vₚ(y)} whenever x, y and x+y are nonzero Lemma
- The rational cuts embed densely in ℝ, preserving sums, products, 0, 1 and the order Lemma
- The rationals embed densely in the reals Lemma
- Cauchy sequences form a commutative ring Theorem
- Euler's product formula φ(n)=n∏_p∣ n(1-1/p)=∏_pᵏ∥ n(pᵏ-pᵏ⁻¹) for n≥1, stated through a finite injective list of its prime divisors Theorem
- Gauss lemma: primitive factorisations over ℚ can be cleared to primitive factorisations over ℤ Theorem
- Rational root theorem Theorem
- The Dedekind reals form a field Theorem
- The inclusion ℤ↪ℚ is monic and epic but neither surjective nor an isomorphism in Ring Theorem
- The rationals form a totally ordered field Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 27 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., §4.2 (standard reference, not scraped)
- Rational number — formal construction (Wikipedia) (standard reference, not scraped)