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.
Order on the rationals
Definition
Every rational has a representative with positive denominator (if then with , Every rational has a positive-denominator representative ↗). For representatives with and define
A rational is positive when ; on such representatives, exactly when .
Remarks
- Well-definedness, totality, and compatibility with the arithmetic: The rationals form a totally ordered field.
- The integer order used on the right is Order on the integers.
Depends on
Used by
- Lipschitz map, α-Hölder map for rational 0 < α ≤ 1, and contraction Definition
- Order on the reals Definition
- Rational powers aʳ of a positive base Definition
- √· on [0,∞) is uniformly continuous and exactly 1/2-Hölder, and is not Lipschitz Example
- On [0,1] the function x^β is β-Hölder and is α-Hölder for no rational α > β, so the Hölder classes are strictly nested Example
- The integral test applied to ∑ 1/ι(k+1)ᵖ for rational p>0, cross-checked against the published p-series theorem Example
- FALSE: a^m/n := (a^1/n)ᵐ extends to negative bases False statement
- Every rational has a positive-denominator representative Lemma
- Laws of rational exponents Lemma
- Monotonicity of r ↦ aʳ and of a ↦ aʳ Lemma
- Rational powers do not depend on the representative Lemma
- The integers embed in the rationals Lemma
- The rationals are Archimedean Lemma
- Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent Theorem
- Hölder's inequality for finite sums (rational exponents) Theorem
- If |f(x) - f(y)| ≤ C|x-y|^α on an interval for some rational α > 1 then f is constant Theorem
- Minkowski's inequality for finite sums (rational exponent) Theorem
- The rationals form a totally ordered field Theorem
- Weighted AM-GM inequality with rational weights Theorem
- Young's inequality for products (rational conjugate exponents) Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 19 results over 11 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)
- L. S. Krapp, Constructions of the real numbers: a set theoretical approach (Oxford, 2014) (standard reference, not scraped)