Hard-to-"realize" instances of downward density This question is motivated by a vague analogy between true paths in priority arguments and realizers - relative to an oracle - in the sense of intuitionistic logic. Intuitively, I'm looking for a precise way to ask the following: "can downward density be proved without infinite injury?" (Incidentally, there is a vague similarity-of-purpose with this other question of mine.)
Precisely, for $X, A$ noncomputable c.e. sets, say that $A$ is efficiently below $X$ iff $\emptyset<_TA<_TX$ and there is a pair $(F,G)$ of ${\bf 0'}$-computable total functions with the following properties:

*

*For each $a\in\omega$, $F(a)$ is a pair $\langle u,i\rangle\in \omega\times 2$ such that if $i=0$ then $\Phi_a^{A}(u)\uparrow$ and if $i=1$ then $\Phi_a^{A}(u)=1-X(u)$; and


*For each $b\in\omega$, $G(b)$ is a pair $\langle v,j\rangle\in\omega\times 2$ such that if $j=0$ then $\Phi_b^\emptyset(v)\uparrow$ and if $j=1$ then $\Phi_b^\emptyset(v)=1-A(v)$.
My question, then, is the following:

Is there a noncomputable c.e. set with no noncomputable c.e. sets efficiently below it?

Note that if we were to replace ${\bf 0'}$ with ${\bf 0''}$ we would get a uniform-in-$X$ negative answer since the true path in the usual proof of Sacks density is ${\bf 0''}$-computable. Meanwhile, we would get a positive answer if we looked at general density instead of specificially downward density, but for boring reasons since any analogous "efficient" witness to an interval $(X,Y)$ being nonempty would a fortiori compute $X'$; this also shows that we get a trivial positive answer if we replace ${\bf 0'}$ by any smaller degree.
 A: Every noncomputable c.e. set has a noncomputable c.e. set efficiently below it. The reason is that "$A$ is efficiently below $X$" is equivalent to "$A$ is low" and it is possible to show that every noncomputable c.e. set has a noncomputable low c.e. set below it.
To prove this let me first restate your definitions a bit. Let's say that $X$ is efficiently not above $Y$ if there is a $0'$ computable function $F \colon \omega \to \omega\times 2$ such that for all $e$, one of the two following options holds.

*

*For some $n \in \omega$ we have $F(e) = (n, 0)$ and $\Phi^X_e(n)\uparrow$

*For some $n \in \omega$ we have $F(e) = (n, 1)$ and $\Phi^X_e(n)\downarrow \neq Y(n)$.
Now "$X$ is efficiently below $Y$" in your sense means that $X$ is efficiently not above $Y$, $0$ is efficiently not above $X$ and $X \leq_T Y$.

Claim 1. If $X$ and $Y$ are c.e. then $X$ is efficiently not above $Y$ if and only if $Y \nleq_T X$ and $X$ is low.
Proof. First suppose that $Y \nleq_T X$ and $X$ is low. Use $0'$ to compute $F$ witnessing that $X$ is efficiently not above $Y$ as follows. Given any $e$, search for an $n$ such that either $\Phi^X_e(n)\uparrow$ or $\Phi^X_e(n) = 0$ and $n$ eventually enters $Y$ or $\Phi^X_e(n) = 1$ and $n$ never enters $Y$. Note that for a fixed $n$ we can figure out if one of these three situations holds (and if so, which one) using $X'$ and hence $0'$ since $X$ is low. Also we are guaranteed to find at least one such $n$ since $X$ does not compute $Y$. Use this $n$ to define $F(e)$.
Now suppose $X$ is efficiently not above $Y$. Clearly this implies $Y \nleq_T X$. To see why it implies $X$ is low, let $F$ be a witness to $X$ being efficiently not above $Y$. Now use $F$ to compute $X'$ as follows. Given $e$, produce $\tilde{e}$ such that if $\Phi^X_e(e)$ diverges then $\Phi_{\tilde{e}}^X$ diverges on every input and if $\Phi^X_e(e)$ converges then $\Phi_{\tilde{e}}^X$ converges on every input. Note that $e \mapsto \tilde{e}$ is computable and the second bit of $F(\tilde{e})$ tells you whether $\Phi^X_e(e)$ converges or not.
Claim 2. If $0 <_T A <_T X$ are c.e. and $A$ is low then $A$ is efficiently below $X$.
Proof. Since $0$ is low and $X \nleq_T 0$, $0$ is efficiently not above $A$. Since $A$ is low and $A \nleq_T X$, $A$ is efficiently not above $X$. And since $A \leq_T X$ this implies $A$ is efficiently below $X$.
Claim 3. For any noncomputable c.e. set $X$ there is a low noncomputable c.e. set computable from $X$.
Proof. If $X$ is low then any set computable from it is also low so the usual density theorem can be applied directly. If $X$ is not low then any noncomputable low c.e. set below it must be strictly below it. But given a noncomputable c.e. set $X$ it is easy to construct a noncomputable low c.e. set $A \leq_T X$ using a finite injury construction (to make it low we simply want to preserve instances of programs converging, to make it noncomputable we occasionally want to put an element in and to make it below $X$ we can use permitting).
