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.

Rational powers of rational bases computed from the definition

Example

In $R$ , with the rational powers of Rational powers $a^{r}$ of a positive base:

$(4 / 9)^{1 / 2} = 2 / 3, (8 / 27)^{1 / 3} = 2 / 3, (4 / 9)^{3 / 2} = 8 / 27, (27 / 8)^{- 2 / 3} = 4 / 9,$

and $8^{2 / 6} = 8^{1 / 3} = 2$ , one value produced from either representative of the rational $1 / 3 = 2 / 6$ . Every base occurring is a positive rational and every exponent a rational with numerator an integer and denominator a natural $\geq 1$ , so the definition applies in each case; the last display is the instance of Rational powers do not depend on the representative that Rational powers $a^{r}$ of a positive base records in its justified_by. The item also checks the negative-exponent and non-coprime-representative cases, the two places where the definition is most easily misread.

Facts & Assumptions

Given: The rational powers of Rational powers $a^{r}$ of a positive base, used at the displayed rational exponents.

[L1]

Definition (Rational powers $a^{r}$ of a positive base): for $a > 0$ and $r = m / n$ with $m \in Z$ and $n$ a natural $\geq 1$ , $a^{r} = (a^{1 / n})^{m}$ , and $0^{r} = 0$ for rational $r > 0$ .

[L2]

Well-definedness (Rational powers do not depend on the representative): the value $(a^{1 / n})^{m}$ depends only on the rational $m / n$ , not on the representative.

[L3]

Roots (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ): every $c \geq 0$ has a unique $c^{1 / n} \geq 0$ with $(c^{1 / n})^{n} = c$ , and $c^{1 / n} > 0$ for $c > 0$ ; in particular $c^{1 / 1} = c$ .

[L4]

Integer powers and their laws (Integer powers $a^{m}$ , Laws of integer exponents): $x^{0} = 1$ , $x^{j + 1} = x^{j} x$ , $(u v)^{n} = u^{n} v^{n}$ for naturals $n$ , and $x^{- j} = (x^{j})^{- 1}$ for $j \geq 1$ and $x \neq 0$ .

[L5]

Rationals (The rationals as equivalence classes of pairs of integers): a rational is an equivalence class of pairs, and equality $m / n = p / q$ holds exactly when $m q = p n$ in $Z$ ; since $2 \cdot 3 = 1 \cdot 6$ this gives $2 / 6 = 1 / 3$ .

[L6]

Uniqueness of inverses (Identities and inverses in a field are unique): a nonzero element of a field has exactly one multiplicative inverse, so an element whose product with a given one is $1$ is that inverse.

Verification

technique · direct

1.1L1L3algebra

The two-thirds roots: field arithmetic gives $(2 / 3)^{2} = 4 / 9$ and $(2 / 3)^{3} = 8 / 27$ with $2 / 3 \geq 0$ , so the uniqueness in [L3] gives $(4 / 9)^{1 / 2} = 2 / 3$ , read at the representative $1 / 2$ , and $(8 / 27)^{1 / 3} = 2 / 3$ , read at the representative $1 / 3$ .

1.2L2L3L5algebra

The non-coprime representative: $2^{3} = 8$ with $2 \geq 0$ gives $8^{1 / 3} = 2$ by [L3], and $2 / 6 = 1 / 3$ as rationals by [L5] (both are the rational with $2 \cdot 3 = 1 \cdot 6$ ), so well-definedness [L2] gives $8^{2 / 6} = 8^{1 / 3} = 2$ : the same value from either representative of $1 / 3$ .

2.1step 1.1L1L4algebra

The exponent $3 / 2$ : by the definition [L1] at the representative $3 / 2$ and the value of step 1.1, $(4 / 9)^{3 / 2} = ((4 / 9)^{1 / 2})^{3} = (2 / 3)^{3} = 8 / 27$ by [L4] and field arithmetic.

2.2step 1.1L1L3L4L6algebra

The negative exponent $- 2 / 3$ : $(3 / 2)^{3} = 27 / 8$ with $3 / 2 \geq 0$ gives $(27 / 8)^{1 / 3} = 3 / 2$ by the same uniqueness argument as step 1.1, so the definition at the representative $- 2 / 3$ and the negative-exponent clause of [L4] give $(27 / 8)^{- 2 / 3} = ((27 / 8)^{1 / 3})^{- 2} = (3 / 2)^{- 2} = ((3 / 2)^{2})^{- 1} = (9 / 4)^{- 1} = 4 / 9$ , the last equality because $(9 / 4) (4 / 9) = 1$ and inverses are unique by [L6].

3.1step 1.1step 1.2step 2.1step 2.2L1L2∎

All four displays are therefore verified from the definition: the first two by uniqueness of the nonnegative roots (step 1.1), the third by the definition at the representative $3 / 2$ (step 2.1), the fourth by the definition at the negative representative $- 2 / 3$ together with the negative-exponent clause of the integer powers (step 2.2), and the fifth by well-definedness across the two representatives of $1 / 3$ (step 1.2); every base used is positive, so no clause of [L1] is applied outside its hypotheses.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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)