CounterexampleConstruction: 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.

The iterated rational-power law fails without a positive base: $((- 3)^{2})^{1 / 2} = 3 \neq - 3$

Statement refuted

Refuted claim: the identity $(a^{r})^{s} = a^{r s}$ of Laws of rational exponents holds for every real $a$ and all rationals $r, s$ for which both sides are defined.

Witness: $a : = - 3$ , $r : = 2$ , $s : = 1 / 2$ . Here $a^{r}$ is the integer power $(- 3)^{2} = 9$ , so $(a^{r})^{s} = 9^{1 / 2} = 3$ by Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , while $a^{r s} = (- 3)^{1} = - 3$ is again an integer power; the two sides differ. Both displayed expressions are defined by the library's definitions — only the rational-power step, on the positive base $9$ , uses Rational powers $a^{r}$ of a positive base — so the positivity hypothesis $a > 0$ in Laws of rational exponents cannot be dropped. The correct general statement in this case is that $(a^{2})^{1 / 2} = ∣ a ∣$ for every real $a$ .

Facts & Assumptions

Given: The real number $a : = - 3$ , the integer power $r : = 2$ and the rational power $s : = 1 / 2$ , with $r s = 1$ .

[L1]

Rational powers (Rational powers $a^{r}$ of a positive base): for $b > 0$ and $r = m / n$ with $m \in Z$ , $n \geq 1$ , $b^{r} = (b^{1 / n})^{m}$ , and $0^{r} = 0$ for $r > 0$ . This construction assigns no noninteger rational powers to negative bases; their integer powers remain defined by [L3].

[L2]

Rational power laws (Laws of rational exponents): for $a, b > 0$ and rationals $r, s$ , $a^{r} > 0$ , $a^{r + s} = a^{r} a^{s}$ and $(a^{r})^{s} = a^{r s}$ ; the positivity of the base is a hypothesis of that item, not a convenience.

[L3]

Integer powers (Integer powers $a^{m}$ , Laws of integer exponents, Sign rules for products: $(- a) b = - (a b)$ and $(- a) (- b) = a b$ ): $x^{0} = 1$ , $x^{j + 1} = x^{j} x$ , $x^{- j} = (x^{j})^{- 1}$ for $x \neq 0$ , and $(- u) (- v) = u v$ for all reals $u, v$ ; so $(- 3)^{2} = (- 3) (- 3) = 9$ and $(- 3)^{1} = - 3$ .

[L4]

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$ ; in particular $9^{1 / 2} = 3$ because $3 \geq 0$ and $3^{2} = 9$ .

[L5]

Absolute value (Basic properties of the absolute value): $∣ a ∣ \geq 0$ and $∣ a ∣^{2} = a^{2}$ for every real $a$ .

[L6]

Monotonicity and signs of powers (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ): $u \geq 0$ implies $u^{j} \geq 0$ for every natural $j$ ; and $u \mapsto u^{j}$ is strictly increasing on the nonnegatives for $j \geq 1$ , so a nonnegative number with $j$ -th power $c$ is unique.

Counterexample

technique · direct

1.1L3algebra

The two integer-power evaluations at the witness: $(- 3)^{2} = (- 3) (- 3) = 9$ and $(- 3)^{1} = - 3$ by [L3].

1.2L1L4algebra

The rational-power step: $9^{1 / 2} = 3$ by [L4], since $3 \geq 0$ and $3^{2} = 9$ ; the base $9$ is positive, so this is a legitimate application of [L1] at the representative $1 / 2$ .

1.3L4L5L6algebra

The correct general statement: for every real $a$ the value $(a^{2})^{1 / 2}$ exists and equals $∣ a ∣$ , because $∣ a ∣ \geq 0$ with $∣ a ∣^{2} = a^{2}$ by [L5], so $a^{2} = ∣ a ∣^{2} \geq 0$ by [L6] and $∣ a ∣$ is a nonnegative square root of $a^{2}$ , which is unique by [L4]; for $a < 0$ this left-hand value is the positive number $∣ a ∣$ and not $a$ , which is the precise sense in which the identity fails without positivity of the base.

2.1step 1.1step 1.2L1L3algebra

The comparison and the failure: $3 \neq - 3$ , since $3 > 0 > - 3$ ; hence at $a = - 3$ , $r = 2$ , $s = 1 / 2$ one has $(a^{r})^{s} = ((- 3)^{2})^{1 / 2} = 9^{1 / 2} = 3$ while $a^{r s} = (- 3)^{2 \cdot (1 / 2)} = (- 3)^{1} = - 3$ , so the identity $(a^{r})^{s} = a^{r s}$ fails; both sides are defined, the right side as an integer power and the left side because its inner value $9$ is positive, so this is a failure of the identity and not of definedness.

3.1step 2.1step 1.3L1L2L3∎

Conclusion: the witness refutes the unrestricted identity (step 2.1), the general computation identifies what survives in its place, namely $(a^{2})^{1 / 2} = ∣ a ∣$ (step 1.3), and the closing correct statement is exactly why [L2] requires $a > 0$ ; no integer-power law is denied, since [L3] governs the evaluations used and imposes only $x \neq 0$ where inverses are taken, which holds at $x = - 3$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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

The iterated rational-power law fails without a positive base: ((−3)2)1/2=3≠−3((−3)2)1/2=3=−3