Point-free Construction of Real Exponentiation

We proceed in stages.

< - paragraph-2 paragraph4-2

Step 0: Set-up. We define \phi\colon Y\rightarrow \mathsf{RIdl}(Y,<) as sending q\mapsto I_q:=\{q'\in Y|q'<q\}. Since (Y,<) is an R-structure, I_q is an ideal by definition, and so \phi is well-defined. In particular, observe that I_q=\!\operatorname*{\,\ThisStyle{\ensurestackMath{ \bigsqcup\stackengine{-0pt}{\!}{\SavedStyle\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\,}_{q'<q}I_{q'}. Further, using the explicit description of the opens in [Vi8], one easily verifies that \phi is indeed an epimorphism.

< - paragraph-2 paragraph4-2

Step 1: Transforming a given map Suppose we have a map f\colon Y\rightarrow X satisfying the monotonicity and continuity conditions. Since I\subseteq Y for any I\in\mathsf{RIdl}(Y,<), we thus define a map \overline{f}\colon \mathsf{RIdl}(Y,<)\rightarrow X as sending I\mapsto\!\operatorname*{\,\ThisStyle{\ensurestackMath{ \bigsqcup\stackengine{-0pt}{\!}{\SavedStyle\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\,}_{q\in I}f(q).

Conversely, suppose we have a map \overline{f}\colon \mathsf{RIdl}(Y,<)\rightarrow X. We then define f\colon Y\rightarrow X as sending q\mapsto \overline{f}(I_q) That this definition of f also satisfies the required properties is a consequence of the fact that I_q=\!\operatorname*{\,\ThisStyle{\ensurestackMath{ \bigsqcup\stackengine{-0pt}{\!}{\SavedStyle\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\,}_{q'<q}I_{q'}. For monotonicity, observe that I_q=\!\operatorname*{\,\ThisStyle{\ensurestackMath{ \bigsqcup\stackengine{-0pt}{\!}{\SavedStyle\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\,}_{q'<q}I_{q'} means that q'<q\implies I_{q'}\sqsubseteq I_{q}. Hence, since \overline{f}(I_{q'}\sqsubseteq I_{q}) induces \overline{f}(I_{q'})\sqsubseteq \overline{f}(I_{q}) by functoriality, this gives q'<q\implies f(q')\sqsubseteq f(q), as desired. Continuity follows immediately from the fact that maps preserve directed joins, and so I_q=\!\operatorname*{\,\ThisStyle{\ensurestackMath{ \bigsqcup\stackengine{-0pt}{\!}{\SavedStyle\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\,}_{q'<q}I_{q'} yields the identity \overline{f}(I_{q})=\!\operatorname*{\,\ThisStyle{\ensurestackMath{ \bigsqcup\stackengine{-0pt}{\!}{\SavedStyle\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\,}_{q'<q}\,\overline{f}(I_{q'}).

< - paragraph-2 paragraph4-2

Step 2: Proving equivalence We need to show that the transformation of maps in Step 1 are inverses. In one direction, suppose we have f\colon Y\rightarrow X satisfying the monotonicity and continuity conditions, and define g(q):=\overline{f}(I_q). Recalling that maps preserve directed joins, since \overline{f}(I_q)=\!\operatorname*{\,\ThisStyle{\ensurestackMath{ \bigsqcup\stackengine{-0pt}{\!}{\SavedStyle\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\,}_{q'<q}f(q')=f(q), it follows that f=g. In the other direction, given a map \overline{f}\colon Z\rightarrow X, define \overline{g}(I):=\!\operatorname*{\,\ThisStyle{\ensurestackMath{ \bigsqcup\stackengine{-0pt}{\!}{\SavedStyle\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\,}_{q\in I}\,\overline{f}(I_q) as well as f(q):=\overline{f}(I_q). By construction, it is clear \overline{f}\circ \phi=f=\overline{g}\circ \phi. Since \phi is epi, this yields \overline{f}\circ\phi=\overline{g}\circ\phi\!\implies\! \overline{f}=\overline{g}, and we are done.

Our main step is to show that P is a proper surjection, and hence the stable coequaliser of its kernel pair. After that it remains to show that it is the stable coequaliser of the pair in the statement.

In fact we prove a stronger property of P, that it is an entire surjection. “Entire” means fibrewise Stone: in other words, each fibre P^{-1}(x) is the spectrum (i.e. the space of prime filters) of a Boolean algebra B_x (of clopens). We define B_x to be the Boolean algebra presented by one generator \alpha subject to the following relations:

We show that the fibre of P over each x is isomorphic to \mathsf{Spec}B_x.

For a geometric description of points of the coproduct, we write them as (p?\,y\mathord{:}\,z), an abbreviation of the notation \text{\textbf{if }}p\text{\textbf{ then }}y\text{\textbf{ else }}z used in [Vi9, 2.2.6]. Here, p is a decidable proposition, y is a point of (0,1] defined if p holds, and z a point of [1,\infty) defined if \neg p. Then, as described in [Vi9], a copairing map [f,g] maps (p?\,y\mathord{:}\,z) to the directed join \!\operatorname*{\,\ThisStyle{\ensurestackMath{ \bigsqcup\stackengine{-0pt}{\!}{\SavedStyle\!^{\mathord{\uparrow}}}{O}{l}{F}{T}{S}}}\,}\left(\{f(y)\mid p\}\cup\{g(z)\mid\neg p\}\right).

For P, it follows that a point of the fibre P^{-1}(x) must be of the form (p?\,x\mathord{:}\,x). Thus if x<1 then p must be true, since x is not defined as point of [1,\infty); and, similarly, if 1<x then p must be false:

To map P^{-1}(x) to \mathsf{Spec}B_x, we map (p?\,x\mathord{:}\,x)\mapsto \{1\}\cup\{\alpha\mid p\}\cup\{\neg\alpha\mid\neg p\}. To show that this subset F of B_x is a prime filter, the main issue is that it does not contain 0. To see this, consider if \alpha=0. Then x>1, hence \neg p, and \alpha\neq F. The case \neg\alpha=0 is similar.

For the reverse direction we map F\mapsto (\alpha\in F?\,x\mathord{:}\,x). Note that \alpha\in F is decidable; its complement is \neg\alpha\in F. If \alpha\in F then \alpha\neq 0, so x\leq 1 and x is defined as point of (0,1]. Similarly, if \neg\alpha\in F then x is defined as point of [1,\infty). It follows that (\alpha\in F?\,x\mathord{:}\,x) is a point of P^{-1}(x).

The two maps are mutually inverse, which proves our claim that P is entire. It is surjective because every B_x is non-degenerate (i.e. it has 1\neq 0), essentially because we cannot have both x < 1 and x>1.

Now we know that P is the coequaliser of its kernel pair, it remains to show that the kernel pair and the pair (1_R,1_L) have the same coequalisers. The kernel pair, the pullback of P against itself, can be calculated as the coproduct of four pairwise pullbacks of the components of (0,1]\amalg[1,\infty). Since both (0,1] and [1,\infty) are embedded in (0,\infty), their kernel pairs are just the reflexive parts and are irrelevant to the coequaliser. The pullback (0,1] \times_{(0,\infty)}[1,\infty), the space of pairs (x,x) such that 1\geq x \geq 1, is just \{1\}, and the remaining component is just the reverse of that, and implied by symmetry. Hence the kernel pair has the same coequaliser as the pair (1_L,1_R).

Let x\in M, and a,a'\in\mathbb{N}. Equation (?), and the second part of Equation (?), come straight from the definition. The others are by induction on a or a'.

Let us fix some a\in\mathbb{N}. Then, consider the diagram:

where f_a\colon Q\rightarrow Q is the map that sends x\mapsto x^a. We now check that \phi\circ f_a satisfies the two lifting conditions of the Lifting Lemma based on \overrightarrow{[0,\infty]}\cong\mathsf{RIdl}(Q,<), where < is the usual strict order on Q but modified to allow 0<0 (cf. Remark 1.30).

For monotonicity, suppose q<q' for q,q'\in Q. By Lemma 2.2, this yields the inequality q^a\leq (q')^a, which is preserved by \phi, and so q<q'\!\implies\! \phi\circ f_a(q)\sqsubseteq \phi\circ f_a(q'). To verify continuity, this amounts to showing that if r<(q')^a, then \exists q<q' such that r<q^a (where r,q,q'\in Q). For a=0, r<(q')^{0}=1, then we can let q=\frac{q'}{2} since r<1=q^{0}. For a\geq 1, we know by Lemma 2.3 that there exists some t\in Q such that r<t^a<(q')^a. Since \text{(---)}^a still reflects the (modified) order < on Q, we have that t<q' and r<t^a, as desired. With the appropriate hypotheses verified, we apply the Lifting Lemma to obtain the (unique) map \overline{f}\colon \overrightarrow{[0,\infty]}\rightarrow \overrightarrow{[0,\infty]}. Viewing this map externally (cf. Convention 1.9), we get an exponentiation map \overrightarrow{[0,\infty]}\times\mathbb{N}\rightarrow \overrightarrow{[0,\infty]} sending (x,a)\mapsto x^a. The Basic Equations, and also the uniqueness, follow from surjectivity of \phi, since we already know that they hold for rational x and y.

A similar argument (using Q_{+}\cup\{\infty\}) works for the upper reals, thus defining x^a for some upper real x\in \overleftarrow{[0,\infty]}.

It remains to verify the inhabitedness, separatedness and locatedness axioms. Right inhabitedness essentially follows from the unboundedness of \text{(---)}^a on \mathbb{Q} (Lemma 2.2) whereas we get left inhabitedness (and non-negativity) for free since for any negative rational q<0, we get q<x^{a} by construction.

For separatedness, suppose q < x^a < r. Notice that r\in Q_+ by construction, hence if q\leq 0, then q<r automatically. Suppose instead that q>0 and there exist non-negative rationals s,t such that s<x<t, whereby q< s^a and t^a<r. Since x is a separated Dedekind, s<x<t\implies s<t. Hence, since s^a=1=t^a if a=0, and s^a<t^a if a>0 by Lemma 2.2, this combines to yield the inequality q<s^a\leq t^a<r, proving separatedness.

For locatedness, suppose we have q,r\in\mathbb{Q} such that q<r. If q<0, then q<x^{a} automatically, so assume q\geq 0 for the remainder of this proof.

In the case where a>0, by Lemma 2.3 we can find q',r'\in Q_+ such that q<(q')^a<(r')^a<r. Since \text{(---)}^a reflects strict order (Lemma 2.2), we get (q')^a<(r')^a\implies q'<r'. Further, since x is a located Dedekind real, this implies that either q'<x (and thus q<x^a) or that r'>x (and thus r>x^a). Alternatively, suppose that a=0. Then locatedness is obvious, since x^0=1 is located. Hence, in either case (a=0 or a>0), locatedness holds.

The Basic Equations follow immediately, because we know they hold for the lower and upper parts.

Consider \text{(---)}^a on the lower reals \overrightarrow{[0,\infty]}. Preservation of non-strict order follows immediately from the fact that any continuous map preserves specialisation order. To show that \text{(---)}^a reflects non-strict order, suppose that x^a\sqsubseteq y^a. This yields the computation:

Next, to show that \text{(---)}^a also preserves strict order on the non-negative Dedekinds, suppose x<y, and so there exists rationals q,q' such that x<q<q'<y. Then since \text{(---)}^a preserves non-strict order, and using Lemma 2.2, we get x^a\leq q^a< (q')^{a} \leq y^a and hence x^a<y^a.

On the other hand, suppose x^a<y^a. Since 0\leq x^a, we may apply Lemma 2.3, to obtain positive rationals s,s'\in Q_+ such that x^a<s^a<(s')^a<y^a. Since s<s' iff s^a<(s')^a, and since \text{(---)}^a reflects non-strict order, we get x\leq s < s' \leq y, which shows that \text{(---)}^a also reflects strict order on the non-negative Dedekinds.

Unboundedness follows directly from the rational case, Lemma 2.2.

Let x be a non-negative lower real. Non-negativity of x^{\frac{1}{b}} is immediate from definition. When q<0, downward closure and roundedness are obvious, so we shall assume that q^b<x\land q\in Q. In which case, downward closure says that if q'<q for q'\in \mathbb{Q}, then q<x^\frac{1}{b}\implies q'<x^{\frac{1}{b}}. If q'<0, this is obvious. If q'\geq 0, this follows immediately from the monotonicity of exponentiation by b\in\mathbb{N}_+ (Lemma 2.2). As for roundedness, we must show if q^b<x then there exists rational q'>q such that q^b<(q')^b<x. We know there exists r\in Q_+ such that q^b<r<x. By Lemma 2.3, there exists q'\in Q_+ such that q^b<(q')^b<r<x, and we are done.

The case for non-negative upper reals is analogous.

As before, to define \text{(---)}^{\frac{1}{b}} on non-negative Dedekinds, we shall need to verify the rest of the axioms from Definition 1.14. Left inhabitedness comes for free since q<x^{\frac{1}{b}} for all negative rationals q. Right inhabitedness follows from the unboundedness of \text{(---)}^b on the rationals (Lemma 2.2).

For separatedness, suppose q<x^{\frac{1}{b}}<r. Since x is non-negative, and since \text{(---)}^b reflects strict order, this immediately implies that r>0. As such, if q<0, then q<r automatically. Hence, suppose instead that q\geq 0, and that q^b<x<r^b. Since x is a separated Dedekind, this implies that q^b<r^b, and so we get q<r (again by Lemma 2.2).

Finally, we check locatedness. Suppose q<r. Again, if q<0, then we get that q<x^{\frac{1}{b}} for free, so suppose q\geq 0. By Lemma 2.2, we know that 0\leq q^b < r^b. Since x is a located Dedekind, this implies that either q^b<x\vee x<r^b, which in turn implies (by construction) that q<x^{\frac{1}{b}}\vee x^{\frac{1}{b}}<r, proving the axiom.

The proof of these identities for the one-sided reals is analogous, so we shall only prove it for the upper reals, which will also automatically extend the result to the Dedekind reals (cf. Corollary 1.27).

To prove x=(x^{\frac{1}{b}})^b for the upper reals, suppose q>(x^\frac{1}{b})^b. This means that \exists q'\in Q_+ such that (q')^b>x and q>(q')^b, which implies that q>x. Conversely, suppose q>x. By roundedness, we know that there exists some q''\in Q_+ such that q>q''>x\geq 0. By Lemma 2.3, we know that there exists some q'\in Q_+ such that q>(q')^b>q''>x, proving that q>(x^{\frac{1}{b}})^b.

To prove x=(x^b)^{\frac{1}{b}}, note that x=(x^\frac{1}{b})^{b} implies that \big((x^b)^{\frac{1}{b}}\big)^b=x^b. The result then follows since \text{(---)}^b reflects the (non-strict) order on the upper reals by Lemma 2.7.

In each case, the proof is to raise both sides to an appropriate power, use equations already known for integer powers, and then take the root. For example, the first one follows from

To show that x^q is well-defined (with respect to the equivalence of rationals), we need to show that given any \frac{a}{b}=\frac{c}{d}, where a,c\in\mathbb{N} and b,d\in\mathbb{N}_+, we have that (x^{a})^{\frac{1}{b}}=(x^{c})^{\frac{1}{d}}. Why is this? First, note that x^{\frac{a}{b}}=x^{\frac{ak}{bk}}, for \frac{a}{b}\in Q and k\in\mathbb{N}_+. Indeed, by Proposition 2.9 and Corollary 2.10, we have:

More generally, suppose we have that \frac{a}{b},\frac{c}{d}\in Q such that \frac{a}{b}=\frac{c}{d}. This obviously implies that ad=bc, and thus our previous computation yields the identity: x^{\frac{a}{b}}=x^{\frac{ad}{bd}}=x^{\frac{bc}{bd}}=x^{\frac{c}{d}}, as desired.

To see why the Basic Equations hold for non-negative rational exponents, this follows follows algebraically from the Basic Equations already established and Corollary 2.10. For example for the law of adding exponents, if r=\frac{a}{b} and s=\frac{c}{d}, then

Preservation and reflection of strict (resp. non-strict) order on the positive Dedekind (resp. one-sided) reals is immediate from Lemma 2.7. Further, express q as \frac{a}{b} for a,b\in\mathbb{N}_+. We know for any positive Dedekind x\in(0,\infty) that there exists s\in\mathbb{Q} whereby 1<s and x<s\leq s^a. Since s^a=(s^b)^\frac{a}{b}=(s^b)^q, this proves that \text{(---)}^q is unbounded.

For the first identity, if q\geq 0 then x^{-q}=\left(x^{q}\right)^{-1} by definition; while if q \leq 0 then \left(x^{q}\right)^{-1} =\left(\left(x^{-q}\right)^{-1}\right)^{-1}=x^{-q}.

As for the identity (x^{q})^{-1}=(x^{-1})^{q}, if q\geq 0 then it follows from the Basic Equations because

Then for q\leq 0 we have

Strict order is decidable on \mathbb{Q}, and so given any q\in\mathbb{Q}, we can split our proof into the cases when q,q' have the same signs or opposite signs.

Case 1: q,q'\geq 0. By Proposition 2.11.

Case 2: q,q'\leq 0. This follows from Case 1 and Lemma 2.14, which yields:

Case 3: q\leq 0\leq q'. This also follows from Case 1 and Lemma 2.14, since:

Case 4: q'\leq 0\leq q. By symmetry with Case 3.

Similar to Proposition 2.16, we split our proof into various cases, based on the sign of the rational exponents of the identity. By previous work, we have already shown the following case:

Basic Case: q,q'\geq 0 (and thus q+q'\geq 0): Immediate from Proposition 2.11.

We claim that all the possible (signed) combinations of q,q' and q+q' ultimately reduce to this basic case after some elementary algebraic manipulations. If at least one of them, say q, is negative, then the equation to prove is equivalent to

once we multiply both sides by x^{-q}=(x^{q})^{-1}. This is another instance of the identity in the statement, but with (q,q') replaced by (-q,q+q'), with strictly fewer of the three exponents negative. If in addition q+q' and/or q' are also negative, then we iterate the process so that we eventually hit the Basic Case.

Immediate from Proposition 2.11 and definitions.

Fix Dedekind x such that x>1. Suppose we are given some r,s\in\mathbb{Q} such that r<s. By the exponent laws for rational exponents, this implies that x^{s}=x^{r+s-r}=x^{r}\cdot x^{s-r}. By Lemma 2.12, we have that 1<x^q for any positive rational q>0. Since 0<s-r\implies 1<x^{s-r}, this in turn implies that x^s=x^{r}\cdot x^{s-r}>x^{r}, proving that x^{\text{(---)}} is indeed strictly increasing on \mathbb{Q}. The case for x^{\text{(---)}} when we have Dedekind 0<x<1 is analogous.

The same proof works for the one-sided case modulo the following adjustments: one, x^{\text{(---)}} is not defined for negative rational exponents, so we restrict the map to just the non-negative rationals Q; and two, Lemma 2.12 now holds that \text{(---)}^q only preserves non-strict order, so we only get weakly monotonic/antitonic results for x^{\text{(---)}} when x is one-sided.

Fix Dedekind x\in[1,\infty) We prove the result for the lower case of \zeta. The upper case is analogous.

Following Remark 1.30, we check the two lifting conditions of the Lifting Lemma based on \overrightarrow{[-\infty, \infty]}\cong\mathsf{RIdl}(\mathbb{Q}\cup\{-\infty\},<) (the involvement of -\infty is largely irrelevant, so we shall leave this case to the reader). Monotonicity amounts to holding for any q,r\in\mathbb{Q}, we have that q<r\implies x^q\leq x^r — which is immediate from Proposition 3.1. For continuity: if r<x^q, with r,q\in\mathbb{Q}, we want rational q' < q with r < x^{q'}. This is clear if r\leq 0, hence suppose instead that 0<r. By strict order <, there exists r'\in\mathbb{Q} such that 0<r<r'<x^q. Applying the Continuity Lemma, we find k with rx^{1/k} < r'<x^q. Then r < x^{q-1/k}.

The basic equations follow from the case of rational exponents.

First, we claim the two maps of Proposition 3.4 combine to give an exponentiation map [1,\infty)\times\mathbb{R} \to (0,\infty), by x^\zeta=(x^{L_\zeta}, x^{R_\zeta}). From the definition, we calculate that:

As before, to show this map is well-defined, it remains for us to check inhabitedness, positiveness, separatedness and locatedness. Inhabitedness and positiveness are easy: we know there exist rationals q_0,r_0\in\mathbb{Q} such that q_0<\zeta<r_0 (since \zeta is an inhabited Dedekind) and so there exists q,r\in\mathbb{Q} such that q<x^{q_0} and r>x^{r_0} (since 0<x^{q_0} and x^{r_0} are inhabited as well).

For separatedness, suppose x^{R_\zeta}<q<x^{L_\zeta}. Then we have x^{r_1}<q<x^{r_2} for some rationals r_1,r_2 with R_\zeta<r_1 and r_2<L_\zeta. But \zeta is separated, and so r_2<r_1, which implies x^{r_2}<x^{r_1} by Proposition 3.1, a contradiction.

For locatedness, suppose we have rationals q<r. When q\leq 0, then q<x^{\zeta} since x^{\zeta} is positive, so let’s assume q>0. Leveraging previous results, we then define a series of parameters:

• Denote r':=(q+r)/2.

• By the Continuity Lemma, find k such that r'x^{1/k}<r.

• By Remark 1.16, find a rational s such that s<\zeta<s+1/k.

Since x^s is a (located) Dedekind real, this means that q<x^s or x^s<r'. If q<x^s then q<x^\zeta, while if x^s<r' then x^\zeta<x^{s+1/k}=x^s\cdot x^{1/k}<r'\cdot x^{1/k}<r.

The exponent laws for this map follow from those for the maps in Proposition 3.4.

Having defined x^\zeta for x\in[1,\infty), we can also define an exponentiation (0,1]\times\mathbb{R} \to (0,\infty), by x^\zeta:=(x^{-1})^{-\zeta}. Let us now fix \zeta\in\mathbb{R}. Since the two maps agree on x=1, we can apply the Gluing Principle (Proposition 1.37) to glue them together and obtain the general exponentiation map via the pushout property:

Externalising yields the desired exponentiation map (0,\infty)\times\mathbb{R}\rightarrow (0,\infty) (cf. Convention 1.9). The exponent laws follow immediately.

Let x\in (1,\infty), and \zeta,\zeta'\in\mathbb{R} such that \zeta<\zeta'. By Exponent Law (?) established in Theorem 3.5, we obtain:

We claim x^{\zeta'-\zeta}>1. Why? By strict order < on the reals, pick some r\in Q_+ such that 0<r<\zeta'-\zeta. Unpacking definitions, we know q<x^{r}\implies q<x^{\zeta'-\zeta}. By Proposition 3.1, we get x^r>1, which in turn implies that x^{\zeta'-\zeta}>1. In particular, we get:

The case when x\in (0,1) is entirely analogous.

Similar to Propositions 2.17 and 2.16, we shall need to case split based on which side of 1 the values s,t,s\cdot t lie. If all three are at least 1, then the equation holds from Proposition 3.4. If at least one of them, say s, is less than 1, so s^\zeta=(s^{-1})^{-\zeta}, then the equation is equivalent to (s^{-1})^\zeta\cdot ((s\cdot t)^{-1})^\zeta=t^\zeta, with s^{-1}>1. We may have to apply similar transformations for t and st, but eventually we end up with an equation in which all three values are at least 1.

We prove the lower case. Following Remark 2.15, we know that a map from the rationals can be defined (geometrically) via case-splitting on <. Thus define:

Note that (R_{(s^{-1})^\zeta})^{-1} is indeed a lower real since \text{(---)}^{-1}\colon \overrightarrow{(0,1]}\cong\overleftarrow{[1,\infty)} (cf. Definition 1.34).

We now apply the Lifting Lemma in the case of \overrightarrow{(0,\infty]}\cong \mathsf{RIdl}(Q_+,<). Monotonicity for s<s' essentially follows from Lemma 3.8, which yields:

For continuity, suppose q<s^\zeta. If 1\leq s, then by definition of s^\zeta we have 0<q<s^r for some rational r<\zeta. Let r=\frac{a}{b} for a,b,\in\mathbb{N}_+. Raising to the power of b, we know that q<s^{\frac{a}{b}}\iff q^b < s^a by Lemma 2.12. Applying Lemma 2.3, there exists some positive rational s'\in Q_+ such that q^b<(s')^a<s^a, which (taking bth roots) yields the desired inequality q<(s')^{r}<s^{r}<s^{\zeta}. If instead s<1, then we have s^\zeta=(s^{-1})^{-\zeta}, and so (s^{-1})^\zeta < q^{-1}. By definition of (s^{-1})^\zeta, there exists r\in Q_+ with \zeta<r and (s^{-1})^r<q^{-1}. Applying Lemma 2.12 again, we know there exists some t such that s^{-1}<t<(q^{-1})^{\frac{1}{r}}, and so t^r<q^{-1}. Thus, since s^{-1}<t\iff t^{-1}<s, by Corollary 3.7 we get q<(t^{-1})^r<(t^{-1})^\zeta<s^\zeta.

Finally, checking definitions, it is clear that (L_{x})^{\zeta}=L_{x^{\zeta}}. The proof for upper reals is similar(Note that the definition includes 0^0=\inf_{0<s\in\mathbb{Q}}s^0=1.).

By Theorem 3.5 and Lemma 3.8, the basic laws hold for rational bases, and we can lift those to the one-sided bases.

Fixing \zeta, the base product equation is between two maps from (0,\infty)^2 to (0,\infty). Since (0,\infty) is locally compact, hence exponentiable, this amounts to equality between two maps 1 \to (0,\infty)^{(0,\infty)^2}, and that is a subspace of 1 — internally in \mathcal{S}\mathbb{R}. Hence the \zetas for which that internal subspace is 1 form a subspace of \mathbb{R}. To prove that subspace is the whole of \mathbb{R}, we use the fact that \mathbb{R} is the subspace join of (-\infty, 0) and its closed complement [0, \infty) (see, e.g. [StoneSp], or, for a geometric treatment, [Vi2]). It thus suffices to check the equation in the two cases \zeta<0 and 0\leq\zeta.

If 0\leq \zeta, then the base product law follows from Theorem 3.9. If \zeta<0, then we reduce to the former case by applying the inverse map \text{(---)}^{-1}:

Suppose \zeta\in (0,\infty). Let us first prove (i) when x=1. In which case, pick some q\in\mathbb{Q} such that 0<q<\zeta. By Corollary 3.7, deduce that 1<y implies 1=1^{\zeta}<y^{q}<y^{\zeta}, as desired. In the general case when x<y for x,y\in(0,\infty), observe that x<y\implies 1<y\cdot x^{-1}. Apply Corollary 3.10 to our previous calculation to get 1<(y\cdot x^{-1})^{\zeta}=y^{\zeta}\cdot x^{-\zeta}, which in turn implies that x^{\zeta}<y^{\zeta}, proving (i). The case when \zeta is negative follows from (i) and the fact that inverses reverese orientation.

We prove the lower case. The upper case is very similar.

Fix x\in \overrightarrow{[1,\infty]}, and recall that Q denotes the non-negative rationals. Following Remark 1.30, we apply the Lifting Lemma in the case of \overrightarrow{[0,\infty]}\cong \mathsf{RIdl}(Q,<), with the special understanding that 0<0.

Monotonicity follows from Proposition 3.1. For continuity, suppose r<x^q with 0< q. We want to prove r<x^{q'} for some q' with 0< q'<q. If r<1 then we can just take q'=\frac{q}{2}, so suppose 1\leq r. Since \text{(---)}^q preserves and reflects strict order, we may find some rational s such that 1\leq r^{\frac{1}{q}}<s<x, which in turn implies that r<s^q<x^q. Now using the fact that s, a rational, is Dedekind, we can apply the argument of Proposition 3.4 to find our q'.

The Basic Equations follow from the rational case.

This is a sharper version of the Continuity Lemma 3.3, which only required the Dedekind base to satisfy b\geq 1. In contrast, this lemma requires the Dedekind base b to be strictly greater than 1 (it is clearly false when b=1).

We start by defining a series of parameters:

• By Bernoulli’s Inequality (Lemma 3.2), find a natural number t such that q' < b^t, and a negative integer s such that b^s < q (i.e. q^{-1} < b^{-s}).

• By the Continuity Lemma, find k\in\mathbb{N}_+ such that 1\leq b^{\frac{1}{k}}<1+\frac{q'-q}{b^t}.

Observe that s+\frac{i}{k}\leq t, for all i\in\mathbb{N} such that 0\leq i\leq (t-s)k, with equality exactly when i=(t-s)k. This yields:

By Corollary 3.7, \big\{b^{s+\frac{i}{k}}\big\}_{0\leq i\leq (t-s)k} is a monotonic sequence of located Dedekinds. In particular, this means q<b^{s+\frac{i}{k}}\vee b^{s+\frac{i}{k}}<q' for all relevant i. Thus, by a reasoning similar to the proof of Lemma 2.3, one shows there indeed exists an i\in\mathbb{N}_+ so that q< b^{s+\frac{i}{k}}<q'.

The proof proceeds in stages. < - paragraph-2 paragraph4-2

Step 0: Set-up Fix b\in (1,\infty). In the case where y is a one-sided real, we define the \log_b maps as:

with the understanding that when y is a lower real, we define b^q<y to mean b^q<r<y for some rational r (and similarly when y is upper). Note that this definition makes sense since b^q is Dedekind. Finally, we remark that we shall freely make use of Corollary 3.7 without explicit mention, in particular the fact that q<r \implies b^{q}<b^r for any rationals q and r. < - paragraph-2 paragraph4-2

Step 1: \log_b(y) as a one-sided To verify downward closure and upper-roundedness for the lower reals, observe that this coincides with verifying the monotonicity and continuity conditions for the Lifting Lemma in our proof of Proposition 3.4. We remark that when y=0, then \log_b0 is the empty lower real, i.e. -\infty. The case for upper reals is similar.

< - paragraph-2 paragraph4-2

Step 2: \log_b(y) as a Dedekind After Step 1, it remains to check inhabitedness, separatedness and locatedness. Inhabitedness can be derived from Lemma 4.1.

To show separatedness, suppose q<\log_b(y)<r. By definition, this means b^q<y<b^r. By decidability of < on \mathbb{Q}, we know that r\leq q or q<r. If r\leq q, then this yields b^r\leq b^{q}<b^{r}, a contradiction. Hence, this forces the inequality q<r.

For locatedness, suppose we have q,r\in\mathbb{Q} such that q<r. As before, we know that q<r yields the inequality b^{q}<b^{r}. Pick u_1,u_2\in\mathbb{Q} such that b^{q}<u_1<u_2<b^{r}. Since y is located, either u_1<y or y<u_2. Since u_1<y\implies b^{q}<y and y<u_2\implies y<b^{r}, this implies q<\log_b(y)\vee r>\log_b(y), i.e. \log_b(y) is located.

< - paragraph-2 paragraph4-2

Step 3: \log_b and b^{\text{(---)}} are inverses We prove \log_b and b^{\text{(---)}} are inverses on the one-sideds, where

The case for the Dedekinds follows immediately by Corollary 1.27.

< - paragraph-2 paragraph4-2

Step 3a: Show that b^{\log_{b}(y)}=y. Now suppose q<b^{\log_b(y)}. Then by definition (cf. Theorem 3.5), \exists q'\in\mathbb{Q} such that q'<\log_b(y) and q<b^{q'}. Since q'<\log_b(y)\implies b^{q'}<y, this assembles to yield the inequality q<b^{q'}<y, proving that b^{\log_b(y)} \leq y. Conversely, suppose q<y. If q<0, then q<b^{\log_b(y)} automatically. If q\geq 0, then pick q',q''\in Q_+ such that q<q'<q''<y. By Lemma 4.1, there exists r\in\mathbb{Q} such that q<q'<b^r<q''<y, hence r<\log_b(y) and q<b^{\log_b (y)}, i.e. y\leq b^{\log_b(y)}. Since y\leq b^{\log_b(y)} and b^{\log_b(y)}\leq y, this shows that b^{\log_b(y)}=y for lower reals. The case for the upper reals is entirely analogous. < - paragraph-2 paragraph4-2

Step 3b: Show that \log_{b}(b^\zeta)=\zeta Suppose q<\log_b(b^\zeta). Then, unwinding definitions, there exists rationals q',q''\in\mathbb{Q} such that b^q<q'<b^{\zeta} and q''<\zeta\land q'<b^{q''}. In particular, this yields the inequality b^{q}<b^{q''}, which in turn implies q<q''<\zeta, proving that \log_b(b^{\zeta})\leq \zeta. Conversely, suppose that q<\zeta. A routine calculation shows that b^{q}<b^{\zeta}, which by definition yields q<\log_b(b^{\zeta}), proving that \zeta\leq \log_b(b^\zeta). Putting everything together yields \log_{b}(b^\zeta)=\zeta. As before, the case for upper reals is entirely analogous.