Rational powers $a^r$ of a positive base

Let $a \in \mathbb{R}$ with $a > 0$ and let $r \in \mathbb{Q}$ (The rationals as equivalence classes of pairs of integers).

Every rational has a representative with positive denominator (Every rational has a positive-denominator representative), so write $r = m/n$ with $m \in \mathbb{Z}$ and $n$ a positive integer; a positive integer is the image of a unique natural $\ge 1$ (The naturals embed in the integers), and we write $n$ for that natural too. Define

$a^{r} := \big(a^{1/n}\big)^{m},$

where $a^{1/n}$ is the unique nonnegative $n$-th root of $a$ (Existence and uniqueness of $n$-th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$) and the outer exponent is an integer power (Integer powers $a^m$). The outer power is legitimate because $a^{1/n} > 0$ when $a > 0$, so it has an inverse and negative integer exponents are allowed.

Well-definedness. The right-hand side must not depend on which representative $m/n$ of $r$ was chosen. It does not: that is Rational powers do not depend on the representative ↗, which is recorded in this item's justified_by rather than in its deps, since it is a statement about the operation defined here and therefore depends on this definition.

The base must be positive. For $a < 0$ the same formula is not a definition at all, because different representatives of the same rational give different answers, or no answer: see FALSE: $a^{m/n} := (a^{1/n})^{m}$ extends to negative bases, which is exactly the item that justifies the restriction.

Supplementary clause for the base $0$. For $a = 0$ and rational $r > 0$ (Order on the rationals) the displayed formula still makes sense and still does not depend on the representative: $r > 0$ forces $m \ge 1$, and $\big(0^{1/n}\big)^{m} = 0^{m} = 0$ (Existence and uniqueness of $n$-th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$ applies to every $a \ge 0$). So we set $0^{r} = 0$ for rational $r > 0$. For $r < 0$ the expression $0^{r}$ is left undefined, since $0$ has no inverse. This clause is what lets the inequalities later on this page be stated for nonnegative entries rather than for positive ones only.

• Consistency with integer powers. If $r \in \mathbb{Z}$ then $r = r/1$, $a^{1/1} = a$ (Existence and uniqueness of $n$-th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$), and the definition returns $(a^{1})^{r} = a^{r}$ as given by Integer powers $a^m$. So the notation $a^{r}$ is unambiguous, and rational powers extend integer powers on positive bases. At $r = 1/n$ it returns $\big(a^{1/n}\big)^{1} = a^{1/n}$, so the root notation of Existence and uniqueness of $n$-th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$ is the special case $r = 1/n$, as intended.
• $a^{r} > 0$ for every $a > 0$ and every $r \in \mathbb{Q}$, the exponent $0$ included. Writing $r = m/n$ with $n \ge 1$: the root $a^{1/n}$ is positive (Existence and uniqueness of $n$-th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$); for $m \ge 0$ the value $\big(a^{1/n}\big)^{m}$ is a natural power of a positive element, hence positive, which is claim 1 of Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$ and covers $m = 0$ as well, since $a^{0} = 1 > 0$; and for $m < 0$ the value is $\big(a^{1/n}\big)^{m} = \Big(\big(a^{1/n}\big)^{-m}\Big)^{-1}$ (Laws of integer exponents, claim 2), the inverse of a positive element, hence positive (Inverses of positives are positive, and reciprocation reverses order). Note that Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$ is stated for natural exponents only, so it does not by itself settle the negative case; that is what the inverse step is for. The exponent laws are Laws of rational exponents and the order behaviour is Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$.
• The exponent is a rational, never a real. Nothing on this page is a limit, a series or a continuous function, and $a^{r}$ is computed in finitely many field operations once the root is available. What would be needed to go further, why it is deferred here, and where the library later defines $a^{x}$ for real $x$ are recorded in Why real exponents are deferred on the rational-powers page.
• The convention $0^0 = 1$ of Integer powers $a^m$ is untouched: $r = 0$ is not covered by the supplementary clause, which asks for $r > 0$. So $0^0 = 1$ while $0^{r} = 0$ for every rational $r > 0$. There is no inconsistency, only the familiar fact that the two-variable function $(a, r) \mapsto a^{r}$ has no continuous extension to $(0,0)$, a statement this library cannot even make yet.