Müller, S., Schindler, R., & Woodin, W. H. (2016). Mice with Finitely many Woodin Cardinals from Optimal Determinacy Hypotheses.

We prove the following result which is due to the third author. Let $n \geq 1$. If $\boldsymbol\Pi^1_n$ determinacy and $\Pi^1_{n+1}$ determinacy both hold true and there is no $\boldsymbol\Sigma^1_{n+2}$-definable $\omega_1$-sequence of pairwise distinct reals, then $M_n^\sharp$ exists and is $\omega_1$-iterable. The proof yields that $\boldsymbol\Pi^1_{n+1}$ determinacy implies that $M_n^\sharp(x)$ exists and is $\omega_1$-iterable for all reals $x$. A consequence is the Determinacy Transfer Theorem for arbitrary $n \geq 1$, namely the statement that $\boldsymbol\Pi^1_{n+1}$ determinacy implies $\Game^{(n)}(<\omega^2 - \boldsymbol\Pi^1_1)$ determinacy.