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$\mathrm{.}If$\boldsymbol\Pi^1_n$determinacyand$\Pi^1_{n+1}$ determinacy both hold true and there is no ${\mathbf{\Sigma }}_{n+2}^1$-definable ${\omega }_1$-sequence of pairwise distinct reals, then $M_n^{\mathrm{\#}}$ exists and is ${\omega }_1$-iterable. The proof yields that ${\mathbf{\Pi }}_{n+1}^1$ determinacy implies that $M_n^{\mathrm{\#}}(x)$ exists and is ${\omega }_1$-iterable for all reals $x$. A consequence is the Determinacy Transfer Theorem for arbitrary $n\ge 1$, namely the statement that ${\mathbf{\Pi }}_{n+1}^1$ determinacy implies ${\mathrm{⅁}}^{(n)}(<{\omega }^2-{\mathbf{\Pi }}_1^1)$ determinacy.