A toolkit for the Dodd-Jensen core model

I just finished a note with some black boxes for the Dodd-Jensen core model $K^\text{DJ}$, the core model that cannot have a measurable cardinal. I am not an expert on core model theory, so this is just a  presentation of $K^\text{DJ}$, like painter A. Dürer’s presentation of a Rhinoceros (in the featured image), just by the descriptions of others, never having seen one himself. And perhaps my note is not as detailed as Dürer’s painting is, but I hope it’s a sufficient presentation for someone who just wants to get consistency strength from $K^{\text{DJ}}$ without having to go through all its glorious detail. One could say this is a note on applied set theory.

This note includes the trick to construct $K^{\text{DJ}}$ inside a model of ZF, by using the fact that  for any set of ordinals $x$, $(K^\text{DJ})^{\text{HOD}}=(K^\text{DJ})^{\text{HOD}[ x] }$ and this equality holds for every level of the $K^\text{DJ}$-construction.

There’s also a running example,  the proof that if $V$ is a model of ZF in which the Chang conjecture $(\omega_5,\omega_4)\twoheadrightarrow (\omega_3,\omega_1)$ holds,  $\omega_4$ is a regular cardinal, and cf$\omega_3>\omega$ then in $(K^\text{DJ})^{\text{HOD}}$, an Erdős cardinal exists, and in particular, $(K^\text{DJ})^{\text{HOD}}\models\omega_5^{V}\to(\omega_3^V)^{<\omega}_2$. This is an example of how to use these black boxes, and I think it helps clarify how this Rhinoceros model looks like. As always, there are pictures included – now in pgfpicture.

I’d be happy to get suggestions, corrections, and more $K^\text{DJ}$-black boxes and examples.