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$X, A$ noncomputable c.e. setsets, say that $W_e$$A$ is efficiently below $X$ iff $\emptyset<_TW_e<_TX$$\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^{W_e}(u)\uparrow$$\Phi_a^{A}(u)\uparrow$ and if $i=1$ then $\Phi_a^{W_e}(u)=1-X(u)$$\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-W_e(v)$$\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.