The covering-with-Chang-models conjecture

Assume $obreak\textsf{NLE}$ and suppose there are unboundedly many Woodin cardinals and strong cardinals. Let $obreak\textsf{NLE}$ denote the assertion that there is no active $obreak\textsf{\omega}_1+1$-iterable countable mouse or lbr mouse whose last extender is a long extender. Let $obreak\textsf{ZFC-Powerset}$ denote ZFC without the powerset axiom. Let $obreak\textsf{AD}^+$ denote the strengthened axiom of determinacy, and let $obreak\textsf{Coll}(\omega,<\kappa)$ be the Levy collapse. If $obreak\kappa$ is a limit of Woodin cardinals and strong cardinals such that either $obreak\kappa$ is measurable or $obreak\operatorname{cf}(\kappa)=\omega$, then there is a transitive model $M$ of $obreak\textsf{ZFC-Powerset}$ satisfying: (1) $obreak\operatorname{Ord}\cap M=\kappa^+$; (2) $M$ has a largest cardinal $obreak\nu$; (3) for every generic $obreak g\subseteq\operatorname{Coll}(\omega,<\kappa)$, defining $obreak\mathbb{R}^*=\bigcup_{\alpha<\kappa}\mathbb{R}^{V[g\cap\operatorname{Coll}(\omega,\alpha)]}$ and $obreak\Gamma^*=\{A^g\cap\mathbb{R}^*: \exists\alpha<\kappa\,(A\in\Gamma^\infty_{g\cap\operatorname{Coll}(\omega,\alpha)})\}$, one has

$$L\left(M,\bigcup_{\alpha<\nu}\alpha^\omega,\Gamma^*,\mathbb{R}^*\right)\vDash\textsf{AD}^+;$$

and (4), if there is no inner model with a subcompact cardinal, then

$$L(M)\vDash\textsf{ZFC}+{\wp}(\nu)={\wp}(\nu)^M+\square_\nu.$$

Covering with Chang Models conjecture. The asserted transitive model $M$ exists with all the listed properties. This conjecture is intended to overcome limitations of the core model induction and would yield consequences for the Proper Forcing Axiom, including an inner model with a subcompact cardinal. Its resolution status is not given in the supplied text.