ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Comparing rational powers: $2^{1 / 3} < 2^{1 / 2} < 3^{1 / 3}$

Example

(i) $2^{1 / 2} > 2^{1 / 3}$ ; (ii) $3^{1 / 2} > 2^{1 / 2}$ ; (iii) $2^{1 / 2} < 3^{1 / 3}$ ; hence

$2^{1 / 3} < 2^{1 / 2} < 3^{1 / 3} .$

All bases are positive and all exponents rational, so Rational powers $a^{r}$ of a positive base applies. Clauses (i) and (ii) are instances of the two monotonicity statements of Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ , but (iii) is not: it compares bases $2 < 3$ against exponents in the opposite order $1 / 2 > 1 / 3$ , and neither monotonicity clause decides it.

Facts & Assumptions

Given: The positive bases $2$ and $3$ and the rational exponents $1 / 3 < 1 / 2$ in $Q$ .

[L1]

Rational powers (Rational powers $a^{r}$ of a positive base, Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ): for $a > 0$ and rational $r$ the value $a^{r}$ is defined and positive, and $a^{1 / n}$ is the unique nonnegative $n$ -th root of $a$ .

[L2]

Rational power laws (Laws of rational exponents): $(a^{r})^{s} = a^{r s}$ for $a > 0$ and rationals $r, s$ , and $a^{1} = a$ .

[L3]

Monotonicity of rational powers (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ ): for $a > 1$ and rationals $r < s$ one has $a^{r} < a^{s}$ ; and for rational $r > 0$ and $0 < a < b$ one has $a^{r} < b^{r}$ .

[L4]

Monotonicity of integer powers (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ): for $j \geq 1$ , $t \mapsto t^{j}$ is strictly increasing on the nonnegative reals, so $0 \leq u < v$ implies $u^{j} < v^{j}$ .

[L5]

Integer powers (Integer powers $a^{m}$ ): $2^{3} = 2^{2} \cdot 2 = 4 \cdot 2 = 8$ and $3^{2} = 9$ by the recursion clause and field arithmetic.

Verification

technique · direct

1.1L1L3algebra

Clause (i): $2 > 1$ and $1 / 3 < 1 / 2$ in $Q$ , so exponent monotonicity [L3] gives $2^{1 / 3} < 2^{1 / 2}$ .

1.2L1L3algebra

Clause (ii): $1 / 2 > 0$ and $2 < 3$ with both bases positive, so base monotonicity [L3] gives $2^{1 / 2} < 3^{1 / 2}$ .

1.3L1L2L4L5algebra

Clause (iii): raising to the sixth power, $(2^{1 / 2})^{6} = 2^{(1 / 2) \cdot 6} = 2^{3} = 8$ and $(3^{1 / 3})^{6} = 3^{(1 / 3) \cdot 6} = 3^{2} = 9$ by [L2] and [L5], and $8 < 9$ ; since $2^{1 / 2} \geq 0$ and $3^{1 / 3} \geq 0$ by [L1], the strict monotonicity of $t \mapsto t^{6}$ on the nonnegatives [L4] turns $8 < 9$ into $2^{1 / 2} < 3^{1 / 3}$ .

2.1step 1.1step 1.2step 1.3L3∎

Chaining (i) from step 1.1 and (iii) from step 1.3 gives $2^{1 / 3} < 2^{1 / 2} < 3^{1 / 3}$ , and (ii) from step 1.2 records the companion comparison $3^{1 / 2} > 2^{1 / 2}$ ; the three claims together are the displayed order, and only clause (iii) needed the sixth-power device, since no single monotonicity statement compares $2^{1 / 2}$ with $3^{1 / 3}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jiří Lebl, Basic Analysis I: Introduction to Real Analysis, Volume I, version 6.3, 15 May 2026 (author-hosted complete book) (standard reference, not scraped)

Comparing rational powers: 21/3<21/2<31/321/3<21/2<31/3