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.

Odd powers are bijections of $R$ : $x^{3} = - 8$ has the unique solution $x = - 2$

Example

Call a natural number $n$ odd when $n = 2 k + 1$ for some natural $k$ ; every odd $n$ satisfies $n \geq 1$ . Let $n$ be odd. Then $x \mapsto x^{n}$ is a bijection of $R$ onto $R$ : every real number has exactly one real $n$ -th root. Explicitly, $x^{3} = - 8$ has the unique solution $x = - 2$ , and $x^{5} = - 32$ has the unique solution $x = - 2$ .

For a negative right-hand side this is a statement about the solution of $x^{n} = a$ , with $n$ an odd exponent; for $n > 1$ it does not extend the symbol $a^{1 / n}$ , since Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ produces that symbol only for $a \geq 0$ and Rational powers $a^{r}$ of a positive base does not define rational powers of negative bases (its separate zero-base clause concerns nonnegative bases only). This is the claim the A-page prose records when it says that odd roots of negatives do exist, while FALSE: every real number has a real square root shows that even ones do not.

Facts & Assumptions

Given: A natural number $n = 2 k + 1$ with $k \in N$ , so that $n \geq 1$ ; all powers are as in Integer powers $a^{m}$ .

[L1]

Roots of nonnegatives (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ): for every $c \geq 0$ and every $n \geq 1$ there is a unique $c^{1 / n} \geq 0$ with $(c^{1 / n})^{n} = c$ , and $c^{1 / n} > 0$ when $c > 0$ .

[L2]

Laws of natural exponents (Laws of integer exponents, claim 1): $a^{m + n} = a^{m} a^{n}$ , $(a^{m})^{n} = a^{m n}$ and $(a b)^{n} = a^{n} b^{n}$ for all reals $a, b$ and all naturals $m, n$ ; the recursion clauses of Integer powers $a^{m}$ give $a^{0} = 1$ and $a^{j + 1} = a^{j} a$ .

[L3]

Monotonicity of powers (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ): $a \geq 0$ implies $a^{j} \geq 0$ and $a > 0$ implies $a^{j} > 0$ for every natural $j$ ; and $0 \leq a < b$ with $j \geq 1$ implies $a^{j} < b^{j}$ . Also $1^{j} = 1$ for every natural $j$ .

[L4]

Sign rules (Sign rules for products and monotonicity of multiplication): a product of two positive reals is positive; and for $c < 0$ , $a < b$ holds exactly when $b c < a c$ . With $c = - 1$ this turns $x < y$ into $- y < - x$ and back. The identity $(- 1) (- 1) = 1$ follows from $(- u) (- v) = u v$ at $u = v = 1$ (Sign rules for products: $(- a) b = - (a b)$ and $(- a) (- b) = a b$ ), followed by $1 \cdot 1 = 1$ .

[L5]

No negative square root (FALSE: every real number has a real square root): there is no real $y$ with $y^{2} = - 1$ , so the hypothesis that $n$ be odd cannot be dropped; even exponents land in the nonnegatives.

[L6]

The rational-power construction (Rational powers $a^{r}$ of a positive base) applies to $a > 0$ and every rational $r$ , and additionally sets $0^{r} = 0$ for rational $r > 0$ . It assigns no noninteger rational powers to negative bases. Integer powers remain defined by Integer powers $a^{m}$ ; in particular the case $n = 1$ gives $a^{1} = a$ .

Verification

technique · cases

1.1L2L3L4algebra

The odd power of a negative is negative: since $n = 2 k + 1$ and $(- 1)^{2} = (- 1) (- 1) = 1$ by [L4], the laws of [L2] give $(- 1)^{n} = ((- 1)^{2})^{k} \cdot (- 1) = 1^{k} \cdot (- 1) = - 1$ by [L3]; hence for every real $u$ , $(- u)^{n} = ((- 1) u)^{n} = (- 1)^{n} u^{n} = - u^{n}$ by the product law of [L2], so a negative input gives a negative output and $(- u)^{n} > 0$ whenever $u < 0$ .

2.1step 1.1L1algebra

Existence, in the two sign cases: if $a \geq 0$ , put $x : = a^{1 / n}$ , so that $x^{n} = a$ by [L1]; if $a < 0$ , put $b : = - a > 0$ , $y : = b^{1 / n} \geq 0$ by [L1], and $x : = - y$ , so that $x^{n} = (- y)^{n} = - y^{n} = - b = a$ by step 1.1 and $y^{n} = b$ ; in both cases $x$ is a real $n$ -th root of $a$ , so every real number is an $n$ -th power.

2.2step 1.1L3L4cases

Injectivity, in the three order cases: let $x < y$ be reals. If $0 \leq x < y$ then $x^{n} < y^{n}$ by [L3]. If $x < y \leq 0$ then $0 \leq - y < - x$ by [L4], so $(- y)^{n} < (- x)^{n}$ by [L3], that is $- y^{n} < - x^{n}$ by step 1.1, and multiplying by $- 1$ through [L4] gives $x^{n} < y^{n}$ . If $x < 0 \leq y$ then $x^{n} = - (- x)^{n} < 0$ by step 1.1 and [L3] applied to the positive $- x$ , while $y^{n} \geq 0$ by [L3], so again $x^{n} < y^{n}$ . Hence $x < y$ always implies $x^{n} < y^{n}$ , and $x \mapsto x^{n}$ is injective.

3.1step 2.1step 2.2step 1.1L2L5L6cases-exhaustive∎

Combining steps 2.1 and 2.2, $x \mapsto x^{n}$ is injective and surjective, hence a bijection of $R$ onto $R$ , and every real number has exactly one real $n$ -th root; in particular $(- 2)^{3} = - 2^{3} = - 8$ and $(- 2)^{5} = - 2^{5} = - 32$ by step 1.1 and the evaluations of [L2], so $x = - 2$ solves $x^{3} = - 8$ and $x^{5} = - 32$ , and injectivity makes those solutions unique; the hypothesis that $n$ is odd is indispensable, since for $n = 2$ the value $- 1$ has no real square root by [L5], and [L6] records why none of this assigns a value to $(- 8)^{1 / 3}$ as a rational power.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

Odd powers are bijections of RR: x3=−8x3=−8 has the unique solution x=−2x=−2