Forcing More DC Over the Chang Model Using the Thorn Sequence

In the context of $\mathsf{Z}\mathsf{F}+\mathsf{D}\mathsf{C}$, we force ${\mathsf{D}\mathsf{C}}_{\kappa }$ for relations on $\mathcal{P}(\kappa )$ for $\kappa <{\mathrm{\aleph }}_{\omega }$ over the Chang model $\mathrm{L}({\mathrm{O}\mathrm{r}\mathrm{d}}^{\omega })$ making some assumptions on the thorn sequence defined by ${\mathit{\text{unicode}}xFE}_0=\omega$, ${\mathit{\text{unicode}}xFE}_{\alpha +1}$ as the least ordinal not a surjective image of ${\mathit{\text{unicode}}xFE}_{\alpha }^{\omega }$ (i.e. no $f:{\mathit{\text{unicode}}xFE}_{\alpha }^{\omega }\to {\mathit{\text{unicode}}xFE}_{\alpha +1}$ is surjective) and ${\mathit{\text{unicode}}xFE}_{\gamma }={\sup }_{\alpha <\gamma }{\mathit{\text{unicode}}xFE}_{\alpha }$ for limit $\gamma$. These assumptions are motivated from results about $\mathrm{\Theta }$ in the context of determinacy, and could be reasonable ways of thinking about the Chang model. Explicitly, we assume cardinals $\lambda$ on the thorn sequence are strongly regular (meaning regular and functions $f:{\kappa }^{<\kappa }\to \lambda$ are bounded whenever $\kappa <\lambda$ is on the thorn sequence) and justified (meaning $\mathcal{P}({\kappa }^{\omega })\cap \mathrm{L}({\mathrm{O}\mathrm{r}\mathrm{d}}^{\omega })\subseteq {\mathrm{L}}_{\lambda }({\lambda }^{\omega },X)$ for some $X\subseteq \lambda$ for any $\kappa <\lambda$ on the thorn sequence). This allow us to use Cohen forcing and establish more dependent choice.