**Context:** This question is about constructive mathematics, such as in the internal logic of a topos with natural numbers object, or in [IZF](https://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html). (I wish to avoid the axiom of countable choice if possible, but a partial answer in, say, Bishop-style constructive mathematics — which has dependent choice — is still interesting.) ❧ By “real numbers” (and the set $\mathbb{R}$ of them) I mean the *Dedekind* reals, as defined in A. S. Troelstra & D. van Dalen, *Constructivism in Mathematics* (1988), chapter 5, section 5, or in P. Johnstone, *Sketches of an Elephant* (2002), section D.4.7.
The following principles are standard at least under the assumption of countable choice (in its absence, the subscript $\mathbb{R}$ is used to distinguish them from analogous principles about binary sequences):
* $\mathbf{LPO}_{\mathbb{R}}$ is the statement that for all $a\in\mathbb{R}$ we have $a<0$ or $a=0$ or $a>0$.
* $\mathbf{WLPO}_{\mathbb{R}}$ is the statement that for all $a\in\mathbb{R}$ we have $a\lessdot 0$ or $a=0$ or $a\gtrdot 0$.
* $\mathbf{LLPO}_{\mathbb{R}}$ is the statement that for all $a\in\mathbb{R}$ we have $a\leq 0$ or $a\geq 0$.
— where “$a\lessdot 0$” is defined as “$\neg(a\geq 0)$” (where $a\geq 0$ is itself equivalent to $\neg(a<0)$) and analogously for “$a\gtrdot 0$”. (Note that $a>0$ implies $a\gtrdot 0$ and that the latter implies $a\geq 0$, so $\mathbf{LPO}_{\mathbb{R}}$ implies $\mathbf{WLPO}_{\mathbb{R}}$ and the latter implies $\mathbf{LLPO}_{\mathbb{R}}$.)
**Definition:** Let me further call $\mathbf{CPO}$ (for “Convexity Principle of Omniscience”, my terminology) the statement that if $c\geq 0$ then $[0,c] = c·[0,1]$, or equivalently:
> if $0\leq x\leq c$ then there is $0\leq t\leq 1$ such that $x = c·t$
(it's sufficient to demand that there is $t\in\mathbb{R}$ such that $x = c·t$ because then $t' = 0\sqcup(t\sqcap 1)$ will satisfy $0\leq t'\leq 1$ and still $x = c\cdot t'$, where $\sqcap$ and $\sqcup$ denote the binary inf and sup operations on $\mathbb{R}$).
**The question:** has the above-defined $\mathbf{CPO}$ been studied in relation to $\mathbf{LPO}_{\mathbb{R}}$, $\mathbf{WLPO}_{\mathbb{R}}$ and $\mathbf{LLPO}_{\mathbb{R}}$ and similar principles? Does it have a standard name? Is it equivalent to one of the three?
----
To motivate my question, let me show that:
* $\mathbf{LPO}_{\mathbb{R}} \Rightarrow \mathbf{CPO}$: We want to show that if $0\leq x\leq c$ then there is $0\leq t\leq 1$ such that $x = c·t$. By $\mathbf{LPO}_{\mathbb{R}}$ we can assume that $c<0$ or $c=0$ or $c>0$. The first case trivially contradicts $c\geq 0$. In the second, we have $x=0$, so $t=0$ works. In the third case, $c$ is invertible (as $\mathbb{R}$ is a Heyting field) so we can let $t = x/c$ which works (and by a remark made above we \[can\] have $0\leq t\leq 1$).
* $\mathbf{CPO} \Rightarrow \mathbf{LLPO}_{\mathbb{R}}$: If $a\in\mathbb{R}$, applying $\mathbf{CPO}$ to $x := \frac{1}{2}(a + c)$ where $c := |a|$, which satisfies $0\leq x\leq c$, we see that¹ there is $-1\leq u\leq 1$ (namely $2t-1$ where $x=c\cdot t$) such that $a = u·|a|$. Now by a fundamental property of the Dedekind reals (Troelstra & van Dalen, *op. cit.*, chapter 5, theorem 5.12(iii)(h)), we have either $u<1$ or $u>-1$. But $u<1$ contradicts $a>0$ (because then $|a|=a$ is invertible so necessarily $u=1$), in other words, $u<1$ implies $a\leq 0$, and similarly $u>-1$ implies $a\geq 0$. So we have $a\leq 0$ or $a\geq 0$, as claimed.
1. \[**Corrected**\] The statement that for if $|a|\leq c$ then there is $u\in[-1,1]$ such that $a = c\cdot u$ is, in fact, clearly equivalent to $\mathbf{CPO}$ and maybe more satisfactory.
I have not been able to prove the converse of one of these two implications, nor to relate $\mathbf{CPO}$ with $\mathbf{WLPO}_{\mathbb{R}}$, hence my question.
I also didn't find the statement I called $\mathbf{CPO}$ above in [Hannes Diener's long text on “Constructive Reverse Mathematics”](https://arxiv.org/abs/1804.05495), though of course I may have missed it, but I'd be surprised if it hasn't been considered (and named) before.