The reciprocal ratio map $a\mapsto a_{\ast }\mathrm{/}a$: strict decrease, inverse, and the exact preimages of points and closed intervals

(Strict decrease.) Let $0<a_1<a_2$. By [L2] claim 2 applied to $a_1<a_2$, $0<a_2^{-1}<a_1^{-1}$; since $a_{\ast }>0$, [L1] claim 4 (multiplying the strict inequality by the positive number $a_{\ast }$) gives $a_{\ast }{a}_2^{-1}<a_{\ast }{a}_1^{-1}$, that is, $F(a_2)<F(a_1)$ by the definition of $F$. Hence $F$ is strictly decreasing on $(0,\mathrm{\infty })$, which is claim 1.

(Inverse and bijectivity.) Let $u>0$. By [L2] claim 1, $a_{\ast }\mathrm{/}u>0$, so $a_{\ast }\mathrm{/}u$ lies in the domain $(0,\mathrm{\infty })$ of $F$ and is nonzero; using associativity, commutativity and the inverse law in the field $\mathbb{R}$ ([F1]), $F(F^{-1}(u))=a_{\ast }(a_{\ast }\mathrm{/}u{)}^{-1}=a_{\ast }u{a}_{\ast }^{-1}=u$. Symmetrically, for $a>0$ one has $F^{-1}(F(a))=a_{\ast }(a_{\ast }{a}^{-1}{)}^{-1}=a_{\ast }a{a}_{\ast }^{-1}=a$. Thus $F$ and the map $u\mapsto a_{\ast }\mathrm{/}u$ are mutually inverse, so $F$ is a bijection of $(0,\mathrm{\infty })$ onto $(0,\mathrm{\infty })$; this is claim 2.

(Interval windows.) Let $0<u_1\le u_2$ and $a>0$. The inequality $F(a)\in [u_1,u_2]$ reads $u_1\le a_{\ast }{a}^{-1}\le u_2$; multiplying both inequalities by the positive number $a$ via [L1] claim 4 gives $u_{1}a\le a_{\ast }\le u_{2}a$, equivalently $u_{1}a\le a_{\ast }$ and $a_{\ast }\le u_{2}a$. Dividing the first inequality by the positive $u_1$ and the second by the positive $u_2$, again by [L1] claim 4, gives $a\le a_{\ast }\mathrm{/}{u}_1$ and $a\ge a_{\ast }\mathrm{/}{u}_2$, that is, $a\in [a_{\ast }\mathrm{/}{u}_2,a_{\ast }\mathrm{/}{u}_1]$. Conversely every $a$ in that interval satisfies $u_{1}a\le a_{\ast }\le u_{2}a$ and hence, after division by the positive $a$, lies in $F^{-1}([u_1,u_2])$; so $F^{-1}([u_1,u_2])=[a_{\ast }\mathrm{/}{u}_2,a_{\ast }\mathrm{/}{u}_1]$. The interval is nonempty because $u_1\le u_2$ and division of positive numbers reverses the reciprocal order ([L2] claim 2 applied to $u_1<u_2$, with the equality case $u_1=u_2$ giving coincident endpoints), and both endpoints are strictly positive by [L2] claim 1; this is the first part of claim 4.

(Point preimages.) Let $u>0$ and $a>0$. Multiplying the equation $a_{\ast }{a}^{-1}=u$ by the nonzero number $a$ and using field arithmetic gives $a_{\ast }=ua$; multiplying instead by the nonzero number $u^{-1}$ gives $a=a_{\ast }{u}^{-1}=a_{\ast }\mathrm{/}u$. Conversely $F(a_{\ast }\mathrm{/}u)=u$ by step 1.2. Hence $F(a)=u$ if and only if $a=a_{\ast }\mathrm{/}u$, and the point preimage is the singleton $\{a_{\ast }\mathrm{/}u\}$; this is claim 3.

(Length of the window.) The length of the interval of step 1.3 is $\frac{a_{\ast }}{u_1}-\frac{a_{\ast }}{u_2}=\frac{a_{\ast }{u}_2-a_{\ast }{u}_1}{u_1{u}_2}=\frac{a_{\ast }(u_2-u_1)}{u_1{u}_2}$, by field arithmetic. The denominator is a product of positive numbers, hence positive ([F1], [L1] claim 1), and the numerator is a product of $a_{\ast }>0$ with $u_2-u_1\ge 0$, hence nonnegative, and positive exactly when $u_2-u_1>0$ by the trichotomy in [F1]. Therefore the length is zero exactly when $u_1=u_2$ and strictly positive exactly when $u_1<u_2$, which completes claim 4.

Collecting the steps: claim 1 is step 1.1, claim 2 is step 1.2, claim 3 is step 2.1, and claim 4 is steps 1.3 and 2.2. No step uses calculus, a choice principle, a limit or a completeness property of $\mathbb{R}$ beyond the ordered field axioms of [F1]; the map and its inverse are explicit rational expressions.