\documentclass[11pt,reqno]{amsart} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage[margin=1.08in]{geometry} \usepackage{amssymb,mathtools,enumitem,microtype} \usepackage[hidelinks,bookmarksnumbered]{hyperref} \hypersetup{pdftitle={Under measurables, HOD\textunderscore\{Ord\textasciicircum omega\} is locally arbitrary},pdfsubject={KW Conservativity v18: three-theory Woodin rank equiconsistency}} \usepackage{fancyhdr} \setlength{\headheight}{13pt} \numberwithin{equation}{section} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{convention}[theorem]{Convention} \newtheorem{question}[theorem]{Question} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\Ord}{\mathrm{Ord}} \newcommand{\HOD}{\mathrm{HOD}} \newcommand{\OD}{\mathrm{OD}} \newcommand{\ZF}{\mathsf{ZF}} \newcommand{\ZFC}{\mathsf{ZFC}} \newcommand{\DC}{\mathsf{DC}} \newcommand{\SVC}{\mathsf{SVC}} \newcommand{\CM}{\mathsf{CM}} \newcommand{\CW}{\mathsf{CW}} \newcommand{\PCW}{\CW} \newcommand{\HYP}{\operatorname{HYP}} \newcommand{\CS}{\mathsf{CS}} \newcommand{\GCH}{\mathsf{GCH}} \newcommand{\GA}{\mathsf{GA}} \newcommand{\KW}{\mathsf{KW}^{*,\omega}_1} \newcommand{\Con}{\operatorname{Con}} \newcommand{\Add}{\operatorname{Add}} \newcommand{\Col}{\operatorname{Col}} \newcommand{\RO}{\operatorname{RO}} \newcommand{\TC}{\operatorname{TC}} \newcommand{\ran}{\operatorname{ran}} \newcommand{\dom}{\operatorname{dom}} \newcommand{\cf}{\operatorname{cf}} \newcommand{\otp}{\operatorname{otp}} \newcommand{\id}{\operatorname{id}} \newcommand{\fin}{\mathrm{fin}} \newcommand{\Hseq}{\mathcal H} \newcommand{\forces}{\Vdash} \newcommand{\sq}{\subseteq} \newcommand{\restr}{\restriction} \newcommand{\seq}[1]{\langle #1\rangle} \newcommand{\Pow}{\mathcal P} \newcommand{\pp}{\mathbb P} \newcommand{\qq}{\mathbb Q} \newcommand{\rr}{\mathbb R} \newcommand{\cc}{\mathbb C} \newcommand{\bb}{\mathbb B} \newcommand{\ssS}{\mathbb S} \newcommand{\ttT}{\mathbb T} \newcommand{\UU}{\mathcal U} \newcommand{\Dens}{\mathcal D} \newcommand{\sym}{\triangle} \newcommand{\sm}{\mathbin{\subseteq^*}} \newcommand{\eqf}{\mathrel{=^*}} \setlist[enumerate]{label=\textup{(\arabic*)},leftmargin=2.3em,itemsep=3pt,topsep=5pt} \setlist[itemize]{leftmargin=1.7em,itemsep=2pt,topsep=4pt} \setlength{\emergencystretch}{2em} \pagestyle{fancy} \fancyhf{} \fancyhead[LE,RO]{\small\thepage} \fancyhead[LO,RE]{\small Under measurables, $\HOD_{\Ord^{\omega}}$ is locally arbitrary} \renewcommand{\headrulewidth}{0pt} \title[Under measurables, $\HOD_{\Ord^{\omega}}$ is locally arbitrary]{Under measurables, $\mathrm{HOD}_{\mathrm{Ord}^{\omega}}$ is locally arbitrary} \author{} \date{October 12, 2026} \subjclass[2020]{03E25, 03E35, 03E45, 03E55} \keywords{ordinal definability, dependent choice, symmetric extensions, Prikry forcing, measurable cardinals, Woodin cardinals, inner models} \begin{document} \begin{abstract} For the inner model $\HOD_{\Ord^{\omega}}$, we derive an analogue for Roguski's classical result that without nontrivial assumptions on $V$, $\HOD$ is an arbitrary model of $\ZFC$. For any sentence $\sigma$, letting $\CM$ denote ``class of measurables,'' the following theories are equiconsistent: \begin{enumerate} \item $\ZFC+\CM+ [\HOD_{\Ord^{\omega}}\models (\exists\kappa\,V_{\kappa}\models\sigma)]$; \item $\ZFC+\GCH+\CM+ [\HOD_{\Ord^{\omega}}\models (\SVC\wedge\CM\wedge\exists\kappa\,V_{\kappa}\models\sigma)]$; \item $\ZF+\DC+\CM+ \exists\kappa\,V_{\kappa}\models\sigma$. \end{enumerate} Thus, under measurables the only local constraint on $\HOD_{\Ord^{\omega}}$ is the requisite choice principle. We also derive an analogue for Woodins. Letting $\CW$ denote ``class of Woodins,'' the following are equiconsistent: \begin{enumerate} \item $\ZFC+\CW+ [\HOD_{\Ord^{\omega}}\models (\exists\kappa\,V_{\kappa}\models\sigma)]$; \item $\ZFC+\GCH+\CW+ [\HOD_{\Ord^{\omega}}\models (\exists\kappa\,V_{\kappa}\models\sigma)]+$ $\HOD_{\Ord^{\omega}}$ is a ground of $V$; \item $\ZFC+\CW+$ some symmetric extension $V(G) \models \DC+\exists\kappa\,V_{\kappa}\models\sigma$. \end{enumerate} \end{abstract} \maketitle \setcounter{tocdepth}{1} \tableofcontents \section{External HOD and local arbitrariness}\label{sec:intro} Roguski's work on the theory of $\HOD$ is the starting point for this paper \cite{Roguski}. In the countable transitive formulation of his realization theorem, every countable transitive model $M$ of $\ZFC$ has a larger model $N$ of $\ZFC$ such that \[ M=\HOD^N. \] Ordinary $\HOD$ can thus realize a prescribed $\ZFC$ universe. We seek an analogue when definitions may use countable sequences of ordinals as parameters. Our first result concerns the theories of rank segments of the resulting inner model under a class of measurable cardinals. A second result relates its rank theory under a proper class of Woodins to that of symmetric extensions of Woodin grounds. For $U\models\ZFC$, write \[ \Hseq^U=\HOD_{\Ord^\omega}^U. \] An allowed parameter is one function from $\omega$ to the ordinals, together with finitely many ordinal parameters; the hereditary requirement is retained. This inner model contains every ordinal $\omega$-sequence of $U$ and satisfies $\ZF+\DC$ (Lemma~\ref{lem:HDC}). The local analogue of Roguski's theorem will therefore compare its rank theory with that of choiceless models satisfying dependent choice. Write $\CM$ for the assertion that measurable cardinals are unbounded in the ordinals, abbreviated as ``class of measurables.'' A measurable cardinal is uncountable and carries a nonprincipal, cardinal-complete ultrafilter. We require normality only in choice models. Put \[ T_0=\ZF+\DC+\CM. \] For each first-order sentence $\sigma$, consider the theories \begin{align*} E_1(\sigma)&=\ZFC+\CM+ [\Hseq\models\exists\kappa\,(V_\kappa\models\sigma)],\\ E_2(\sigma)&=\ZFC+\GCH+\CM+ [\Hseq\models\SVC\wedge\CM\wedge\exists\kappa\,(V_\kappa\models\sigma)],\\ E_3(\sigma)&=T_0+\exists\kappa\,(V_\kappa\models\sigma). \end{align*} In the first two theories, the witnessing rank is computed inside $\Hseq$. Theory $E_2$ requires GCH in the ambient universe and SVC together with a class of measurables inside $\Hseq$. Our first main result is the following. \begin{theorem}[External rank equiconsistency]\label{thm:external-main} For every $\sigma$, \[ \Con(E_1(\sigma))\ \longleftrightarrow\ \Con(E_2(\sigma))\ \longleftrightarrow\ \Con(E_3(\sigma)). \] \end{theorem} This is the sense in which $\HOD_{\Ord^\omega}$ is locally arbitrary under measurables. Every rank-sentence assertion consistent with $\ZF+\DC+\CM$ can hold inside the sequence-parameter HOD of a $\ZFC+\GCH+\CM$ universe, even when that HOD is itself required to satisfy $\SVC+\CM$. GCH is imposed on the ambient universe, so it does not restrict the rank theory being realized inside $\Hseq$. The comparison concerns consistency of rank-sentence theories. Exact realization of an entire starting model is available under the prepared-ground hypotheses stated below. \subsection{The Woodin equiconsistency} Write $\PCW$ for the assertion that Woodin cardinals are unbounded in the ordinals. For a fixed first-order sentence $\sigma$, put \[ R_\sigma\equiv\exists\alpha\,(V_\alpha\models\sigma). \] Consider the following three theories: \begin{align*} W_1(\sigma)&=\ZFC+\PCW+[\Hseq\models R_\sigma],\\ W_2(\sigma)&=\ZFC+\PCW+ [\text{some set-symmetric extension satisfies }\DC+R_\sigma],\\ W_3(\sigma)&=\ZFC+\GCH+\PCW+[\Hseq\models R_\sigma]\\ &\qquad+[\Hseq\text{ is a symmetric ground of }V]. \end{align*} The symmetric extension in $W_2$ is a model of $\ZF$. The assertion $\PCW$ is imposed on its $\ZFC$ ground, and need not hold in the symmetric extension. To read $W_2$ syntactically, assert the existence of a set symmetric system and a condition forcing $\DC+R_\sigma$ under the hereditary-symmetric interpretation. The symmetric forcing theorem supplies $\ZF$ in that interpretation. In $W_3$, both GCH and $\PCW$ are assertions about the ambient universe. We impose no Woodin-cardinal assertion on $\Hseq$. The term symmetric ground has its set-forcing meaning. In a $\ZFC$ ambient universe, it is equivalent to being an ordinary set-forcing ground, which may fail choice \cite[Corollary~5.9]{Usuba}. \begin{theorem}[Woodin rank equiconsistency]\label{wd-main} For every fixed first-order sentence $\sigma$, \[ \Con(W_1(\sigma))\ \longleftrightarrow\ \Con(W_2(\sigma))\ \longleftrightarrow\ \Con(W_3(\sigma)). \] \end{theorem} The proof preserves the relevant membership structure $V_\alpha$. It uses a relative inner model containing a given real and a proper class of Woodins, together with a set-forcing presentation of that inner model over its own HOD. The relative construction is invariant under Turing-equivalent recodings in the same ambient universe. These properties allow the collapse argument to descend to a model with the required rank and dependent choice. For the converse, retain the Woodin ground of the given symmetric extension. Its old normal measures supply the local Prikry construction. After the sequence generator has been coded, a bounded homogeneous code makes enough of the original ground ordinal-definable to recover the prescribed rank. This uses only set forcing over the Woodin ground. This rank-realization argument works over the original $W_2$ ground without an eventual-GCH hypothesis. To obtain $W_3$, we instead use the particular ground supplied by the reverse construction. It satisfies eventual GCH, and each of its sets is internally definable from ordinals and one fixed set parameter. A bounded $\diamondsuit^*$ code makes that parameter and a ground-defining parameter ordinal-definable while preserving GCH. The spectrum then recovers the whole sequence-generated model as $\Hseq$, with the ambient universe a set-forcing extension of it. This proves the consistency strengthening without a class preparation preserving Woodin cardinals. \subsection{Realization and rank preservation} The construction first preserves a specified rank while passing to a model generated by a set of ordinal sequences. It then realizes that rank inside external HOD. Two presentation principles enter the first step. Write $\SVC(S)$ when every nonempty set is a surjective image of $\eta\times S$ for some ordinal $\eta$; $\SVC$ asserts that such a set $S$ exists. The assertion $\KW$ says that every nonempty set is a surjective image of $\mu^\omega$ for some ordinal $\mu$, with the sequence power computed in the model under discussion. Write $T_{\mathrm{s}}=T_0+\SVC$. The external realization step takes the following form. \begin{theorem}[External realization]\label{thm:external-realization} Suppose $M\models T_0+\SVC+\KW$. For every ordinal $\alpha$ there is an outer model $U\models\ZFC+\GCH+\CM$ of $M$ such that \[ \Hseq^U\models\SVC+\CM,\qquad V_\alpha^{\Hseq^U}=V_\alpha^M. \] If $M$ has a presentation as in Proposition~\ref{prop:secure-realize} whose choice envelope satisfies eventual GCH, one may require $\Hseq^U=M$. \end{theorem} The secure-ground case gives equality with the whole generated model by further set forcing over its fresh choice envelope. The general preparation uses class forcing, so the outer model in Theorem~\ref{thm:external-realization} is not asserted to be a set-forcing extension of $M$. The next theorem supplies the required presentation while retaining any chosen rank and its full power set. In particular, SVC is not an assumption on the original model. Here $D(A)$ denotes the model generated over a transitive base. It contains $D$ and the transitive closure of $\{A\}$. \begin{theorem}[Rank transfer without SVC]\label{thm:rank-transfer} Suppose $V\models T_0$ and $\alpha\in\Ord$. In a set-generic extension of $V$ there is a model $M$ such that \[ M\models T_0+\SVC+\KW,\qquad V_\alpha^M=V_\alpha^V,\qquad \Pow(V_\alpha^V)^M=\Pow(V_\alpha^V)^V. \] Moreover, $M=D(A)$ for a choice symmetric ground $D\models\ZFC+\CM$ and a set $A\sq\mu^\omega$. \end{theorem} The model $M$ contains a rank-preserving SVC inner model of $V$, but need not contain all of $V$. Once the starting model satisfies SVC, the local construction also gives containment. \begin{theorem}[Local rank-to-sequence transfer]\label{thm:transfer-intro} Suppose $N\models T_{\mathrm{s}}$ and $\alpha\in\Ord$. In a set-generic extension of $N$ there is an inner model $M$ containing $N$ such that \[ M\models T_{\mathrm{s}}+\KW,\qquad V_\alpha^M=V_\alpha^N. \] More precisely, one can choose $\lambda>\alpha$ and $X=V_\lambda^N$ so that \[ \Pow(X)^M=\Pow(X)^N,\qquad V_\lambda^M=X. \] There are a choice symmetric ground $D\models\ZFC+\CM$, an ordinal $\mu$, and $A\sq\mu^\omega$ in $M$ such that $M=D(A)$. \end{theorem} The two transfer statements also give the following equiconsistency. \begin{corollary}[Rank-sentence equiconsistency]\label{cor:ranksentence} For every first-order sentence $\sigma$, the theories \[ T_0+\exists\alpha\,(V_\alpha\models\sigma) \quad\hbox{and}\quad T_0+\SVC+\KW+\exists\alpha\,(V_\alpha\models\sigma) \] are equiconsistent. \end{corollary} \begin{proof} Apply Theorem~\ref{thm:rank-transfer} to a witnessing rank. The converse is immediate. \end{proof} Combining rank transfer with external realization gives the implication from $E_3(\sigma)$ to $E_2(\sigma)$ at the level of consistency. The implication from $E_2(\sigma)$ to $E_1(\sigma)$ is immediate. For the remaining implication, Proposition~\ref{prop:one-three} uses core-model preparation and homogeneous descent to obtain an inner model of the given sequence-parameter HOD while retaining its witnessing rank. This step does not assume that the original HOD already has a class of measurables. \subsection{Structural conservativity} The rank-preserving construction also yields a structural conservativity theorem. This result concerns full second-order truth in arbitrary set-sized structures and allows a starting theory without Foundation. Put \[ T_-=(\ZF-\mathsf{Foundation})+\DC+\CM. \] \begin{definition}[Structural $\Pi_2$ sentences]\label{def:structural-pi2} A \emph{structural $\Pi_2$ sentence} is a set-theoretic assertion of the form \[ \forall\mathcal M\, (\mathcal M\text{ is a set-sized }\mathcal L\text{-structure} \ \Longrightarrow\ \mathcal M\models_{\mathrm{full}}\varphi), \] where $\varphi$ is a fixed second-order sentence in a finite signature $\mathcal L$. Satisfaction uses full second-order semantics: if $A$ is the domain of $\mathcal M$, each $n$-ary second-order relation variable ranges over all of $\Pow(A^n)$ in the ambient universe. This assertion has a $\Pi_2$ formulation in the L\'evy hierarchy. The second-order quantifier complexity of $\varphi$ is unrestricted. \end{definition} \begin{theorem}[Structural conservativity]\label{thm:main} The theory $T_0+\SVC+\KW$ is conservative over $T_-$ for structural $\Pi_2$ assertions. That is, for every fixed full second-order sentence $\varphi$, the assertion that $\varphi$ holds in every set-sized structure has the same provability in the two theories. \end{theorem} Foundation removal preserves structural truth. Theorem~\ref{thm:main} does not identify the non-well-founded membership structure of an arbitrary starting universe with a rank of a well-founded model. The argument represents a full second-order counterexample by a structure on atoms. After the local forcing construction, fibers of ordinal-sequence surjections give a pure copy of that structure and of an SVC witness. The full power sorts retain the truth of the original sentence. \begin{remark}[Role of the core-model preparation]\label{rem:prior} The core-model argument gives a passage to SVC that preserves each specified rank. We use this rank-preserving result directly. The proof constructs a uniform choice model over the coding real inside relative HOD, using the core model in the negative branch. Canonical refinement preserves its pure universe under finite recodings and gives a set-forcing presentation over its own HOD. The proof does not require $V=\HOD(r)$. The earlier $\SVC+\mathsf{KW}^{*,1}_1$ conservativity result is compatible with this preparation and is not an additional hypothesis of the structural conservativity theorem. \end{remark} \subsection{Limits of the conclusions} The large-cardinal assumption cannot simply be deleted from Theorem~\ref{thm:external-main}. Put $\mathbb R=\Pow(\omega)$ and \[ A_L\quad\equiv\quad \mathbb R=\mathbb R^L\ \wedge\ \omega_2=\omega_2^L. \] Over $\ZF$, this agreement implies that every countable ordinal sequence belongs to $L$. To see this, fix such a sequence $s$ and apply Jensen covering in the choice model $L[s]$. A constructible cover of its range has size at most $\omega_1$ there. Agreement at $\omega_2$ makes its constructible size at most $\omega_1$ as well; agreement on reals then returns $s$ to $L$. Thus \[ \ZF+A_L+\KW\ \vdash\ \mathsf{AC}. \] Likewise, if $\Hseq^U\models A_L$ for $U\models\ZFC$, all its allowed sequence parameters are constructible, and $\Hseq^U=\HOD^U$. A symmetric extension of $L$ using countable conditions and countable supports satisfies $\ZF+\DC+A_L$ while $\Pow(\omega_1)$ is not wellorderable and $\DC_{\omega_1}$ fails. Appendix~\ref{app:no-meas} gives the construction and a single guarded rank sentence $\sigma$ that can hold in this model but in no rank of any external $\Hseq^U$. Hence the rank-equiconsistency conclusion itself fails when $\CM$ is removed. There is also an obstruction below measurables to the structural conservativity theorem. Let $\mathsf{CR}$ assert a class of Ramsey cardinals, with Ramseyness understood as $\kappa\longrightarrow(\kappa)^{<\omega}_2$. There is a parameter-free $\Pi^2_3$ sentence $\Phi$ of third-order arithmetic such that, for $T_{\mathrm R}=\ZF+\DC+\mathsf{CR}$, \[ T_{\mathrm R}+\KW\vdash\Phi, \qquad \Con(\ZFC+\mathsf{CR})\Longrightarrow\Con(T_{\mathrm R}+\neg\Phi). \] Its semantic form over this base is \[ \bigl[\neg\exists 0^\dagger\ \wedge\ \mathbb R=\mathbb R^K\ \wedge\ \omega_2=\omega_2^K\bigr] \ \Longrightarrow\ \mathsf{Fodor}(\omega_1), \] where $K$ is the classical Dodd--Jensen core computed in HOD. The Ramsey class and the absence of $0^\dagger$ exclude an inner model with a measurable. Strong covering then returns every countable ordinal sequence to $K$, so $\KW$ implies Choice under the displayed agreement. A countably supported symmetric extension of the classical core retains the agreement, DC, and a class of Ramseys, but has a stationary regressive map with no stationary fiber. Appendix~\ref{app:ramsey} proves the claim and gives its third-order formulation. The $\Pi^2_3$ bound counts quantifiers over sets of reals; it is not a claim of minimal complexity. The same sentence has a structural formulation as in Definition~\ref{def:structural-pi2}. Thus $\mathsf{CR}$ cannot replace $\CM$ in Theorem~\ref{thm:main}. The choice of inner model matters as well. Let $C=L[\Ord^\omega]$ denote the Chang model, the least transitive inner model of $\ZF$ containing every countable ordinal sequence. Under the same ambient measurables, its failure of SVC prevents the strengthened conclusion of Theorem~\ref{thm:external-main}. \begin{proposition}[The Chang obstruction]\label{prop:chang-no-svc} If $U\models\ZFC+\CM$, then $C^U\models\neg\SVC$. \end{proposition} \begin{proof} Every member of $C$ is uniquely definable over $C$ from a countable ordinal sequence, with finite ordinal parameters absorbed into that sequence \cite[Section~1.2]{MitchellChang}. For a normal ultrapower $j:U\to M$, countable closure gives $C^M=C^U$; hence $j\restr C:C\to C$ is elementary. We also use Kunen's finite-movement lemma: after choosing normal measures at distinct measurable cardinals, each ordinal is moved by only finitely many of the corresponding ultrapowers \cite[Lemma~4.10]{CarlSchlichtWelch}. The stated form follows from the countable-sequence version by selecting infinitely many exceptions if they exist. Suppose $S\in C$ witnesses SVC. Choose an uncountable set $I$ of ambient measurables above $\operatorname{rank}(S)$, with a normal measure at each, and let $\lambda>\sup I$. There is in $C$ a surjection $f:\eta\times S\twoheadrightarrow\lambda^\omega$; Chang contains the full ambient sequence space. Let $p\in\Ord^\omega$ define $f$ uniquely over $C$. Only countably many of the selected ultrapowers move a coordinate of $p$. Choose distinct remaining measurables $\seq{\kappa_n:n<\omega}$ and put $z=\seq{\kappa_n:n<\omega}$. Take one preimage $f(\xi,s)=z$. Some selected ultrapower $j$ with critical point $\kappa_n$ fixes $\xi$. It fixes $s$ by rank and fixes $f$ by its definition from $p$ over the unchanged Chang model. Therefore \[ j(z)=j(f)(j(\xi),j(s))=f(\xi,s)=z, \qquad j(z)(n)=j(\kappa_n)>\kappa_n=z(n), \] a contradiction. All choices here are made in $U$. \end{proof} Replacing $\Hseq$ by $C$ in $E_2(\sigma)$ therefore makes that theory inconsistent for every $\sigma$. This already rules out the three-way Chang replacement. The proposition uses internal definability over Chang and its invariance under ambient normal ultrapowers. It does not assert invariance of the ambiently computed $\HOD_{\Ord^\omega}$, nor does global failure of SVC exclude SVC from each individual Chang rank. Even the comparison of theories (1) and (3) can fail after replacing $\Hseq$ by $C$. Relative to $\ZFC$ with a proper class of strong cardinals and an inaccessible limit of strong cardinals, there is a sentence $\sigma$ for which theory (3) is consistent but the Chang version of theory (1) is inconsistent. Appendix~\ref{app:chang} gives the statement and proof. This explains why the choice of $\HOD_{\Ord^\omega}$ matters even without the SVC requirement in theory (2). Whether an anti-inner-model hypothesis restores the two-way comparison remains open; Question~\ref{q:chang-anti-inner} considers excluding inner models with a measurable of Mitchell order at least two. \subsection{Proof outline and formalization} Sections~\ref{sec:prelim}--\ref{sec:transfer} prove the local rank-to-sequence theorem. A high Prikry sequence and a countably closed labeling forcing produce $Q\sq\kappa^\omega$ and $F:Q\twoheadrightarrow X$. Paired comparison removes the labeling coordinate from low-rank names while keeping their values fixed. External countable domination gives DC in $N(Q,F)$. Section~\ref{sec:remove-svc} supplies the initial passage to SVC without changing the protected rank. The core-model and atomization reductions originate in the research archive \cite{ResearchArchive}; Section~\ref{sec:foundation} gives the atomization and fiber purification needed for structural conservativity. Sections~\ref{sec:external-basics}--\ref{sec:finish} complete the external-HOD argument. Sparse Cohen rows with evaluated terminal caps code the sequence generator over a recognizable choice envelope. The code makes the generator ordinal-definable, while homogeneous descent bounds the resulting HOD by the intended model. Repeated $\diamondsuit^*$ codes provide a secure ground with eventual GCH. A countably closed collapse gives GCH in the choice envelope, and the final coding preserves it. The measurable consistency implications combine this realization with the rank-preserving preparation. Sections~\ref{wd-inner-model-section}--\ref{wd-consistency-section} prove the Woodin theorem. The relative fully backgrounded construction and its top-iteration alternative give a canonical choice inner model with a proper class of Woodins, presented by set forcing over its own HOD. Homogeneous descent produces the required symmetric model. In the other direction, an old-ground form of the local Prikry construction and bounded high coding realize its protected rank. Section~\ref{wd-exact-section} uses the special reverse ground to obtain GCH and exact equality with a symmetric ground. The proof first codes a fixed approximation-and-cover parameter, then places the spectrum above that code. This identifies the full choice envelope in the final universe. Every forcing used in the Woodin argument is set forcing. Appendix~\ref{app:chang} gives the separate strong-cardinal obstruction to the Chang replacement. We use transitive-model notation for the forcing and inner-model interpretations. This notation does not assume that consistency supplies a transitive model. The set-forcing arguments use the forcing theorem. Generated models use the definable transitive-base construction, and the Foundation-free construction uses the interpreted cumulative hierarchy over a set of atoms. These constructions can equivalently be carried out over countable models, using their internal notions of well-foundedness and satisfaction. The KW and Foundation reductions in Sections~\ref{sec:prelim}--\ref{sec:foundation} use only set forcing. The measurable exact-realization preparation uses the progressively closed $\diamondsuit^*$ coding of Section~\ref{sec:envelope}. Each of its set arguments takes place in a set-sized initial segment. \section{Small forcing and generated-model presentations}\label{sec:prelim} \begin{lemma}[Small forcing in $\ZF$]\label{lem:ZFmeasure} Let $V\models\ZF$, let $\bb\in V$ be a complete Boolean algebra, and let $\UU$ be a nonprincipal $\kappa$-complete ultrafilter on $\kappa$, where $\kappa>h(\bb)$. For every $V$-generic $G\sq\bb$, the filter \[ \UU^G=\{a\in\Pow(\kappa)^{V[G]}:\exists b\in\UU\ (b\sq a)\} \] is a nonprincipal $\kappa$-complete ultrafilter in $V[G]$. In particular, arbitrary set forcing over $\ZF$ preserves a proper-class tail of measurable cardinals. \end{lemma} \begin{proof} For a name $\dot a\sq\check\kappa$, the range of \[ \zeta\longmapsto\|\check\zeta\in\dot a\|_{\bb} \] is canonically well-orderable by least preimages. Its cardinality is below $h(\bb)$, hence below $\kappa$. The partition into Boolean-value fibers therefore has a unique $\UU$-positive fiber $b_{\dot a}$, with associated Boolean value $v_{\dot a}$. In the generic extension, this old fiber is contained in $a$ if $v_{\dot a}\in G$, and is contained in $\kappa\setminus a$ otherwise. Thus the generated filter decides every subset of $\kappa$. To prove completeness, take a name for a sequence $\seq{a_i:i<\delta}$, where $\delta<\kappa$. Localize and give the name a fixed default value outside the localization. For every $i$, form the unique positive Boolean-value fiber $b_i$ in $V$. Uniqueness makes this construction uniform, so the sequence $\seq{b_i:i<\delta}$ belongs to $V$ without a choice of antichain witnesses. If each evaluated $a_i\in\UU^G$, its associated Boolean value belongs to $G$. Hence \[ b=\bigcap_{i<\delta}b_i\in\UU, \qquad b\sq\bigcap_{i<\delta}a_i. \] Nonprincipality is immediate. Completeness also prevents $\kappa$ from acquiring cardinality below $\kappa$. A short enumeration would express $\kappa$ as a union of fewer than $\kappa$ null singletons. \end{proof} For a normal measure in a $\ZFC$ ground and forcing of size below its measurable cardinal, we also use the usual normal generated lift and the downward L\'evy--Solovay theorem; see \cite{HamkinsGap}. If $D\sq W\sq D[G]$ and the forcing is small relative to a normal $D$-measure $\UU$ on $\kappa$, its restriction to $W$ is the set \begin{equation}\label{eq:measure-restrict} \UU^W=\{a\in\Pow(\kappa)^W:\exists b\in\UU\ (b\sq a)\}. \end{equation} This definition belongs to $W$ when $D\sq W$ and $W\models\ZF$. Restricting the ambient lift gives normality and completeness. The argument requires this restriction construction; measurability need not be downward absolute to an arbitrary inner model. \begin{lemma}[Bounded presentations]\label{lem:presentation} Suppose $N\models\ZF$ and $M=N(Q,F)$, where $Q\sq\kappa^\omega$ and $F:Q\to X\in N$. Each set in $M$ is the value of a bounded, set-sized evaluator whose inputs are the whole sets $Q,F$, finitely many members of $Q$, parameters in $N$, and ordinal codes. The evaluator is absolute between transitive outer models containing the same inputs. For every nonempty $Y\in M$, there are an ordinal $\eta$, a nonempty set $Z\in N$, and a surjection in $M$ \[ \pi:\eta\times Z\times Q^{<\omega}\longrightarrow Y. \] The whole sets $Q,F$ remain fixed parameters of this surjection; they are not replaced by finitely many of their members. \end{lemma} \begin{proof} We use transitive-base constructibility. For a sufficiently large ordinal $\theta$, put \[ B_\theta=\TC\bigl(\{V_\theta^N,Q,F\}\bigr),\qquad J_0(B_\theta)=B_\theta,\quad J_{\xi+1}(B_\theta)=\operatorname{Def}(J_\xi(B_\theta)), \] and take unions at limits. The transitive base makes these levels transitive and increasing. Taking the union of these hierarchies over ground ranks and construction stages gives $N(Q,F)$. Thus each $Y\in M$ is contained in a set-sized level $J_\beta(B_\theta)$. This transitive-base construction includes the members of the adjoined sets, which predicate constructibility may omit; see \cite{Grigorieff,Usuba}. At a fixed level, code each element by a finite expression. A base element is a leaf. An element first produced at a successor stage is specified by a formula over the preceding set-sized level and finitely many parameters from that level. Substitute descriptions of those parameters. Transfinite induction gives a finite expression for each element, with leaves in $B_\theta$ and ordinal stage labels. At a limit stage use an earlier stage. At a successor stage combine the finitely many earlier descriptions. A description of a member of $J_\beta(B_\theta)$ uses stages bounded by $\beta$, allowing a finite increase in $\beta$ if needed. To evaluate an expression, use satisfaction for the indicated set structures $J_\xi(B_\theta)$. Set satisfaction, the definable-subset operation, and the recursion through a bounded list of levels are absolute between transitive outer models with the same base and ordinals. This proves the evaluator's absoluteness without a satisfaction predicate for the proper class $M$ or $N$. We next reduce its leaves. Apart from the whole sets $Q,F$, an element of $\TC(\{Q,F\})$ is obtained by finitely many pairing and projection operations from individual members of $Q$ and ground elements. Indeed, values of $F$ and their hereditary members belong to $N$, and the members occurring in a sequence $q\in Q$ are built from natural numbers and ordinals below $\kappa$. The same statement holds for the ordered pairs coding the graph of $F$. Leaves from $\TC(\{V_\theta^N\})$ are already ground elements. Consequently every expression can be converted to one using the fixed whole parameters $Q,F$, a finite tuple from $Q$, and a finite tuple from one set $V_\rho^N$, where $\rho$ may be chosen uniformly from $\theta,X,\kappa$. Let $Z=(V_\rho^N)^{<\omega}$, increasing $\rho$ so that $Z$ is nonempty and contains all the required fixed ground data. Finite syntactic expressions, finite ordinal labels below the chosen bound, and finite type information form a wellorderable set. Index it by an ordinal $\eta$. Evaluate the codes with all parameters in $Z$ and all finite tuples from $Q$. Keep an output exactly when the code is valid and its value belongs to $Y$. This defines a set-sized partial function in $M$ with range $Y$. Fix one $y_0\in Y$ and send every unused argument to $y_0$, obtaining the total map $\pi$. Using all codes avoids choosing a definition for each $y\in Y$ or a wellordering of the ground parameter set $Z$. \end{proof} \section{The choice symmetric ground from SVC}\label{sec:core} \begin{proposition}[A fixed small presentation with a measurable tail]\label{prop:coretransfer} If $N\models\ZF+\SVC+\CM$, there is a choice inner model $D$ with \[ D\models\ZFC+\CM,\qquad N=D(z) \] for some $z\in N$. There are fixed set forcings $P\in N$ and $T\in D$ and a common extension \[ E=N[H]=D[G] \] such that $N$ is a symmetric submodel of $D[G]$ for a set-sized symmetric system in $D$. \end{proposition} \begin{proof} By \cite[Proposition~5.4]{Usuba}, SVC gives a choice symmetric ground $D$ and a set generator $z$ with $N=D(z)$. Use \cite[Lemma~4.2]{Usuba} to fix a common-cover presentation in which $N$ is a symmetric submodel. An arbitrary pair of forcings witnessing a common extension need not give this symmetric system; see \cite[Note~4.6]{Usuba}. A sufficiently large pair of collapses gives the required presentation. It remains to show that this same $D$ has a proper class of measurables. Put \[ \theta=h^N(\RO^N(P)),\qquad \tau=|T|^D. \] These are fixed ordinals. For every $N$-measurable $\kappa>\max\{\theta,\tau,\omega\}$, Lemma~\ref{lem:ZFmeasure} lifts its measure to $N[H]$. Thus $\kappa$ is measurable in the choice model $D[G]$. Downward L\'evy--Solovay for the $D$-forcing $T$, whose $D$-size is $\tau<\kappa$, puts a measure on $\kappa$ in $D$. The bounds and the ground were fixed independently of $\kappa$, so $D\models\CM$. No absoluteness of the Hartogs calculation between $N$ and $D$ is used. \end{proof} Now assume also $N\models\DC$. Fix an SVC witness $S\in N$, the generator $z$, the protected rank, and the ground symmetric-system data. Choose an uncountable regular $D$-cardinal $\rho$ above the size of $T$ and the rank bounds for this presentation. Then choose a sufficiently high beth fixed point $\lambda$ of $D$ with $\cf^D(\lambda)=\rho$. One obtains such a point as the supremum of a sufficiently high, strictly increasing continuous sequence of beth fixed points of length $\rho$. The forcing $T$ preserves this cofinality. Since $D\subseteq N\subseteq D[G]$, it follows that $\cf^N(\lambda)=\rho>\omega$. Choose $\lambda$ large enough that the transitive set $X=V_\lambda^N$ contains $z$, $S$, and the protected data. Then \[ N=D(X),\qquad N\models\SVC(X). \] For the first equality, $D(X)\subseteq N$ and $z\in X\subseteq D(X)$; for the second, extend each given surjection on $\eta\times S$ by a default value on the rest of $\eta\times X$. Increase the bounds once more if necessary, and choose a measurable $\kappa$ of $D$ above them. The fixed forcing $T$ is small below $\kappa$, so $\kappa$ remains inaccessible in $D[G]$. All rank-bounded data below $\lambda$, including $X$ and the old countable-condition posets introduced below, have size below $\kappa$ there. This construction preserves $N$ and its protected ranks. We use the common choice cover to choose subsequent generics and make the size calculations. \section{The Prikry ambient universe}\label{sec:ambient} For the next four sections fix a symmetric presentation \[ D\sq N\sq D[G],\qquad D\models\ZFC+\CM, \qquad N\models\ZF+\DC+\SVC. \] Write $\mathcal S=(\mathbb A,\mathcal G,\mathcal F)\in D$ for its symmetric system, and take $G$ to be $\mathbb A$-generic over $D$. Choose a transitive rank $X=V_\lambda^N$ containing a generator for $N$ over $D$, an SVC witness, and the structure to be protected. Choose $\lambda$ sufficiently closed, with uncountable cofinality in the full choice cover; one may take a ground beth fixed point of cofinality greater than the size of the fixed small presentation. Then choose a measurable $\kappa$ of $D$ above $\lambda+\omega$ and all presentation bounds. In particular, arrange \begin{equation}\label{eq:setup} N=D(X),\qquad N\models\SVC(X),\qquad |X|^{D[G]}<\kappa, \qquad \mathcal S,\RO(\mathbb A)\in V_\kappa^D. \end{equation} The forcing $\mathbb A$ and all subsequent choice-envelope forcing below $\kappa$ have size less than $\kappa$. We can impose these bounds before choosing $\kappa$. The presentation is fixed, and a small forcing has fewer than $\kappa$ bounded-rank names below a sufficiently large ground inaccessible. The small cover preserves the chosen ground cofinality of $\lambda$, so $\cf^N(\lambda)>\omega$. Let $\UU\in D$ be a normal measure on $\kappa$, and let $\pp_{\UU}$ be its \emph{old} Prikry forcing in $D$. Its ground wellordering belongs to $N$. The old measure base generates the normal lift in every small choice cover under consideration; therefore $\pp_{\UU}$ is dense in the Prikry forcing computed there from that lift. Put $\nu=\omega_1^N$ and let \[ \cc=\{k:k\text{ is an }N\text{-countable partial function } \nu\longrightarrow X\}^{N}, \] ordered by reverse inclusion. We keep the poset computed in $N$ fixed. Every condition belongs to $X$, since its domain is bounded in $\nu<\lambda$ and its countable range has bounded rank below $\lambda$. We may use the dense initial-segment presentation $\bigcup_{\gamma<\nu}{}^\gamma X$ computed in $N$. In the full choice cover $|\cc|<\kappa$, after increasing the bound on the small presentation if necessary. Choose $(c,K)$ generic for the actual product $\pp_{\UU}\times\cc$ over the \emph{full choice cover} $D[G]$, and set \[ W=N[c][K]=N[K][c]. \] The product uses these fixed old posets. Genericity over the full cover gives the displayed genericities over $N$ and the stronger genericity needed in part (3) below. We do not assume that the old collapse remains countably closed after adjoining $c$. In $N$, $\DC$ makes $\cc$ countably closed. Its generic union enumerates $X$ with domain $\nu$. By $\SVC(X)$, $N[K]$ can wellorder every old set, and the same is then true of every set of names and its evaluated range. Thus $N[K]\models\ZFC$. The full cover $D[G][K]$ is a small forcing extension of $D$, so its normal lift of $\UU$ restricts to the normal generated measure in $N[K]$. Product genericity makes $c$ Prikry generic over this choice model. Consequently $W\models\ZFC$. \begin{lemma}\label{lem:ambientfacts} In this setup: \begin{enumerate} \item ${}^{\omega}X\cap W={}^{\omega}X\cap N$; \item every $W$-countable family of elements of $N$ is contained in an $N$-wellorderable set; \item $V_\kappa^{N[c]}=V_\kappa^N$. \end{enumerate} \end{lemma} \begin{proof} For (1), first force with $\cc$. The deciding-sequence argument uses $\DC$ in $N$ and the countable closure of $\cc$. It shows that $N[K]/N$ adds no countable sequence of elements of any fixed old set. In $N[K]$, $X$ has size at most $\nu<\kappa$. The Prikry property for the lifted normal measure implies that the subsequent forcing adds no bounded subset of $\kappa$. Use the enumeration of $X$ to code a countable sequence from $X$ in $W$. The sequence therefore already lies in $N[K]$, and countable closure returns it to $N$. The same argument gives equality of the reals. We use the Prikry property and infinite-subsequence criterion as stated in \cite[Section~3]{Benhamou}. For (2), bound the ranks of the countably many ground elements by an ordinal and place them in one set $Z\in N$. Let $\seq{z_n:n<\omega}\in W$ be the resulting sequence. View it as the value of a $\cc$-name $\dot z\in N[c]$. In $W$, for each $n$ choose $k_n\in K$ which forces \[ \dot z(n)=\check z_n \] over $N[c]$. Such a condition exists by the truth lemma; a fixed localization can be included in all the $k_n$. Since $\cc\sq X$, (1) gives $\seq{k_n:n<\omega}\in N$. Inside $N[c]$, that array, $Z$, and $\dot z$ reconstruct $\seq{z_n}$ by the forcing relation: $z_n$ is the unique $z\in Z$ for which $k_n\forces_\cc\dot z(n)=\check z$. Hence the whole sequence belongs to $N[c]$. Take a $\pp_{\UU}$-name $\dot v\in N$ for it and let \[ B=\{z\in Z:\exists n<\omega\ \exists p\in\pp_{\UU} \ (p\forces\dot v(n)=\check z)\}. \] This is an $N$-set containing every $z_n$. Fix the old wellordering of $\omega\times\pp_{\UU}$. Send each $z\in B$ to its least deciding pair. Distinct values have distinct pairs, so the map induces an $N$-wellordering of $B$ without wellordering $Z$. For (3), use the following generic-intersection fact, valid without Choice: \[ N_0\sq E_0,\quad \mathbb P\in N_0,\quad h\text{ generic over }E_0 \quad\Longrightarrow\quad N_0[h]\cap E_0=N_0, \] where the transitive models satisfy $\ZF$ and have the same ordinals, and the forcing is the same old poset in both models. We give the proof. First, if $h_0,h_1$ are mutually $\mathbb P$-generic over $N_0$, then \[ N_0[h_0]\cap N_0[h_1]=N_0. \] Induct on the rank of a common set $x$. Its members belong to $N_0$ by induction, so $x\sq V_\gamma^{N_0}$ for some ordinal $\gamma$. Choose names $\tau_0,\tau_1\in N_0$ for $x$ and a product condition $(p_0,p_1)$ forcing their equality and that common value to be a subset of $V_\gamma^{N_0}$. For each $y\in V_\gamma^{N_0}$, $p_0$ must decide $y\in\tau_0$: otherwise two extensions giving opposite decisions, paired with one extension of $p_1$ deciding $y\in\tau_1$, contradict the forced equality. Hence \[ x=\{y\in V_\gamma^{N_0}:p_0\forces_{\mathbb P}\check y\in\tau_0\}\in N_0. \] Separation and the forcing theorem suffice; no choice of deciding conditions for all $y$ is needed. Now let $x=\tau^h\in N_0[h]\cap E_0$, where $\tau\in N_0$ is a forcing name. The forcing theorem over $E_0$ gives $p\in h$ with \[ p\forces_{E_0,\mathbb P}\tau=\check x. \] In a further auxiliary extension, choose $h'$ generic over $E_0[h]$ with $p\in h'$. The filters $h,h'$ are mutually generic over $E_0$, hence over $N_0$, and $\tau^{h'}=x$. The preceding intersection argument gives $x\in N_0$. This assertion concerns membership in the original ground, so the auxiliary extension does not change it. The forcing theorem for the further product gives an equivalent formulation that does not infer transitive models from consistency. Apply this fact with $E_0=D[G]$, $N_0=N$, and $\mathbb P=\pp_{\UU}$. The old forcing is dense in normal Prikry forcing for the lifted measure over the choice model $E_0$. Small forcing preserves the inaccessibility of $\kappa$, and the Prikry property gives \[ V_\kappa^{E_0[c]}=V_\kappa^{E_0}. \] The absence of new bounded subsets suffices because $E_0$ satisfies Choice and each old rank below the inaccessible $\kappa$ has size below $\kappa$. Induction on rank proves the displayed equality. If $x\in V_\kappa^{N[c]}$, the inclusion $N[c]\sq E_0[c]$ puts $x$ in $E_0$. Generic intersection then puts $x$ in $N$. The converse inclusion is immediate. This proves (3) using the fixed old posets, without reducing to bounded symmetric names or recomputing the collapse after Prikry forcing. \end{proof} \section{Tagged caps and the labeling forcing}\label{sec:caps} All sequences, carriers, records, and diagram witnesses in this section belong to $N$. The word \emph{old} means ``in $N$,'' even when we work in an auxiliary extension. Changing finitely many initial blocks does not affect any asymptotic requirement. Fix $m_0\ge4$ and, for $m\ge m_0$, put \[ I_m=[2^m,2^{m+1}),\qquad w_m=2^{\lfloor\sqrt m\rfloor},\qquad G_m=2^{\lfloor m^{1/4}\rfloor},\qquad J_m=[2^m+w_m,2^m+2w_m]. \] For $m\omega$. The remaining countable data and the finite rank overhead of coding also stay below $\lambda$. A countable decreasing chain of conditions has its literal union as a lower bound. Every pair of rows and every finite diagram occurs at an earlier stage, so its requirements and witness persist. Finite directedness modulo finite inclusion persists for the same reason. We use $\DC$ only to show that the union of the old countable families is countable. The diagram witnesses are already assigned. \begin{lemma}[Dense tops and insertions]\label{lem:tops} The following extensions are dense in $\rr$. \begin{enumerate} \item A condition can be extended by a designated top containing every previous cap and every current canonical row modulo finite sets. \item A new row of any prescribed color can be inserted at any old cut in the countable current row chain. \item Every old $a\in\mathcal J$ can be included in a cap, and every fixed integer translate of a listed cap can be included in a cap. \end{enumerate} \end{lemma} \begin{proof} \emph{Tops.} Enumerate the caps as $a_i$ and the rows as $f_i$; when a list is finite, omit nonexistent entries in the formulas below. Let $\mathcal D_n$ be the diagram of the first $n$ whole caps and first $n$ canonical rows. Take increasing old density-zero sets $U_n$ containing their assigned diagram exceptions and cap exceptions. Choose increasing thresholds $M_n$, $n\ge1$, such that, for $m\ge M_n$, \[ \sum_{i\omega$ and its whole derived normal measure $U$ belongs to $M$, then \[ \Pow(\kappa)^P =U\cup\{\kappa\setminus a:a\in U\}\sq M. \] Thus $P$ and $M$ have the same $\kappa$-subsets; normality and completeness restrict to $M$, which regards $\kappa$ as measurable. Hence \[ \{\xi<\kappa:P\models\text{``$\xi$ is measurable''}\}\in U. \] The standard relative mouse extraction and least-sound extraction therefore supply an $r$-kukri. Here $i$ fixes the real in $P$. This argument excludes the relative obstruction; it makes no claim about unrelativized mice that omit $r$. For completeness, the fixed-real application keeps the real as one amenable predicate throughout the rudimentary hierarchy, fine codes and comparisons. All hulls used for covering or for the true-core construction contain $\omega$ and $r$. Their collapses fix the real, and all comparison critical points lie above it. Including this fixed countable base leaves the covering cardinal bounds and thick-hull argument unchanged. The failure configuration is consequently a mouse over that same real. This is the ordinary real-bottom instance of the classical theorems, not a comparison of varying arbitrary oracles. Lemma~\ref{lem:kukri-noncreation} keeps the obstruction absent in the required set-forcing extensions. The true-core theorem gives literal equality of the ground and extension cores. \end{proof} \begin{lemma}[Measurable capture by singularization]\label{lem:core-capture} In the negative alternative of Lemma~\ref{lem:fixed-core}, every measurable cardinal of the choice background is measurable in its fixed core. \end{lemma} \begin{proof} Let $\kappa$ be measurable in the choice background $C$, and choose a normal measure there. Ordinary Prikry forcing preserves cardinals and makes $\cf(\kappa)=\omega$ \cite{Benhamou}. Before forcing, $\kappa$ was regular in the inner model $K=K(r)^C$. In the Prikry extension $C[h]$, generic invariance gives $K(r)^{C[h]}=K$. Thus $\kappa$ is an ambient singular cardinal regular in this same core. Apply the full-covering consequence in Lemma~\ref{lem:fixed-core}. Its witnessing measure belongs to the unchanged ground class $K$. This is an internal forcing proof in $\ZFC$ of an assertion about the unchanged core. It assumes no actual generic filter in the original ambient universe. It uses neither a trace of the original measure on $K$ nor an extra weak-amenability assertion. This auxiliary Prikry argument adds no stage to the main Prikry--labeling construction. \end{proof} \begin{lemma}[Measurables in one fixed relative core]\label{lem:fixed-measurables} In a $\ZF$ universe with unbounded measurables, put $B=\HOD(r)$. If $B$ has no $r$-kukri, then $K(r)^B\models\CM$. \end{lemma} \begin{proof} Fix one ambient measurable $\kappa$ and one ambient $\kappa$-complete nonprincipal ultrafilter $\mu$. Set \[ C=\HOD(r,\mu),\qquad u=\mu\cap\Pow(\kappa)^C. \] The parameterized Vop\v{e}nka theorem applies in $\ZF$: take $Y=r$, $X=V_\theta\ni\mu$ and $x=\mu$ in \cite[Lemma~3.6]{GoldbergChoiceless}. Thus $C$ is a set-generic extension of $B$ and satisfies $\ZFC$. The whole $u$ belongs to $C$, since it is ordinal definable from $r,\mu,\kappa$ and every member is already in $C$. This does not require $\mu\in C$. Every $C$-subset of $\kappa$ is decided by $u$. Every whole $C$-sequence of fewer than $\kappa$ members of $u$ is also an ambient sequence, so its intersection belongs to $u$ by ambient completeness. Nonprincipality also transfers. Consequently $C$ regards $\kappa$ as measurable. The negative alternative persists by Lemma~\ref{lem:kukri-noncreation}. Apply Lemma~\ref{lem:core-capture} inside $C$ and use $K(r)^C=K(r)^B$. This makes the original ambient $\kappa$ measurable in the one fixed core. Repeat the existential argument separately for each ambient measurable. No simultaneous choice of measures, ambient normality or ambient Dependent Choice is needed. \end{proof} \subsection{The positive choice model and recoding} \begin{lemma}[The top-iteration choice model]\label{lem:kukri-class} If a choice background contains an $r$-kukri, its canonical top iteration gives a uniformly $r$-definable inner model $S_r$ containing $r$ and satisfying $\ZFC+\CM$. \end{lemma} \begin{proof} Use the least sound mouse and its standard top-only iteration $(P_i,\kappa_i)$, with the real predicate fixed. The construction in \cite[Section~2, Facts~(ii)--(v)]{WelchHartig} gives the inner model \[ S_r=\bigcup_{i\in\Ord}H_{\kappa_i}^{P_i},\qquad |P_i|=H_{(\kappa_i^+)^{S_r}}^{S_r}. \] Its critical points are unbounded, and its displayed lower cuts are coherent elementary cuts. The theorem applies with the fixed amenable real predicate included in every hull and fixed by every map; see the fine-structure convention in \cite[Chapter~1]{ZemanInnerModels}. The whole $H$-cut identification supplies all final subsets and short graphs below $\kappa_i$. Top normality makes $\kappa_i$ inaccessible in $S_r$, so the lower cut is $V_{\kappa_i}^{S_r}$. Given any bound below $\kappa_i$, choose a lower measurable $\delta$ above it in $P_i$. Its whole normal measure and all $S_r$-subsets of $\delta$, regressive graphs and short families of such subsets have rank below $\kappa_i$. They occur in the same unchanged cut. The measure therefore remains full and normal in $S_r$. These lower witnesses are unbounded, giving $\CM$. No measurability of the moving top itself is used. The published construction supplies $\ZFC$ and canonical set-length iterates. Its defining recursion takes place inside the choice background, so it defines one class without class choice. The bottom real is retained throughout. \end{proof} \begin{lemma}[Recoding covariance]\label{lem:recoding} Mutually recursive reals $r,s$ in the same choice background give the same pure output in each of the two alternatives above. \end{lemma} \begin{proof} We first check the pure carriers in the declared predicate convention. The first $J$-block is $\mathrm{HF}$ for either real. The second is the appropriate rudimentary closure of $\mathrm{HF}\cup\{\mathrm{HF}\}$. In $J_2[s]$, both $\omega$ and the whole set $\mathrm{HF}$ are present, as is the whole trace $s$. If program $e$ computes $r$ from $s$, then \[ r=\{n\in\omega:\exists c\in\mathrm{HF}\; c\text{ is an accepting $s$-oracle computation of $e(n)$}\}. \] This is bounded Separation with the old set $\mathrm{HF}$ as the computation bound. Thus $r\in J_2[s]$. Since intersection with this old $r$ is rudimentary, $J_2[s]$ is closed under the $r$-predicate operations. Reverse the programs and use minimality of rudimentary closure to obtain the same $J_2$. Induction gives the same subsequent $J$-carriers when the measure predicates are held fixed. The finite auxiliary $S$-stages need not agree. The inverse formula translations preserve $\Sigma_1$ truth with each fixed ordinal parameter tuple. Above $\mathrm{HF}$, computation witnesses are bounded by the old set $\mathrm{HF}$; its uniform $\Sigma_1$ name can be witnessed by the whole pure finite-stage construction tower, whose graph is a bounded subset of $\mathrm{HF}$ at $J_2$. At an $\mathrm{HF}$ reduct, bounded quantifier domains are finite, so one finite evaluation tree collects the needed finite computation witnesses. This supplies the same translations without assuming that $\omega$ is a set in that reduct. Consequently missing-subset projecta and good parameter classes agree. Each canonical Skolem graph is a uniquely defined partial $\Sigma_1$ function in the other language. The two Skolem hulls are closed under one another's such functions and hence are identical. Very-good parameter classes agree; the unchanged ordinal ordering gives the same least standard parameters. Repeat this argument on the theory-code reducts. Their formula indices translate recursively while tuple coordinates stay fixed. Whole bounded theory witnesses translate by bounded image or preimage under the old recursive translation graph. At an $\mathrm{HF}$ reduct the finite witnesses are hereditarily finite in both presentations. Thus the code recovery and pure sound-core collapses agree. These are the standard fine-code operations of \cite[Chapter~1]{ZemanInnerModels}, in each chosen category separately. The transport is invertible on the eligible mice and commutes with their comparisons, measure quotients and direct limits. It therefore preserves the least kukri and its top-iteration cuts. In the negative alternative, inverse transport preserves the class of relative candidate mice, their comparison relation and the ambient thick-class tests in this same background. Apply the standard true-core definition and uniqueness theorem to these corresponding data. The pure true cores are consequently equal; no literal equality of preliminary auxiliary constructions is required. \end{proof} \subsection{Canonical refinement inside a choice model} We now obtain the own-HOD presentation directly from a choice model with unbounded measurables. This construction uses ordinary normal measures and their iterated ultrapowers. It applies inside either choice model supplied above. For a set selection $F$ of measures, $L[r,F]$ denotes construction with its domain and filter-incidence predicates, rather than with the whole vector and its transitive closure as an initial seed. \begin{lemma}[Bounded uniqueness and exhaustion]\label{lem:bounded-refinement} Work in a choice universe $B$. Let $d$ be a set of measurable cardinals above $\omega$ such that $d\cap\kappa$ is bounded below $\kappa$ for every $\kappa\in d$. Let $F$ and $G$ be whole selections of full normal $B$-measures on $d$, and let $r$ be a real. Then \[ L[r,F]=L[r,G], \] and the two predicates have the same restricted kernels in this model. The model's only normal measures are these listed restricted measures. \end{lemma} \begin{proof} The restricted kernel of a bounded selection is a whole set in its predicate model: form the model's bounded powerset and tuple carrier, take one later construction-stage trace of the incidence and domain predicates on that carrier, and regroup the trace by Replacement. Each restricted measure is full and normal there, since all its internal test sequences and functions are background sets. For uniqueness put $T=\ran(F)\cup\ran(G)$. If $U\in T$ is on $\kappa$, then \[ \kappa\in j_U(d)\quad\Longleftrightarrow\quad d\cap\kappa\in U, \] which is false by spacing. Thus $j_U(T)$ has no measure at the old $\kappa$. The whole earlier family has rank below $\kappa$ and is fixed. Consequently $T$ is a closed set of measures in the sense of \cite[Lemma~19.35]{Jech}, and every member has relative $T$-rank zero. This permits several different measures at one critical point. Apply that lemma to two copies of $(B,T)$, obtaining ordinary iteration maps $i:B\to M$ and $j:B\to N$, with, say, $i(T)$ an initial segment of $j(T)$. Write $\ell(e)=\sup\{\delta+1:\delta\in e\}$. The initial-segment test compares \emph{all} cross-pairs of measures at a common critical point and relative rank on all common subsets \cite[(19.20)]{Jech}. Both $i(F)$ and $i(G)$ have domain $i(d)$, including any new positions in this image domain. The restriction $j(F)\restr\ell(i(d))$ has the same domain. Thus simultaneous induction through the three relative hierarchies gives \[ L[r,i(F)]=L[r,i(G)]=L[r,j(F)\restr\ell(i(d))]. \] At each common level every predicate argument belongs to both terminal models, so the incidence answers agree. The first two predicates also agree on every query in their common construction. These are first-order assertions inside $M$ about its two set parameters $i(F),i(G)$. Pulling them back through the single map $i$ proves both assertions of uniqueness. All critical points fix $r$. For clarity, this comparison terminates at a set stage. Choose $\gamma$ above the original domain and put $\mu=2^{|\gamma|}$ and $\Theta=\mu^+$ in $B$. Finite-support representations bound each current image of $\gamma$ and $\Pow(\gamma)$, at stage $\nu<\Theta$, in size by $\mu\cdot|\nu|^{<\omega}<\Theta$. All choices can therefore be made in one wellordered set carrier. If comparison continued through $\Theta$, Fodor's lemma at limit stages, followed by stationary thinning, would make the earlier representatives of the disagreement ordinal constant on both sides. In the two-measure case it also makes the representatives of a common distinguishing subset constant. Slot erasure makes comparison critical points strictly increase. At a one-sided step, the padded side consequently fixes the old seed while the other moves it. At a two-sided step, normality puts the old seed into exactly one image of the distinguishing subset, and later maps preserve that disagreement. Both conclusions contradict the equal later representatives. This is the set version of the comparison argument in \cite[Lemma~19.35]{Jech}. For exhaustion, suppose a predicate model has an extra normal measure. Choose its first critical prefix with this property, allowing the whole final prefix. Replace that selection by its whole internal kernel $E$ and write $M_0=L[r,E]$. Every proper critical prefix of $E$ has no extra normal measure in its own predicate model. These prefix constructions are literal inside $M_0$, so $M_0$ satisfies this assertion. Choose there the least $\kappa$ carrying an extra normal measure, then an extra $W$ of least Mitchell rank, breaking ties by the canonical $L[r,E]$ order. This choice is definable from $r,E$ alone; the Mitchell order is well founded \cite[Lemma~19.32]{Jech}. Let $j_W:M_0\to N_0=\operatorname{Ult}(M_0,W)$ and $E_1=j_W(E)$. Compare $(M_0,E)$ and $(N_0,E_1)$ by the same closed-family lemma, with terminal maps \[ i:M_0\to P=L[r,I],\qquad k:N_0\to Q=L[r,J]. \] If $I$ were a proper critical prefix of $J$, literal hierarchy induction would give $P=L[r,J\restr\ell(\dom I)]\sq Q$. Its restricted kernel is exactly $I$. The transferred minimal-prefix assertion in $Q$ forbids an extra normal measure in this very model $P$, whereas $i(W)$ is such a measure. No fullness over $Q$ is being inferred here. The reverse orientation is excluded in the same way. Thus $P=Q$ and $I=J$ as whole restricted kernels. Put $l=k\circ j_W$. The maps $i,l$ have the same target and the same images of $r,E$. The canonical definitions give \[ i(\kappa)=l(\kappa),\qquad i(W)=l(W). \] The normal ultrapower $N_0$ has the same subsets of $\kappa$ as $M_0$. If $E_1$ has a measure $T$ at the old $\kappa$, then $T\in N_0\sq M_0$. Codes as $\kappa$-subsets for short families and regressive graphs show that $T$ is a full normal $M_0$-measure. It is a Mitchell predecessor of $W$, so minimality of $W$'s rank forces $T$ to be the sole listed measure at $\kappa$. The two initial sequences agree below $\kappa$. If they agree at $\kappa$ as well, all comparison critical points exceed $\kappa$; then $i(\kappa)=\kappa\beta+\omega$ with $\cf^V(\lambda)>\omega$, and let $B=V_\lambda^V$. DC supplies such a limit ordinal. For example, start sufficiently high and add $\omega_1^V$. Collapse $B$ to be countable, and let $r$ code membership and equality of entries in its generic enumeration. By Lemma~\ref{lem:ZFmeasure}, this fixed collapse preserves a proper-class tail of measurables. Apply Lemma~\ref{lem:earlier-core} in the collapse extension and put $C=C_r$. Inside $C$, first quotient the coded enumeration by its equality relation and then take its well-founded extensional collapse. This recovers the same transitive set $B$. Define \[ N=\HOD^{C}_{B\cup\{B\}}, \] allowing individual elements of $B$ as parameters as well as the whole set $B$. This relative hereditary-definability construction satisfies $\ZF$ and contains $B$ and all its elements. Finite permutations of the $\omega$-domain witness weak homogeneity of the collapse by moving the finite domain of one condition away from that of another. They replace $r$ by exactly the recodings covered by Lemma~\ref{lem:earlier-core}(2) and fix the actual ground set $B$ and its members. Thus the group preserves every fixed ordinal-and-$B$ definition over $C$. The usual hereditary rank induction gives $N\sq V$. Consequently \[ V_\lambda^N=B=V_\lambda^V. \] In particular, both the rank $V_\beta$ and all its subsets have been retained. For every nonempty $Y\in N$, the relative-HOD definition gives a surjection in $N$ from $\eta\times B^{<\omega}$ onto $Y$, for some ordinal $\eta$. The surjection enumerates all bounded definition codes and finite parameter lists, without choosing a definition for each element of $Y$. Finite lists from the limit rank $B$ can be coded into $B$, so $N\models\SVC(B)$. For DC, let $R\in N$ be serial on $Y$, fix $y_0\in Y$, and take $f:\eta\times B\twoheadrightarrow Y$ in $N$. At a current $y$ put \[ \xi(y)=\min\{\xi<\eta:\exists b\in B\ (y\,R\,f(\xi,b))\}. \] Use DC in $V$ to choose successive $b_n$ at these least ordinal coordinates. The array $s=\seq{b_n:n<\omega}$ belongs to $B$ because $\cf^V(\lambda)>\omega$ and $\lambda$ is a limit. Hence it belongs to $N$. Within $N$, recursion from $s$, $y_0$, and the least-coordinate rule reconstructs the entire chain. Thus $N\models\DC$. Finally, $D=\HOD^C\sq N\sq C=D[g]$. Since the forcing is fixed, downward L\'evy--Solovay gives a measurable tail in $D$ from $C\models\CM$. For every sufficiently high ground measure $U$, its generated lift in $C$ restricts to the set \[ \{a\in\Pow(\delta)^N:\exists b\in U\ (b\sq a)\} \] in $N$. This is the complete nonprincipal ultrafilter required for $\CM^N$. We fix the ground $D$ and cover $C$ before taking this tail. If desired, the intermediate symmetric-model theorem and $\SVC^N$ make $D$ a symmetric ground of $N$. \end{proof} \begin{proof}[Proof of Theorem~\ref{thm:rank-transfer}] Apply Proposition~\ref{prop:remove-svc} above $\alpha+1$ to obtain $N\sq V$. Then apply the local Theorem~\ref{thm:transfer-intro} to $N$, protecting the same rank and its power set. The resulting $M$ has the displayed rank and power-set equalities with $V$, together with the stated sequence-seed presentation. Choose all required generics over the original collapse extension. The construction then takes place in a set-generic extension of $V$. The inclusion asserted is $N\sq M$; the argument does not assert $V\sq M$. \end{proof} \section{Removing Foundation by atomization and fibers}\label{sec:foundation} We now reduce the Foundation-free starting theory to the preceding case. The atomization and fiber purification follow the earlier argument of \cite[23 September, 06:07 UTC]{ResearchArchive}. We first prove the version of the local forcing theorem needed here. In this section, $\mathsf{ZFA}$ has Foundation above a fixed set $\mathcal A$ of atoms, and $\operatorname{Ker}$ denotes the pure kernel. \subsection{The local construction with atoms} \begin{lemma}[The choice-envelope version]\label{lem:atom-local} Let $N\sq E$ be $\mathsf{ZFA}$ models with the same ordinals and the same set $\mathcal A$ of atoms. Suppose: \begin{enumerate} \item $N\models\DC+\SVC(X)$, where $X=V_\lambda^N(\mathcal A)$ is a sufficiently high limit rank, $\cf^N(\lambda)>\omega$, and $\mathcal A\sq X$; \item $E$ satisfies Choice, $\mathcal A$ is countable in $E$, and $\operatorname{Ker}(E)=D[g]$ for a pure $D\sq N$ satisfying $\ZFC+\CM$ and fixed set forcing; \item a measurable $\kappa>\lambda+\omega$ of $D$ is chosen above the size of this fixed forcing and the sizes in $E$ of $X$, the old collapse, and the cap and comparison posets. \end{enumerate} Then the local Prikry--labeling construction produces $N\sq U$ with \[ U\models\mathsf{ZFA}+\DC+\CM+\SVC+\KW,\qquad \Pow(X)^U=\Pow(X)^N,\qquad V_\lambda^U(\mathcal A)=X. \] \end{lemma} \begin{proof} This version requires only the pure $D$ and the choice envelope $E$. Use the old pure Prikry poset from $D$ with its old wellordering. The old normal measure base generates the normal lift in $E$ and its small choice extensions. Compute the countably closed collapse in $N$ and choose the product generic over $E$, as in Section~\ref{sec:ambient}. Internal countable closure and condition coding use $\cf^N(\lambda)>\omega$. No requirement is imposed on $\cf^E(\lambda)$. The small-forcing assertions with atoms reduce to their pure counterparts. Fix an enumeration of the atoms in $E$. Recursively code each atom by its tagged index and each set by the tagged set of its members' codes. Every resulting code is pure and belongs to $\operatorname{Ker}(E)$. Choice in $E$ codes any set forcing by an ordinal condition set and a pure order. Translate names using the same atom indices. Decoding a name for a pure value uses no atoms. The pure kernel after forcing is therefore the corresponding set-forcing extension of the old pure kernel. We use this coding only in the envelope and do not adjoin its atom enumeration to $N$ or $U$. The collapse-first proof of Lemma~\ref{lem:ambientfacts}(1)--(2) therefore applies to atomful $X$ and arbitrary ground values. SVC makes $N[K]$ a choice model with atoms. Since Prikry forcing adds no bounded subsets, we obtain the same preservation of countable sequences from $X$ and wellorderable covers of ground families. For part (3), we need preservation of atom-ranks. Since $|\mathcal A|^E<\kappa$ and $\kappa$ remains inaccessible in the choice envelope, every old atom-rank below $\kappa$ has size below $\kappa$. Prikry forcing preserves these ranks because it adds no bounded subsets. A new set of least rank would be a subset of a small old rank; its pullback by an old wellordering would be a new bounded subset of $\kappa$. The atoms are unchanged. The generic-intersection proof proceeds by rank over the common atom set, starting with the atoms, which already belong to $N$. Thus \[ V_\kappa^{N[c]}(\mathcal A)=V_\kappa^N(\mathcal A). \] Use transitive-base constructibility with atoms retained at every successor stage, for example \[ J_{\xi+1}=\mathcal A\cup\operatorname{Def} (J_\xi;\in,\mathsf{Atom}), \] so that taking definable subsets does not discard the atoms. Lemma~\ref{lem:presentation} still gives finite expressions. Atoms are ground leaves, and the atom predicate has the same interpretation in the compared universes. The presentation lemma does not use an equality $N=D(X)$. All cap and paired constructions concern integer carriers and their literal colors in $X$. A color may be an atom. Since the constructions never recover a color from its members, the proofs in Sections~\ref{sec:caps}--\ref{sec:paired} are unchanged. The common atom predicate also gives bounded-evaluator absoluteness. Labeling elimination and the atom-rank equality just proved yield $\Pow(X)$ preservation. The old condition-array argument, the real-coded masks, and the wellorderable-tree argument prove DC as before. Bounded presentations and $F:Q\twoheadrightarrow X$ give SVC and KW for every nonempty set of $U$, including sets containing atoms. Finally the full choice envelope after these set forcings has pure kernel a set-forcing extension of $D$, by the coding paragraph above. A sufficiently high tail of ground measures has generated lifts there, and the old-base definition used in Proposition~\ref{prop:seed} restricts those lifts to measures belonging to $U$. This proves $\CM^U$. The atom lemma does not include the pure sequence-seed and symmetric-ground conclusions of Proposition~\ref{prop:seed}. The predecessor-set quotient does not distinguish distinct atoms, and a pure $D(A')$ cannot contain them. Neither conclusion is needed below. \end{proof} \subsection{Preparation of the protected atom structure} Start with $V\models T_-$ and a full second-order counterexample $\mathcal M$ to a fixed sentence. Take its relational multisorted presentation, with a first-order sort $S_0$ and, for each arity $k$ in the sentence, a sort representing all $V$-subsets of $S_0^k$ with the incidence relation. The two-sorted presentation is the unary or tuple-coded case. Replace the combined domain by a set $\mathcal A$ of formal atoms, with distinct tags for the sorts. Form the full interpreted cumulative hierarchy $\mathcal H(\mathcal A)$ using the original universe's power sets. Treat its atoms as opaque labels whose original members do not become members of the atoms. Non-well-founded membership in $V$ therefore introduces no cycles in the interpreted hierarchy. The hierarchy satisfies $\mathsf{ZFA}$. It also satisfies DC, since an ambient chain through a set of its coded objects has bounded atom-rank and belongs to the hierarchy. Its pure kernel has the original ordinals and their full power sets. It therefore retains the original measures and the ordinal-indexed families testing their completeness. Hence \[ \mathcal H(\mathcal A)\models\mathsf{ZFA}+\DC+\CM. \] The atomized structure remains full because inverse images under the atom-label bijection identify its subsets and finite-arity relations with all the original ones. Choose a limit $\lambda$ of uncountable cofinality in this hierarchy, high enough to contain the structure and the full power sorts, and set \[ B=V_\lambda^{\mathcal H(\mathcal A)}(\mathcal A). \] Collapse $B$ to be countable. Its real code $r$ records membership, equality of repeated enumeration entries, and which entries are atoms. The small-forcing proof of Lemma~\ref{lem:ZFmeasure} works with fixed atoms, so a measurable tail remains. Apply the earlier core-model Lemma~\ref{lem:earlier-core} in the pure kernel of this collapse extension, obtaining $C_r=D[g]$. Construct the choice companion $E$ as follows. Let $I$ be the least enumeration indices of the distinct atoms, as determined by $r$. Inside $C_r$, form the hierarchy over the formal atom set indexed by $I$. Use the collapse enumeration to relabel those formal atoms by the actual atoms. The resulting $E$ satisfies Choice, has pure kernel $C_r$, and contains the literal $B$. To prove the last assertion, quotient the code by its equality predicate and take its well-founded collapse with the specified atom labels. These labels distinguish the atoms from one another and from the empty set. Uniqueness of the collapse gives the same $B$. The finite permutation group used in Proposition~\ref{prop:remove-svc} preserves this companion. The pure $C_r$ is unchanged, and the induced bijection between the two atom-index sets belongs to the same pure model. Transporting the hierarchy along this bijection gives the identical actual companion. Therefore \[ N=\HOD^E_{B\cup\{B\}}, \] with the atom predicate retained, descends to $\mathcal H(\mathcal A)$ by the same hereditary homogeneity argument. It contains $B$ and has $V_\lambda^N(\mathcal A)=B$. Relative-HOD presentations give $\SVC(B)$, and the least-ordinal-coordinate DC proof in Proposition~\ref{prop:remove-svc} applies using the countable closure of $B$ in $\mathcal H(\mathcal A)$. The pure $D=\HOD^{C_r}$ is contained in $N$, because definitions over the definable pure kernel of $E$ are available over $E$. Ground measure lifts restrict to $N$, giving $\CM^N$. We have a pure ground inside $N$ and a choice envelope above it. This does not assert a choice ground with atoms inside $N$, and it does not apply the pure SVC symmetric-ground theorem to an atom model. Lemma~\ref{lem:atom-local} now applies with $X=B$. In particular, $\cf^N(\lambda)>\omega$ because $N\sq\mathcal H(\mathcal A)$. The envelope may see $B$ and $\lambda$ as countable, which the lemma permits. The old condition sets have codes in $B$ and are small in $E$. Once these set-sized bounds are fixed, choose a sufficiently high $D$-measurable $\kappa$. The lemma yields \[ U\models\mathsf{ZFA}+\DC+\CM+\SVC+\KW \] with the protected power sets unchanged. The original multisorted counterexample is consequently still full in $U$. \subsection{Fiber purification and the final theorem} \begin{lemma}[Fiber purification]\label{lem:fiber} If $U\models\mathsf{ZFA}+\DC+\CM+\SVC+\KW$, then its pure kernel $P$ satisfies $T_0+\SVC+\KW$. Every full second-order structure in $U$ has a full isomorphic copy in $P$. \end{lemma} \begin{proof} For the nonempty combined domain $S$ of a relational presentation, take a surjection $f:\kappa^\omega\twoheadrightarrow S$ in $U$ and put \[ j(s)=f^{-1}\{s\}. \] The nonempty disjoint fibers make $j$ injective. Each fiber is a set of ordinal sequences and is therefore pure. Thus the whole range $j[S]$, its sort predicates, and all transported finite-arity relations are pure sets in $P$. The graph of $j$ may contain atoms and need not belong to $P$. Empty domains can be treated directly. To check fullness at each relevant arity, let $Y\in P$ with $Y\sq j[S_0]^k$. Its pullback under $j^k$ is a $U$-subset of $S_0^k$, represented by an element of the full power sort in $U$. The image of that element represents exactly $Y$. Conversely, each represented subset in the transported structure is pure and belongs to $P$. In the application, preservation of the protected power sets identifies these $U$-relations with the relations of the original counterexample. The copied structure therefore has the same full second-order truth. The pure kernel satisfies $\ZF$, including Foundation. A DC chain through a pure set is itself pure. Measures on ordinals and all families testing their completeness are pure as well, so $\CM$ descends. The models have the same $\kappa^\omega$; a surjection from it onto a pure set has pure graph. Hence KW descends. Finally, fix one SVC witness $C$ in $U$ and fiber-code it as above to obtain a pure copy $C^\flat$. For any nonempty pure $Y$, compose an SVC surjection $\eta\times C\twoheadrightarrow Y$ with the inverse of this fiber bijection. The resulting map $\eta\times C^\flat\twoheadrightarrow Y$ has pure graph and belongs to $P$. The same $C^\flat$ works for every $Y$, proving SVC in $P$. \end{proof} \begin{proof}[Proof of Theorem~\ref{thm:main}] Given a full second-order counterexample in a model of $T_-$, atomize it, carry out the core-model preparation, and apply the local atom theorem as above. Lemma~\ref{lem:fiber} gives a pure model of $T_0+\SVC+\KW$ containing a full counterexample to the same sentence. The countermodel contrapositive proves structural conservativity. The reverse implication of provability follows because the target theory extends $T_-$. All constructions are interpretations and set-forcing constructions over the starting model. No external transitive-model hypothesis is used. \end{proof} \section{External HOD and homogeneous descent}\label{sec:external-basics} \begin{lemma}\label{lem:HDC} If $U\models\ZFC$, then $\Hseq^U\models\ZF+\DC$. It contains every ordinal $\omega$-sequence of $U$ and is closed under $U$-countable sequences of its elements. \end{lemma} \begin{proof} The usual hereditary-definability proof of $\ZF$ applies to the definable class of allowed parameters. For example, the internal power set of $x\in\Hseq^U$ is \[ \{y\sq x:y\in\Hseq^U\}, \] which is definable from a definition of $x$ and has only hereditary members of the class. The same argument gives Separation and Replacement. Let $\seq{x_n:n<\omega}\in U$, with each $x_n\in\Hseq^U$. In $U$, choose a definition of $x_n$ from an ordinal sequence and ordinal parameters. Evaluate each definition at a rank level where its formula has the required unique value. Interleave the sequence parameters, the rank levels, the ordinal parameters, and the formula codes. This gives one $q\in(\Ord^\omega)^U$ from which the entire sequence $\seq{x_n}$ is definable in $U$. Its hereditary members already belong to $\Hseq^U$, so the sequence belongs to $\Hseq^U$. Every $q\in(\Ord^\omega)^U$ is itself hereditarily definable from $q$. To prove DC, choose a dependent-choice chain in $U$ through a serial relation belonging to $\Hseq^U$ and apply the countable closure just proved. \end{proof} \begin{lemma}[Homogeneous descent]\label{lem:homdesc} Let $M\models\ZF$, and suppose $U=M[G]$ is a weakly homogeneous set-forcing extension with \[ (\Ord^\omega)^U=(\Ord^\omega)^M. \] Then $\Hseq^U\sq M$. No ordinal-definability assumption on the forcing is needed. \end{lemma} \begin{proof} Induct on hereditary rank. Suppose $x\in\Hseq^U$ and every member of $x$ is in $M$. Choose $\beta$ with $x\sq V_\beta^M$. A definition of $x$ in $U$ uses an allowed parameter $q$ belonging to $M$ and ordinal parameters. By weak homogeneity, the largest condition decides the corresponding uniqueness assertion and, for each $y\in V_\beta^M$, whether $y$ belongs to its unique value. The forcing relation therefore defines $x$ as a subset of $V_\beta^M$ inside $M$. \end{proof} \begin{proposition}\label{prop:one-three} For every $\sigma$, $\Con(E_1(\sigma))$ implies $\Con(E_3(\sigma))$. \end{proposition} \begin{proof} Let $U\models E_1(\sigma)$, put $H=\Hseq^U$, and choose $\kappa$ with $V_\kappa^H\models\sigma$. Choose $\lambda>\kappa+\omega$ of uncountable cofinality in $U$, and set $X=V_\lambda^H$. This $X$ is ordinal-definable in $U$, belongs to $H$, and is closed under $U$-countable sequences of its elements by Lemma~\ref{lem:HDC}. Collapse $X$ to be countable over $U$, coding both equality and membership and quotienting repetitions before collapse. Apply Lemma~\ref{lem:earlier-core}, and again set $W=\HOD_{X\cup\{X\}}^{C_r}$. The collapse-homogeneity argument gives $W\sq U$ and controls the parameters in each descended definition. The collapse forcing is definable from the OD set $X$, so these definitions use $X$, finitely many elements of $X$, and ordinals. The set $X$ is OD in $U$, and each of those finitely many elements is hereditarily definable from an ordinal $\omega$-sequence. Combining their parameters gives $W\sq H$. Since $X\in W$, we have $V_\lambda^W=X$. The presentation $\SVC(X)$ and the ambient countable closure of $X$ give $\DC$ in $W$. The same generated-measure argument gives $\CM$. Therefore $W\models E_3(\sigma)$. \end{proof} \section{Sparse evaluated Cohen caps}\label{sec:spectrum} We work over a choice model $B$ and code a \emph{family of coherent rows}. The code records which bit positions belong to each row, rather than only their union. We use the convention $\Add(\gamma,1)=2^{<\gamma}$, ordered by extension; the dense partial-function presentation gives the same forcing. Throughout this section, the superscript specifies the model in which each poset is computed. \begin{theorem}[Fixed-base spectrum]\label{thm:spectrum} Let $B\models\ZFC$ have a proper class of inaccessible cardinals, and let $\varnothing\ne F\sq2^\tau$ belong to $B$, where $\tau$ is infinite. There are a schedule of inaccessible coding cardinals, uniformly defined forcings $Q_e$ for $e\in2^\tau$, and a cap cardinal $\rho$, all definable from $B$ and ordinal parameters independently of $F$, such that the weakly homogeneous forcing $P_F$ defined below has the following spectrum in $B[G]$: \begin{equation}\label{eq:spectrum} e\in F\quad\Longleftrightarrow\quad \begin{gathered} \text{there is a $B$-generic }h_e\sq Q_e,\ \text{and an }\Add(\rho,1)^{B[h_e]}\text{-generic over }B[h_e]. \end{gathered} \end{equation} The first coding cardinal can be placed above any prescribed bound, and the resulting forcing is correspondingly distributive. \end{theorem} \subsection{The schedule and the actual forcing} Order the physical sites $s=(\xi,i)$, for $\xi<\tau$ and $i<2$, lexicographically with $\xi$ first. Distinct rows have independent copies at a shared physical site. Choose inaccessible cardinals $\gamma_s$ recursively, with the first above $2^{|\tau|}$ and the prescribed protection bound, and with \begin{equation}\label{eq:sparse} |\RO(S_{|V_\eta^B|$ preserves $V_\eta^B$ by rank induction. The canonical lower-row automorphisms lift through the name for the recomputed Cohen forcing, which is forced homogeneous. Coordinatewise automorphisms then witness weak homogeneity of the full product. \subsection{Localization to physical sites} \begin{lemma}\label{lem:site} Suppose a $B$-generic $h_e\sq Q_e$ belongs to the $P_F$-extension. Then \[ B[h_e]\sq B[G_s:s\text{ is selected by }e]. \] \end{lemma} \begin{proof} The whole lower generic $h_e$ can be coded by a subset of a ground ordinal below $\rho$. The cap quotient adds no such subsets, so $h_e$ is in the lower extension. Let $k_s\sq\gamma_s$ be its component at an $e$-selected site. If there is a site after $s$, its first cardinal exceeds the Boolean size of the prefix through $s$. The ground full tail is closed up to that cardinal. Easton's lemma over the smaller prefix therefore makes it add no subsets of $\gamma_s$; at a final site there is no tail. Thus the required tail distributivity follows from \eqref{eq:sparse}, and \[ k_s\in B[G_s][G_{\chi$, the cutoff is fixed by the normal ultrapower embedding. The iteration and its image agree below $\kappa$ and have the same stage-$\kappa$ Cohen preparation and closed upper tail used in the cited lift. Removing the bounded initial stages introduces no further lifting requirement. Consequently a class of measurables survives. These conclusions give eventual GCH and $\CM$; they impose no GCH requirement on the protected rank. The coding density argument applies above each prescribed bound. Every ordinal set appearing in an initial extension can be written on a fresh block by choosing the appropriate coding factors. Subsequent tails preserve that block's truth pattern. It follows that every ordinal set of $D$ has arbitrarily high $\diamondsuit^*$ codes. We next verify that these codes make $D$ secure. First, if $W[g]/W$ is set forcing and $\lambda$ is regular above its size, then $\diamondsuit^*_\lambda$ has the same truth value in the two models, by \cite[Lemma~19]{CFH}. The locations of sufficiently high codes also agree. Indeed, if the forcing has size $\nu$, cardinal preservation and the bound of $(2^\kappa)^W$ on names for subsets of $\kappa$ show that the cardinal-valued continuum functions agree for cardinals $\kappa>\nu$. Let $b_\xi$ and $b'_\xi$ be the two beth sequences. Above a fixed initial bound, monotonicity gives fixed ordinal shifts $\theta,\theta'$ with \[ b_\xi\leq b'_{\theta+\xi},\qquad b'_\xi\leq b_{\theta'+\xi} \quad(\xi\in\Ord). \] For example, choose the shifted initial value beyond the disturbed continuum segment and induct using their common continuum function there. If $\delta$ is a beth fixed point in either model above these shifts, then $\delta$ is an infinite cardinal and $\theta+\xi,\theta'+\xi<\delta$ for every $\xi<\delta$. The inequalities put all values of the other beth sequence below $\delta$. Continuity, together with $\beth_\delta\geq\delta$, makes it a fixed point there too. Thus the high beth fixed points and their triple successors agree. Describe a coding block by its actual first beth fixed point and its ordinal length. This avoids any change in the enumeration below the agreement bound. Now let $U$ be a set-forcing extension of $D$. For any ordinal set $x\in D$, choose one of its codes above the forcing size and the bound for agreement of locations. The unchanged truth pattern defines $x$ in $U$ from the starting point and length. Ordinal codes for transitive closures then give $D\sq\HOD^U$. The same reasoning gives the Ground Axiom in $D$. If $D=W[g]$ were a nontrivial set extension, a sufficiently high code for each ordinal set of $D$ could be read in $W$. Separation in $W$ would reconstruct every such set. Choice then gives $D=W$, a contradiction. Finally, let $W$ be any ground of $U$. Downward directedness of grounds gives a common ground below $D$ and $W$; see \cite{UsubaGrounds,Usuba}. The intermediate-model theorem makes it a ground of $D$. The Ground Axiom makes this common ground equal to $D$. Since $D$ itself is a ground of $U$, its mantle is exactly $D$. \end{proof} The Continuum Coding Axiom also gives secure grounds by the same high-code and Ground Axiom argument \cite{ReitzGA}. Its continuum codes entail unbounded failures of GCH. The $\diamondsuit^*$ preparation is what allows the later choice envelope to satisfy eventual GCH. \begin{lemma}[A fresh GCH envelope]\label{lem:gch-envelope} Suppose $M\models\ZF$ and $B=M[K]\models\ZFC+\CM$ is a weakly homogeneous set-forcing extension with no new ordinal $\omega$-sequences. If $B$ satisfies eventual GCH, there is a further set-forcing extension $B'=B[H]$ such that \[ B'\models\ZFC+\GCH+\CM,\qquad (\Ord^\omega)^{B'}=(\Ord^\omega)^M. \] Moreover $B'/M$ is a weakly homogeneous set-forcing extension. \end{lemma} \begin{proof} In $B$, choose an inaccessible $\delta$ above all GCH exceptions. Use the following presentation of $L_\delta=\Col(\omega_1,<\delta)$. A condition is a countable partial function $p$ on $\delta\times\omega_1$ with $p(\beta,\xi)<\beta$, ordered by reverse inclusion. All ordinals below $\delta$ are coordinates; the definition does not use a model's list of cardinals. In $B$ this forcing is countably closed, has size $\delta$, and is $\delta$-cc. For the last assertion, the generalized $\Delta$-system lemma gives a common root for $\delta$ many countable domains. Inaccessibility bounds the number of value assignments on that root below $\delta$. Two conditions therefore agree on the root and are compatible. Each nonzero coordinate adds a surjection from $\omega_1$ onto that ordinal. Hence $\omega_1$ is preserved, $\delta$ becomes $\omega_2$, and all cardinals at least $\delta$ are preserved. There are no new reals, and the old continuum has size less than $\delta$, so CH holds. A nice name for a subset of $\omega_1$ uses $\omega_1$ antichains, each of size less than $\delta$. The entire name has size less than $\delta$, so $\delta^{<\delta}=\delta$ bounds their number by $\delta$. Thus $2^{\omega_1}=\delta=\omega_2$. For each old cardinal $\lambda\geq\delta$, a name for a subset of $\lambda$ is coded by a subset of $\lambda\times L_\delta$. There are at most $(2^\lambda)^B$ such codes, and that cardinal is preserved. The old subsets give the opposite bound, so the continuum cardinal at $\lambda$ is unchanged. This proves global GCH. Small forcing preserves all $B$-measurables above $\delta$. The models $M$ and $B$ have the same countable ordinal sequences, so they agree on $\omega_1$ and on this literal presentation of $L_\delta$. An enumeration of a condition is coded by one ordinal $\omega$-sequence and therefore belongs to $M$. The same observation applies to the countable graphs of the permutations used below. No inaccessibility assumption on $\delta$ in $M$ is needed. Permute the second coordinate $\omega_1$ to move the countable domain of one condition away from that of another. A permutation with countable support suffices, and belongs to $M$. It witnesses weak homogeneity of $L_\delta$ there. If $\mathbb C\in M$ is the old forcing for $K$, the product lemma identifies $B'=M[K,H]$ as an extension by the fixed product $\mathbb C\times L_\delta$. This product is weakly homogeneous. Countable closure is used in the choice model $B$, so it adds no ordinal $\omega$-sequences. This proves all assertions. \end{proof} \begin{lemma}[Recognizing an envelope]\label{lem:recognize} Suppose $D$ is secure and $B=D(A,K)$ is a set-forcing extension of $D$ satisfying $\ZFC$. Choose $\eta$ with $A,K\in V_\eta^B$. If $U$ is a further set-forcing extension preserving $V_\eta^B$, then the actual class $B$ is definable in $U$ from the ordinal $\eta$ by \[ B=D(V_\eta^U). \] \end{lemma} \begin{proof} The right-hand model is constructed inside $B$ when $V_\eta^U=V_\eta^B$, and contains $D,A,K$. Thus it equals $B$. Security identifies $D$ inside $U$ as its mantle. \end{proof} \begin{remark}\label{rem:ODnotHOD} Definability of the \emph{class} $B$ does not imply $B\sq\HOD^U$. Similarly, $V_\eta^U$ is OD but need not belong to HOD. The decoder can therefore recognize the choice envelope without placing its new wellorderings in the target inner model. \end{remark} \section{Exact external realization}\label{sec:realize} \begin{proposition}[Realization over a secure ground]\label{prop:secure-realize} Suppose \[ D\sq M=D(A)\sq B=M[K], \] where $D\models\ZFC+\CM$ is secure, $A\sq\mu^\omega$, $B$ is a set-forcing extension of $D$ satisfying $\ZFC$, and $B/M$ is weakly homogeneous with no new ordinal $\omega$-sequences. Then there is a further set-forcing extension $U$ of $B$ such that \[ U\models\ZFC+\CM,\qquad \Hseq^U=M,\qquad M\models\SVC+\CM. \] If $B$ satisfies eventual GCH, one may also require $U\models\GCH$. \end{proposition} \begin{proof} If $B$ satisfies eventual GCH, first apply Lemma~\ref{lem:gch-envelope} to obtain $B'=B[H]$ with GCH. Otherwise put $H=\varnothing$ and $B'=B$. In either case $B'/M$ is weakly homogeneous and adds no ordinal $\omega$-sequences. Since $B$ is a set extension of $D$, so is $B'$, and we have $B'=D(A,K,H)$. Choose $\eta$ in this actual envelope $B'$ so that $A,\seq{K,H}$ belong to $V_\eta^{B'}$. Apply Corollary~\ref{cor:ODcoding} over $B'$, starting above $|V_\eta^{B'}|$, to code $A$, and call the extension $U$. Lemma~\ref{lem:recognize}, with the pair $\seq{K,H}$ as its second generator, gives \[ B'=D(V_\eta^U). \] Thus the capped-history spectrum defines $A$ in $U$. In the GCH case, Lemma~\ref{lem:spectrum-gch} gives $U\models\GCH$. The combined forcing from $M$ to $U$ is weakly homogeneous. The name for the coding forcing is uniformly defined from the old $A$ and ordinal parameters. Automorphisms of the first forcing carry it to a forced equal name and therefore lift to the iteration. The second forcing is forced weakly homogeneous. For a local name for a second-stage automorphism, use the identity off a condition forcing it to be an automorphism. This requires only localized Boolean mixing, without a choiceless maximum principle. By hypothesis, the first extension adds no ordinal $\omega$-sequences; the coding extension is highly distributive over the choice model $B'$. Lemma~\ref{lem:homdesc} gives $\Hseq^U\sq M$. Conversely, $D\sq\HOD^U\sq\Hseq^U$ and $A\in\Hseq^U$. The latter holds because it is OD in $U$ and every member of $A$ is an allowed ordinal-sequence parameter. Minimality of $D(A)$ gives $M\sq\Hseq^U$. The entire extension $U/D$ is by set forcing. All sufficiently high normal $D$-measures lift to $U$, and their restrictions \eqref{eq:measure-restrict} belong to $M$. Thus both models have a proper class of measurables. Finally, $B=M[K]\models\ZFC$ is a set-forcing extension of $M$. The truth lemma gives a condition forcing Choice. Restricting the forcing to that condition shows that Choice is forceable over $M$. Blass's equivalence of this property with SVC, as stated in \cite[Theorem~3.14]{Usuba}, gives $M\models\SVC$. \end{proof} The next preparation allows us to apply this proposition without assuming that class forcing preserves $\DC$ in arbitrary choiceless intermediate models. \begin{proposition}[Installing the secure ground]\label{prop:install} Suppose $M=D(A)\models\ZF+\DC+\CM+\SVC$, where $D\models\ZFC+\CM$ is a symmetric ground and $A\sq\mu^\omega$. Given an ordinal $\alpha$, there are \[ D^*\sq M^*=D^*(A)\sq B^*=M^*[K] \] satisfying the hypotheses of Proposition~\ref{prop:secure-realize}, with $B^*$ satisfying eventual GCH and \[ V_\alpha^{M^*}=V_\alpha^M. \] \end{proposition} \begin{proof} Take a fresh envelope $B=M[K]$ from Lemma~\ref{lem:envelope}. The symmetric-ground relation composes with set-forcing extensions. Since $D$ and $B$ satisfy Choice, $D$ is a set-forcing ground of $B$ by \cite[Lemma~5.8]{Usuba}. Write $B=D[b]$ using a forcing presentation in $D$. Let $\mathbb P\in D$ be the presentation with generic $b$. Choose in $D$ a regular $\delta>\max(|\mathbb P|,\omega)$, above a uniform $\mathbb P$-name bound for the cardinality of the protected $B$-rank. Such a bound is available before evaluating $b$, using a set of names for that rank. Choose the preparation $\mathbb Q$ of Lemma~\ref{lem:secure} in $D$, independently of $b$, with every set-sized initial segment $\mathbb Q_\beta$ $<\delta$-closed in $D$. Take a coherent class generic $J$ over $B$ for this fixed $D$-iteration in the set-name framework just specified. For every $\beta$, the ordinary product lemma gives \[ D[b][J_\beta]=D[J_\beta][b]. \] Since $\mathbb P$ is $\delta$-cc, Easton's lemma makes the fixed $\mathbb Q_\beta$ $<\delta$-distributive in $B$. This does not assert that its ground closure persists in $B$. This commutation of small forcing with class preparation is used in \cite[Appendix, Lemma~121]{ReitzGA}. Put $D^*=D[J]$. Every dense subset of the fixed $\mathbb P$ in $D^*$ appears in some $D[J_\beta]$, where $b$ is generic by the product lemma. Thus $b$ is generic over $D^*$, and \[ B^*=D^*[b]=\bigcup_\beta B[J_\beta]\models\ZFC, \qquad M^*=D^*(A). \] Every short ordinal sequence in $B^*$ appears at a set stage. Distributivity at each such stage therefore shows that $B^*/B$ adds none of length less than $\delta$. It also preserves the protected rank: a first new set in that rank would be a new subset of an old set of cardinality less than $\delta$, coded by its old wellorder as a short ordinal sequence. Thus, by freshness of $B/M$ and the inclusions $M\sq M^*\sq B^*$, \begin{equation}\label{eq:same-sequences} (\Ord^\omega)^{M^*}=(\Ord^\omega)^{B^*}=(\Ord^\omega)^M. \end{equation} We claim \begin{equation}\label{eq:intersection} M^*\cap B=M. \end{equation} Every set of $D^*(A)$ belongs to $M[J_\beta]$ for some set-sized initial segment of the class iteration. Indeed, take a bounded transitive-base construction witnessing membership, then a stage at which the required rank of $D^*$ has stabilized. The old set forcings for $K$ and $J_\beta$ are mutually generic over $M$, so \[ M[J_\beta]\cap M[K]=M. \] The usual product-intersection proof works over $\ZF$: compare two names for a first new set of a given rank and use product conditions deciding membership. This proves \eqref{eq:intersection}. Together with preservation of the protected $B$-rank, it gives $V_\alpha^{M^*}=V_\alpha^M$. The same filter $K$ is generic over $M^*$ for the \emph{fixed} old collapse forcing. Each dense set in $M^*$ appears in some $M[J_\beta]$, where mutual genericity makes $K$ meet it. Also $B^*=M^*[K]$. One inclusion holds inside $B^*$. For the reverse inclusion, $D^*\sq M^*$ and $b\in B=M[K]\sq M^*[K]$ give $D^*[b]\sq M^*[K]$. The old collapse automorphisms still witness weak homogeneity, and \eqref{eq:same-sequences} shows that there are no new allowed parameters. By Lemma~\ref{lem:secure}, $D^*$ is secure and satisfies $\ZFC+\CM$ and eventual GCH. Its set-forcing extension $B^*$ also satisfies eventual GCH: above the forcing size, the cardinals and continuum cardinal values are unchanged. Thus the GCH clause of Proposition~\ref{prop:secure-realize} applies. The set-forcing identity $B^*=M^*[K]$ also yields $M^*\models\SVC$ by Blass's equivalence. We have not assumed that the class preparation preserves $\DC$ in $M^*$. Once $M^*$ is identified with $\Hseq^U$, Lemma~\ref{lem:HDC} gives $\DC$. \end{proof} \begin{proof}[Proof of Theorem~\ref{thm:external-realization}] From $\SVC$, take a choice symmetric ground $D$ and a transitive generator $T$ with $M=D(T)$; see \cite[Proposition~5.4]{Usuba}. The choice ground may be taken to have a proper class of measurables: make a set-generic choice envelope, use Lemma~\ref{lem:ZFmeasure}, and apply downward L\'evy--Solovay to the resulting choice-ground presentation. Alternatively, in the application from Theorem~\ref{thm:rank-transfer}, the ground $D$ already has this property. By $\KW$, choose a surjection $f:(\mu^\omega)^M\to T$. Code its domain and the relation $f(p)\in f(q)$ by a single set $A$ of ordinal $\omega$-sequences. Equality of predecessor sets and the well-founded extensional collapse, as in Proposition~\ref{prop:seed}, recover $T$ and $f$. Hence $M=D(A)$. Apply Proposition~\ref{prop:install} and then Proposition~\ref{prop:secure-realize}. \end{proof} \section{The three consistency implications}\label{sec:finish} \begin{proof}[Proof of Theorem~\ref{thm:external-main}] The implication $\Con(E_2(\sigma))\Rightarrow\Con(E_1(\sigma))$ follows directly from the definitions. If $U\models E_2(\sigma)$, Lemma~\ref{lem:HDC} gives $\Hseq^U$ as a model of $E_3(\sigma)$. Hence $\Con(E_2(\sigma))\Rightarrow\Con(E_3(\sigma))$. Proposition~\ref{prop:one-three} gives $\Con(E_1(\sigma))\Rightarrow\Con(E_3(\sigma))$ without assuming that the original external HOD already contains a proper class of measurables. For the remaining direction, let $V\models E_3(\sigma)$ and choose $\kappa$ with $V_\kappa^V\models\sigma$. Apply Theorem~\ref{thm:rank-transfer} above $\kappa$ to obtain a sequence-generated model $M$ with $V_\kappa^M=V_\kappa^V$. Apply Theorem~\ref{thm:external-realization} while protecting that rank. The resulting $U$ satisfies $\ZFC+\GCH+\CM$, and \[ \Hseq^U\models\SVC+\CM, \qquad V_\kappa^{\Hseq^U}=V_\kappa^M=V_\kappa^V. \] Hence $U\models E_2(\sigma)$, completing the cycle of implications. \end{proof} \subsection*{Why this is an external theorem} The original Prikry ambient universe contains the master sequence $c$. Every external $\Hseq$ contains all ambient ordinal $\omega$-sequences, including $c$. We therefore cannot simply take the final external HOD in that universe. The master can expose real-coded information omitted from the intermediate model. Lemma~\ref{lem:envelope} provides a \emph{fresh} choice envelope with no new ordinal $\omega$-sequences. The high witnesses in Section~\ref{sec:spectrum} need not belong to the final $\Hseq$. Their ambient existence makes $A$ definable, and weak homogeneity controls hereditary descent. The proof requires neither tree-Prikry completions of the Cohen caps nor a unique high witness for each code. \subsection*{Proof dependencies and scope} The construction uses two nonstandard forcing results, Lemma~\ref{lem:paired} and Theorem~\ref{thm:spectrum}. The first uses tagged finite interpolation and a countable diagonal argument. The second applies an existing approximation criterion to the displayed quotient order. Both are needed, for different parts of the proof. Lemma~\ref{lem:earlier-core} supplies the separate fine-structural reduction. The following qualifications describe their scope. \begin{enumerate} \item The global rank-preservation proof uses literal equality of $Q,F$ and of supported parameters, not merely isomorphism of their indexing structures. \item The $\DC$ proof uses external countable domination and wellorderable search spaces; it does not assert that every ambient countable sequence belongs to the inner model. \item The cap spectrum is computed over the actual recognizable envelope. It requires no classification of arbitrary incomparable grounds. \item The secure preparation uses repeated $\diamondsuit^*$ codes and retains a proper class of measurables. A subsequent countably closed set collapse gives global GCH in the choice envelope; the final evaluated cap forcing preserves it. The protected rank belongs to the target inner model and need not satisfy GCH. \item The conclusion concerns first-order sentences true in a rank segment. It neither identifies the complete theories of the three ambient universes nor proves the internal assertion $V=\HOD_{\Ord^\omega}$ in the original model. \end{enumerate} \section{A canonical relative inner model with unbounded Woodin cardinals} \label{wd-inner-model-section} The reverse consistency argument needs a choice model containing a prescribed real, with unbounded Woodin cardinals, whose definition is unchanged by a finite recursive recoding of that real. It also needs this model to be a set-forcing extension of its own HOD. We establish these requirements together. The fine structure used below is the classical Mitchell--Steel short-extender fine structure of pure-extender premice. The model we construct has no strategy predicate. For a real $r$, put \[ a(r)=\HYP(r)=L_{\omega_1^{\mathrm{CK},r}}[r]. \] Here $\HYP(r)$ denotes the entire transitive admissible set, including its ordinals, rather than its collection of reals. It is countable, transitive, and self-wellordered in the usual relative-premouse sense. The normalization by $a(r)$ will remove the choice of a real code from the construction. \begin{convention}\label{wd-relative-convention} We use classical premice over the named transitive base $a$. Every relative Skolem hull contains $a\cup\{a\}$, and every extender has critical point above $\operatorname{rank}(a)$. Cores, projecta, standard parameters, and ultrapowers are taken in this one convention throughout. An enumeration or wellorder of $a$ may be used to prove a property of a premouse; it is not an additional predicate of that premouse. For a class premouse $C$, \emph{countable iterability} means that every countable elementary pullback of a set initial segment, with the base fixed pointwise, has the ordinary Mitchell--Steel stack iterability in the applicable degrees. The game allows taking an initial segment at the start of a round. This is the countable-hull convention of \cite[Section~1.1]{SteelCoreBook}; the relative fine-structural \L o\'s and copying conventions are those of \cite[Section~2.5]{SteelTutorial}. \end{convention} \begin{theorem}[Canonical Woodin envelope]\label{wd-envelope} There is a uniform first-order class definition $F(a)$ such that $\ZFC+\PCW$ proves the following, with assertions of $\ZFC$ understood schematically. For every real $r$, if $a=\HYP(r)$ and $C=F(a)$, then: \begin{enumerate}[label=\textup{(\roman*)}] \item $C$ is a transitive inner model containing $a$ as a set, and $C\models\ZFC+\PCW$; \item the definition uses only the pure set $a$, with no chosen enumeration, background witness, or iteration strategy; \item $C$ is a set-forcing extension of $\HOD^C$. \end{enumerate} Consequently, in the same ambient universe, \[ r\equiv_T s\quad\Longrightarrow\quad F(\HYP(r))=F(\HYP(s)). \] \end{theorem} The equality in the last assertion is literal equality of the resulting classes. It is a same-universe assertion; no generic absoluteness of $F$ is asserted or needed. We prove the theorem in four steps. \subsection{The standard background construction and its stopping rule} \label{wd-background} We use the fully backgrounded, minimum-support Mitchell--Steel construction, with its usual core and limit clauses \cite{MSFine}. The explicit version in \cite[Section~2.3]{LNSBackground} fixes the transition rule we need. Suppose that the current sound premouse $M_\xi$ is passive and has height $\alpha$. An active extension with fine extender $E$ and support $\nu<\alpha$ is eligible when $(M_\xi,E)$ is a premouse and there is a total background extender $E^*$ over the ambient universe such that \begin{equation}\label{wd-background-predicate} V_{\nu+\omega}\subseteq\operatorname{Ult}(V,E^*), \qquad E\restr\nu=E^*\cap \bigl([\nu]^{<\omega}\times M_\xi\bigr). \end{equation} Among eligible extensions, the construction takes one of least support. It first forms the raw active level $N_{\xi+1}$, verifies reliability, and then takes its $\omega$-core. If there is no active extension, or the current level is active, it instead forms the usual raw passive Jensen successor before the same reliability and core operations. At a limit $\lambda$, the raw level has height \[ \eta_\lambda=\liminf_{\xi\longrightarrow\lambda} (\rho_\omega(M_\xi)^+)^{M_\xi}; \] its bounded initial segments are the stabilized bounded initial segments of the earlier levels. Reliability is again checked before taking the core. We retain the raw levels and the decoded cores as distinct objects. This distinction matters when a core is represented by a type~III code. We add diagnostic stopping tests, without changing a transition which passes those tests: \begin{enumerate}[label=\textup{(\alph*)}] \item Test each raw level for nontameness before testing reliability or taking a core. Test the decoded core as well. \item At a passive core, stop if any eligible active head is nontame, before selecting a minimum-support head. \item Stop if a core already has a sound tame active type~I proper initial segment whose top critical point is a limit of Woodin cardinals above the base. \end{enumerate} At a stop, we will choose the least index of a segment as in (c) on the already determined sequence. The extraction argument below proves that such a segment exists in every genuine stopping case. We record precisely the classical fine-structure inputs to this construction. The tame extension of Mitchell--Steel fine structure gives reliability, solidity and universality of the relevant cores, and countable-hull stack iterability for tame backgrounded levels and their associated comparison objects \cite{SchimmerlingSteelTame}. In particular, it applies to the associated bicephali used in next-extender uniqueness; this scope of the tame theory is also explained in \cite[p.~9]{SteelCMIP}. The assertion is about tame levels of the construction and their associated objects. It does not require that every premouse in the universe be tame. Before we continue at a passive core, test (b) has excluded every nontame eligible head. Two eligible heads of minimum support therefore give an associated tame bicephalus to which the joint iterability and next-extender uniqueness theorems apply. The classical category check is useful here: type~II has successor natural support, whereas types~I and~III have limit natural support. Equal minimum support places the two heads in the same category covered by the classical uniqueness theorem. Thus the fine extender is unique. We use joint iterability of the associated bicephalus, not an inference from separate iterability of its two heads. The witness $E^*$ in \eqref{wd-background-predicate} is only existential data. Once the fine head is unique, different witnesses do not change the next premouse. Jensen successor, core-taking, the liminf clause, and the diagnostic tests are uniform from the current set structures. The resulting recursion is therefore definable from $a$ alone. No wellorder of the possible background witnesses is used. Since $a$ is countable in the ambient universe, the critical point of any total background extender, being measurable there, exceeds $\operatorname{rank}(a)+\omega$. This bound may be used in the relative fine-structure calculations without adding an eligibility restriction to \eqref{wd-background-predicate}. \begin{lemma}\label{wd-never-stops} If the construction never stops, its stabilized class limit is a countably iterable inner model of $\ZFC+\PCW$ containing $a$. \end{lemma} \begin{proof} Every raw level and decoded core is tame. The tame fine-structure theorem therefore supplies reliability at the point where the ordinary construction requires it, so there is no breakdown. The standard core-stabilization theorem gives the class premouse limit. We now apply the Woodin-inheritance theorem for this very construction: the fully backgrounded Mitchell--Steel construction, when it does not break down, inherits the ambient Woodin cardinals. This is the theorem recalled at the opening of \cite{SteelLocalKc}. In the relative version, the Woodins above the base are inherited, which suffices for $\PCW$. All extender critical points fix $a$, so the usual reflection and background-restriction proof uses exactly the same bounded data above the base. In particular, we have not imposed an extra inaccessible- length or certificate requirement on \eqref{wd-background-predicate}. Such a restriction would require a separate inheritance argument. The classical fine structure and stabilization give $\ZFC$ for the proper-class limit. To check the required countable iterability, fix a set initial segment and a countable pullback. A sufficiently late tame stage contains its stabilized segment. Include the segment and the pullback map in the ambient hull used for that stage's iterability theorem, and use the initial-segment move and copying. This supplies the required stack strategy on the pullback. \end{proof} \subsection{Extracting a tame top measure at the first overlap} \label{wd-extraction} The stopping alternative does not require an iterable nontame mouse. It uses a measure fragment already present on a determined sequence. We give the endpoint details because the Woodin overlapped by the new extender can equal its natural support. \begin{lemma}[First-overlap extraction]\label{wd-first-overlap} Suppose a first nontame active level $Q=(P,E)$ is encountered in the construction above, either as an eligible head or inside a decoded core. Then the already determined sequence below that head has a sound tame active type~I segment $S$ whose top critical point is a limit of Woodin cardinals. The countable elementary pullbacks of $S$ have the inherited stack iterability. The least index of such a segment is determined by the preceding core, without choosing a bad head or a countable hull. \end{lemma} \begin{proof} Choose the first offending extender index in the indicated premouse. Write \[ \kappa=\operatorname{crit}(E),\qquad \nu=\nu(E),\qquad \alpha=\operatorname{lh}(E),\qquad P=J_\alpha[\vec E,a]. \] There is a $\delta\geq\kappa$ which $P$ regards as Woodin and which is overlapped by $E$. All earlier active initial segments are tame. Let $i$ be the degree-zero ultrapower map by $E$, and put $R=i(J_\kappa^P)$. The coherence and indexing axioms give \begin{equation}\label{wd-overlap-coherence} J_\alpha^R=P, \qquad \alpha=(\nu^+)^{\operatorname{Ult}_0(P,E)}, \qquad \alpha\kappa$. If $\delta=\kappa$, the proper segment through $(\kappa^+)^P$ would have the same subsets of $\kappa$ and would regard $\kappa$ as a Woodin limit of Woodin cardinals. That segment is tame and has iterable countable pullbacks. This contradicts the tame-smallness fact recorded immediately after \cite[Definition~6.15]{SteelOutline}: a tame mouse cannot have a Woodin limit of Woodin cardinals. Set $\eta=(\kappa^+)^P$. Then \[ \kappa<\eta<\delta\leq\nu. \] Apply the initial-segment condition to $E\restr\eta$. Its natural support is $\eta$, so this is not the type~Z exceptional fragment. The condition puts its trivial completion either earlier on the sequence of $P$, or on the one-step ultrapower using a nonempty extender indexed at $\eta$ \cite[Definition~2.4(3)]{SteelOutline}. The second alternative is impossible: $\eta$ is a cardinal of $P$, whereas a nonempty extender at that index makes it noncardinal at the next Jensen stage, which still lies below $\alpha$. Thus the completion occurs at an earlier index $\gamma<\alpha$ on the sequence of $P$. The active segment at $\gamma$ is the desired $S$. Its extender is the normal-measure fragment with critical point $\kappa$, hence is type~I. It agrees on the bounded sets below $\kappa$, so its top critical point remains a limit of Woodin cardinals. It is tame by the choice of the first offending index, and it is sound as a proper initial segment. Here is the iterability accounting. When $P$ is a passive decoded core of a tame background level $N$, a countable hull of $P$ maps weakly into $C_\omega(N)$. The tame level theorem supplies its stack iterability, and the initial-segment choice before the first round supplies that of the corresponding pullback of $S$. If instead the decoded core itself is nontame, take an ambient countable hull containing the \emph{unsquashed} core, its code, the chosen overlap witness, and the relevant set satisfaction relations. Collapse this data together. The overlap witness survives even when it uses a type~III top extender and the endpoint $\delta=\nu$ lies outside the ordinal domain of the squashed code. The restriction on the codes is the weak core embedding to which the tame predecessor's iterability theorem applies. We may therefore take the first bad active initial segment and then the proper segment $S$ just found. This uses iterability inherited from the preceding tame level, not an assumed strategy on a newly adjoined bad head. Finally, the fragment belongs to the fixed preceding sequence. The existence of a bad eligible head is used only to prove that a suitable index exists there. Taking the least suitable index makes $S$ independent of the choice of that head. Countable hulls are used to verify iterability, never to select the output. \end{proof} For completeness, the raw-level tests create no further stopping case. A first nontame passive successor would already have its local overlap witness on the previously tested indexed extender sequence. At a first nontame limit, that witness is bounded and occurs in a stabilized earlier segment. Thus neither can be the first new failure. The tests are nevertheless made before reliability, so the proof never takes a core whose existence has not been justified. \subsection{Iterating the top measure out of the model} \label{wd-top-iteration} \begin{lemma}[Top-measure envelope]\label{wd-top-envelope} Let $S$ be a sound tame active type~I premouse over $a$, with inherited countable-hull stack iterability, whose top critical point $\kappa$ is a limit of Woodin cardinals above the base. There is a class premouse $C_S$, uniformly definable from $S$, containing $a$, whose pure universe satisfies $\ZFC+\PCW$. Its set initial segments have the countable iterability of Convention~\ref{wd-relative-convention}. \end{lemma} \begin{proof} Form the linear degree-zero iteration of the top measure. Every set-length history is wellfounded. For if a first bad history existed, take a countable elementary hull of a sufficiently large ambient $H_\Theta$ containing the history, its maps and direct-limit data, and an actual descending $\omega$-sequence in the illfounded last structure. The collapse is a bad countable linear history of a countable pullback of $S$, contradicting its inherited stack strategy. This argument also covers an uncountable $S$: the starting model in the collapsed history is its iterable pullback, rather than $S$ itself. The unique compatible set recursions therefore define the linear iteration through all ordinals. Write $S_\xi$ for the iterates, $i_{\xi\zeta}$ for their maps, and $\kappa_\xi=i_{0\xi}(\kappa)$. We will show that \begin{equation}\label{wd-rank-chain} B_\xi=J_{\kappa_\xi}^{S_\xi} =V_{\kappa_\xi}^{S_\xi}, \qquad B_\xi\prec B_\zeta\quad(\xi<\zeta), \end{equation} where the elementary map in the second assertion is literal inclusion. Some care is needed because the entire active premouse $S$ has not been assumed to satisfy $\ZFC$. First, $\kappa$ is internally regular in the sense required below. If $S$ contained a cofinal $f:\lambda\longrightarrow\kappa$ with $\lambda<\kappa$, the next degree-zero map $j$ would send it to a cofinal map from the same $\lambda$ to $j(\kappa)$. This statement is bounded in its displayed parameters. But $j(f)(\xi)=j(f(\xi))=f(\xi)<\kappa$ for every $\xi<\lambda$, a contradiction. The same argument rules out a bijection from a smaller ordinal onto $\kappa$. The cofinal Woodin cardinals and acceptability give strong-limit closure below $\kappa$. Given $\tau<\kappa$, choose a Woodin between $\tau$ and $\kappa$. Its bounded inaccessible-rank calculation locates the power set of $\tau$ and a bound on its size below that Woodin; acceptability excludes new subsets at later levels. Consequently the usual acceptable-hierarchy calculation above a self-wellordered base gives $J_\kappa^S=V_\kappa^S$. Each of its elements has an internal wellordering of order type below $\kappa$. All its power sets agree with those computed in $S$ and belong to $J_\kappa^S$. Put $B=J_\kappa^S$. The type~I top index lies beyond $\kappa^+$, so $B$ itself and the finite Jensen successor closures used next are sets in $S$. Fix a formula $\varphi$ and parameters from $B$, and suppose that, in $B$, it defines a function on $x\in B$. Relativize all quantifiers of this one formula to the set $B$. The resulting graph is a bounded-definable subset of $x\times B$, and belongs to a finite Jensen successor closure above $B$, still inside $S$. There is no appeal to Replacement in $S$ in forming this graph. Assign to each value its least construction level below $\kappa$. The hierarchy through $\kappa$ and this least-level graph also lie in the finite successor room above $B$. If these levels were unbounded in $\kappa$, composition with an internal enumeration of $x$ of length $\lambda<\kappa$ would give, in $S$, a cofinal map $\lambda\longrightarrow\kappa$. Internal regularity excludes this. Thus the range is bounded in some $J_\eta^S$, $\eta<\kappa$. Coding that level by a set of size below $\kappa$ and using the power-set calculation puts the range in $B$. This proves each Replacement instance. The same bounded-graph argument followed by the subset calculation proves Separation. The remaining elementary axioms and Choice follow from the acceptable relative hierarchy and the wellordering of the base. Hence $B\models\ZFC$. The Woodins cofinal in $\kappa$ remain Woodin in $B$: their subsets, functions, and bounded extender witnesses agree. Therefore $B\models\PCW$. Fine ultrapower coherence gives, for $\xi<\zeta$, \[ i_{\xi\zeta}(J_{\kappa_\xi}^{S_\xi}) =J_{\kappa_\zeta}^{S_\zeta}. \] These hierarchy sets are actual elements of the premice. Bounded relativization to them proves full elementarity of the maps between the set structures $B_\xi$ and $B_\zeta$, and transfers $\ZFC+\PCW$ from $B_0$ to every $B_\xi$. The maps fix $B_\xi$ pointwise. To see this, argue by rank and take an internal enumeration $e:\lambda\longrightarrow x$ with $\lambda<\kappa_\xi$ for $x\in B_\xi$. By induction its values are fixed, while bounded elementarity says that $i_{\xi\zeta}(e)$ maps the same domain onto $i_{\xi\zeta}(x)$. Thus $i_{\xi\zeta}(x)=x$. The base is fixed by convention. This proves \eqref{wd-rank-chain} with inclusion as the elementary map. The critical sequence is strictly increasing and unbounded in the ordinals. Define \[ C_S=\bigcup_{\xi\in\Ord} B_\xi. \] It is transitive and contains all ordinals. The elementary-chain argument applies to each formula: an existential witness in the union lies in a later stage and can be reflected to any earlier stage containing its parameters. Thus $B_\xi\prec C_S$, and $C_S\models\ZFC+\PCW$. The stabilized extender sequence presents it as the class premouse obtained by iterating out the top measure. For countable iterability of a set initial segment of $C_S$, include that segment, its pullback map, a sufficiently high top iterate, and the preceding linear history in an ambient countable hull. The collapsed starting premouse has its given stack strategy. Following the collapsed top history, and then taking its tail and the indicated initial segment, supplies the required strategy. This proves the countable-hull assertion. It does not assert a single strategy on the entire class premouse, and none is needed. \end{proof} \subsection{The fixed-base own-HOD argument} \label{wd-own-hod} The own-HOD step requires more than choosing a canonical extender sequence externally. We must define that sequence over the pure universe of the resulting premouse from bounded set parameters. We use the direct condensation-stack argument of \cite[Theorem~4.1 and Remark~4.3]{SchlutzenbergDefinability}, with the trivial forcing. The following proof gives the fixed-base and local-iterability details of that application. \begin{proposition}\label{wd-relative-own-hod} Let $C$ be a proper-class classical pure-extender premouse over a transitive self-wellordered base $a$. Suppose that its pure universe satisfies $\ZFC$, that $a$ is countable both in $C$ and in the ambient universe, and that $C$ has the countable iterability of Convention~\ref{wd-relative-convention}. Then, for some set of ordinals $t\in C$, \[ C=\HOD_{\{t\}}^C. \] In particular $C=\HOD^C[h]$ for set forcing in $\HOD^C$. \end{proposition} \begin{proof} Choose in $C$ an enumeration $e$ of $a$. Fix cardinals $\gamma<\theta$ of $C$, with $\theta$ regular, so far above the base that $a$, $e$, and a hierarchy segment coding them are bounded below $\gamma$. Put $m=C\restr\theta$. These are parameters for this internal proof; they do not change the external definition of $C$. \smallskip\noindent \emph{Local condensation.} The ordinary finite-degree solidity, universality, and sound-source condensation theorems hold with the base fixed \cite{MSFine,SteelCoreBook}. Each required instance on an uncountable set segment follows by reflection to a countable ambient hull containing the structures, the map, their set satisfaction relations, and $a$ pointwise. Countable iterability supplies the target strategy there. This derives local condensation without selecting a class strategy for $C$. For the sound-hull construction we also need the stronger condensation theorem for a $\rho$-sound source, which need not yet be fully sound. We use the passive degree-zero case of \cite[Theorem~5.2]{SchlutzenbergCondensation}. Retain its lifting, projectum, cardinal, and $\rho$-soundness hypotheses, place $a$ in each hull and fine theory, and require the maps to fix $a$ pointwise. The proof gives the same alternatives in this relative setting. We describe why its stronger conclusion, rather than just ordinary sound-source condensation, is available. The solid-core parameters and fine theories are formed using tuples from $a$ as well as the ordinal parameters. Relative \L o\'s and the classical hull calculations preserve them. In the equal-successor- cardinal case of that proof, the required agreement of power sets and generalized solidity witnesses is unchanged, since the base is fixed and has its enumeration below our cardinal floor. The condensation used for already sound proper segments is the ordinary theorem just established; the stronger conclusion is not assumed at this point. In the other case, the bicephali and cephalanxes have the same named base. The iterability proof starts with the source embedding and the identity into one iterable target, as in Claim~5 of the proof of the cited theorem. The Shift maps send $[u,f]$ to $[\pi(u),\pi(f)]$ and fix every element of $a$. Model and degree drops take initial segments over the same base; direct limits retain the fixed base. If a type~III structure occurs in a comparison, the usual squashed copying and unsquashing are performed with this same fixed-base \L o\'s calculation. The subsequent comparison analysis \cite[Theorems~4.3, 4.5, 4.17 and the proof of Theorem~5.2]{SchlutzenbergCondensation} uses least disagreement, extender lengths and generators, cardinal cutpoints, and the solid-core calculations. All these computations take place above the base. Replacing an ordinal hull by its hull together with $a$ does not repair an omitted-generator contradiction: the maps already have every base element in their range. The same terminal alternatives follow. In the passive degree-zero application these are the initial-segment and active-ultrapower possibilities, including the type~I normal-measure exception. The active type~II final alternative is absent. This supplies the stronger local condensation needed below. The argument has used classical relative premice throughout; no conversion to an operator-premouse convention is required. \smallskip\noindent \emph{Sound hulls above the base.} Repeat the finite sound-hull construction of \cite[Lemma~2.3]{SchlutzenbergDefinability}. In a passive $1$-sound target $H$ with $\rho_1^H\geq\gamma$, put $a$ into each generating set and include the desired finite data among its prescribed parameters. The recursion adjusts a finite decreasing ordinal parameter and a cardinal bound $\gamma_i$, maintaining $\gamma\leq\gamma_i$. At a nonterminal step it chooses a noncardinal new generator $\eta>\gamma$ while putting the earlier solidity witnesses in the appropriate preceding hull. The resulting collapse $W$ is $\rho$-sound, with \[ \rho=\gamma_i^{+W},\qquad \rho_1^W=\gamma_i; \] it has not at this stage been asserted $1$-sound. Apply the stronger condensation just proved in the specialization used by that lemma. Either $W$ is an initial segment of $H$, or the remaining exceptional case presents $W$ as a type~I degree-zero ultrapower with critical point $\gamma_i$. The exception contradicts the choice of the new generator: that ultrapower is generated by the old range and its normal-measure seed $\gamma_i$, with the standard-parameter tail carried along. Since the old range already contains $a$, the proposed new generator would be in the hull generated by $a$, $\gamma_i+1$, and that tail. Thus $W$ is an initial segment. Its description as the least relevant projecting segment makes the next solidity witness available in the next hull. Each nonterminal step strictly decreases the cardinal bound. The bound remains at least $\gamma$, so the recursion terminates with a sound collapse containing the prescribed objects in its range. In particular it never crosses the base. This proves soundness for these adjusted hulls, rather than for arbitrary hulls. The simultaneous version is obtained by alternating these parameter adjustments for two passive successor structures with the same pure universe and the same initial segment $m$. Include $a,e$, the two preceding structures, and a prescribed element $x$ in the common parameters. At each adjustment retain the previously arranged ordinal agreement and mutual containment. The construction in \cite[Theorem~4.1, Subclaim~1.1]{SchlutzenbergDefinability}, with trivial forcing, then gives sound collapses of the same ordinal height whose uncollapse maps agree on ordinals and on $a$. The enumeration $e$ ensures that the common pure-universe collapse also fixes the whole base. \smallskip\noindent \emph{The internal regular stack.} Let $\eta\geq\theta$ be regular in $C$. Compute inside $C$ the Jensen stack of sound classical $a$-premice extending $C\restr\eta$, projecting to $\eta$, and satisfying the condensation properties above. This stack is exactly $C\restr\eta^{+C}$. Here both the internal qualification and the equality are important. For comparability, put the base pointwise into the common hull in the proof of \cite[Fact~3.1]{SchlutzenbergDefinability}. Regularity makes the hull's intersection with $\eta$ an ordinal. The two collapse maps have the corresponding common critical point, and their projecta collapse to it. Sound-source condensation places the collapses in the same initial segment of the root, or in the same exceptional ultrapower of that root, giving comparability. For a candidate coded in $C$, compare with a sufficiently high true sound projecting segment containing it. The argument of \cite[Fact~3.2]{SchlutzenbergDefinability} puts the candidate on the true sequence. Conversely, the acceptable-hierarchy calculation gives cofinally many sound projecting levels below $\eta^{+C}$: the bounded power sets are already fixed below $\eta$, and the levels adding the relevant subsets of $\eta$ project to $\eta$. Their union is the true successor-cardinal segment. Its pure universe is $H_{\eta^+}^C$. We have made no assertion about a stack containing every externally available mouse. \smallskip\noindent \emph{Uniqueness over the pure universe.} Use the excellent-candidate definition in the direct proof of \cite[Theorem~4.1]{SchlutzenbergDefinability}, restricted to the fixed base $a$ and trivial forcing. A candidate extends $m$, has regular height $\eta$, has the local condensation just used, and has a successor-cardinal stack whose pure universe is $H_{\eta^+}^C$. The true $C\restr\eta$ is a candidate by the preceding paragraph. If $R$ is another candidate, alternately take the least appropriate projecting extensions on the two sides containing the preceding structure on the other side. The resulting $\omega$-unions, and then their passive successors, have the same pure universe. For each $x$ in this universe, take the simultaneous sound hulls just constructed. Condensation places both collapsed mice in the common initial segment $m$. They have the same ordinal height, hence are the same premouse. Their uncollapse maps agree on ordinals and on $a$; relative Skolem generation makes the maps agree everywhere. Varying $x$ identifies the two successor structures and hence identifies $R$ with $C\restr\eta$. Excellence is expressed using set-coded premice, their satisfaction relations, and their bounded stacks. Thus this uniqueness defines $C\restr\eta$ over the pure universe $C$ from $m,a,e$, uniformly for all sufficiently large regular $\eta$. Taking their union defines the extender sequence of $C$ from those set parameters. No iteration strategy for a possibly spurious candidate is assumed: its required condensation is part of the candidate definition, and the adjusted-hull argument uses those properties directly. The relative Jensen hierarchy, together with the fixed enumeration of the base, now gives a global wellorder definable over $C$ from $m,a,e$. Every element is therefore hereditarily ordinal-definable from this tuple. Choice in $C$ permits coding the tuple and its transitive closure by one set of ordinals $t\in C$, giving $C=\HOD_{\{t\}}^C$. Vop\v enka forcing over $\HOD^C$, for the bounded ordinal code $t$, gives a generic filter $h\in C$ with \[ \HOD^C[h]=\HOD_{\{t\}}^C=C. \] This is the coarse own-HOD observation used in \cite[Introduction]{SchlutzenbergOrdinal}; no additional hypothesis for its subsequent refined conclusions is used here. The proof assumed $\ZFC$ only in the pure universe. All candidates, local satisfaction relations, and bounded stacks were sets. Codes for true initial segments belong to $C$ by its premouse hierarchy and amenability. After extender definability has been proved, formulas in the expanded premouse language can be translated into pure formulas with the fixed parameters. Expanded-language Separation and Replacement thus follow at the end; they were not assumed to obtain the definition. \end{proof} \subsection{Completion and recoding invariance} \label{wd-envelope-completion} \begin{proof}[Proof of Theorem~\ref{wd-envelope}] Run the construction of Section~\ref{wd-background} over the pure set $a=\HYP(r)$. If it never stops, use its stabilized limit from Lemma~\ref{wd-never-stops}. If it stops, choose the least qualifying type~I segment on the determined sequence, using Lemma~\ref{wd-first-overlap}, and use its top-measure envelope from Lemma~\ref{wd-top-envelope}. The transition rule, stopping tests, least-index choice, and unique linear iteration are all first-order uniform from $a$. This defines $F(a)$ without any additional choice parameter. In both cases $C=F(a)$ is a countably iterable classical premouse containing $a$, and its pure universe satisfies $\ZFC+\PCW$. Since $r\in a\in C$, we have $L[r]\subseteq C$. The ordinal $\omega_1^{\mathrm{CK},r}$ and the set $L_{\omega_1^{\mathrm{CK},r}}[r]$ are countable in $L[r]$; their enumerations therefore belong to $C$. Thus $a$ is countable in $C$ as well as in the ambient universe. Proposition~\ref{wd-relative-own-hod} applies and supplies the own-HOD set-forcing presentation. Finally, if $r\equiv_T s$, every admissible set containing $r$ contains $s$, and conversely: the recursive computation is available inside the admissible set. The least transitive admissible sets containing the two reals are consequently identical. Thus $\HYP(r)=\HYP(s)$, and the uniform pure-set definition gives the stated equality of envelopes. \end{proof} \begin{remark}\label{wd-envelope-scope} This construction retains fine structure. Its role is confined to the tame background construction, the first-overlap fragment, and the condensation needed for the own-HOD presentation. It requires neither the iterability of an arbitrary nontame premouse nor a strategy on the ambient universe. The enumeration used in the own-HOD proof is internal evidence about an already determined model; it is not part of the definition whose recoding invariance is used in the consistency argument. \end{remark} \section{From external HOD to a Woodin symmetric ground}\label{wd-reverse-section} We apply the relative inner-model theorem to a real coding a rank of external HOD. The recoding invariance is needed inside a single collapse extension. No absoluteness of the relative construction between different universes is used. \begin{proposition}\label{wd-reverse} Suppose $U\models\ZFC+\PCW$, let $H=\Hseq^U$, and fix an ordinal $\alpha$. In a set-generic extension of $U$ there are transitive classes $D\sq N$ such that \[ D\models\ZFC+\PCW,\qquad N\models\ZF+\DC+\SVC,\qquad V_\alpha^N=V_\alpha^H. \] Moreover, $N$ has a set-symmetric presentation over $D$. \end{proposition} \begin{proof} Choose $\lambda>\alpha+\omega$ with $\cf^U(\lambda)>\omega$, and put $X=V_\lambda^H$. By Lemma~\ref{lem:HDC}, $H$ is closed under $U$-countable sequences of its members. The cofinality condition then gives \begin{equation}\label{wd-X-closure} {}^\omega X\cap U\sq X. \end{equation} Indeed, the ranks of the countably many entries have a bound below $\lambda$, and adding the finitely many levels needed to code the sequence still leaves a rank below $\lambda$. The set $X$ is ordinal-definable in $U$ from $\lambda$. Force over $U$ with the finite partial functions from $\omega$ to $X$. Let $e:\omega\twoheadrightarrow X$ be the generic enumeration. Let $r$ code both relations \[ i\mathrel{E_r}j\ \longleftrightarrow\ e(i)=e(j), \qquad i\mathrel{R_r}j\ \longleftrightarrow\ e(i)\in e(j). \] Set forcing preserves the sufficiently high Woodins, so $U[e]\models\ZFC+\PCW$ by \cite{HamkinsWoodin}. Apply Theorem~\ref{wd-envelope} there to obtain \[ C=F(\HYP(r)),\qquad C\models\ZFC+\PCW, \qquad C=\HOD^C[h]. \] Since $r\in C$, the extensional quotient of $(\omega,R_r)$ by $E_r$ and its Mostowski collapse belong to $C$. Their collapse is the actual transitive set $X$. Thus $X\in C$. Define \[ N=\HOD_{X\cup\{X\}}^C. \] Here definitions may use $X$, finitely many of its elements, and ordinals. Relative hereditary definability gives $N\models\ZF$, $X\in N$, and $\HOD^C\sq N$. \smallskip\noindent \emph{Descent to the original external HOD.} Finite permutations of $\omega$ witness weak homogeneity of the collapse. If $\pi$ is such a permutation, the real coding $e\circ\pi$ is Turing equivalent to $r$. Consequently \[ \HYP(r_{e\circ\pi})=\HYP(r_e), \qquad F(\HYP(r_{e\circ\pi}))=F(\HYP(r_e)). \] Both equalities are evaluated in $U[e]$, which is also $U[e\circ\pi]$. The class $C$ and the parameters $X$ and $x\in X$ are therefore fixed by these recodings. Induct on hereditary rank to show $N\sq H$. If $y\in N$ and all members of $y$ have already descended to $U$, then $y$ is a subset of a ground rank $V_\beta^U$. Choose a relative-HOD definition of $y$ over $C$, evaluated at a sufficiently large set-sized rank. The formula uses $X$, finitely many elements of $X$, and ordinals. The preceding invariance and weak homogeneity make its membership decisions independent of the collapse condition. The forcing relation defines $y$ in $U$ from these same parameters. Since $X$ is OD in $U$ and its finitely many specified elements belong to $H$, their ordinal-sequence definitions can be combined into a single ordinal-sequence parameter. Hence $y$ is definable in $U$ from an allowed parameter. The induction hypothesis supplies the hereditary requirement, proving $y\in H$. Transitivity and $X\in N\sq H$ now give \[ V_\lambda^N=X=V_\lambda^H, \qquad V_\alpha^N=V_\alpha^H. \] \smallskip\noindent \emph{Small violations of choice and dependent choice.} The bounded evaluation map for relative-OD definitions gives $\SVC(X)$ in $N$. To spell out its parameter bound, fix a nonempty $Y\in N$ and a member $y_*\in Y$. Collection in $C$ bounds ranks witnessing relative-OD definitions of all members of $Y$. Formula codes, stage ordinals, and ordinal parameters are absorbed into an ordinal $\eta$. Finite tuples of elements of $X$ can be coded by elements of $X$. Thus an evaluation map in $N$ gives a surjection \[ f:\eta\times X\twoheadrightarrow Y. \] Send invalid codes to $y_*$. The graph is relatively OD in $C$ from $Y$, $y_*$, $X$, and the ordinal bounds, and all its hereditary constituents belong to $N$. Thus $f\in N$. This does not choose a wellordering of $X$. Let $R\in N$ be a serial relation on a nonempty set $Y\in N$, and fix $y_0\in Y$. Use such a surjection $f$. In $U$, having chosen $y_n$, take the least $\xi_n<\eta$ such that \[ \exists x\in X\quad y_n\mathrel R f(\xi_n,x), \] choose one such $x_n$ using choice in $U$, and put $y_{n+1}=f(\xi_n,x_n)$. All these operations take place in $U$, since $R,Y,f\in N\sq U$. By \eqref{wd-X-closure}, the whole sequence $\seq{x_n:n<\omega}$ belongs to $X$, and hence to $N$. Inside $N$, reconstruct the $y_n$ by recursion using this sequence, $y_0$, $f$, $R$, and the least-ordinal rule. Its defining quantifiers range over the same sets in $N$ and $U$, so the reconstruction gives exactly the chosen chain. This proves $\DC$ in $N$. No bound on $\eta$ by $\lambda$ is needed. \smallskip\noindent \emph{The Woodin ground.} Set $D=\HOD^C$. Theorem~\ref{wd-envelope} gives a set forcing $P\in D$ and a $D$-generic $h$ such that \[ D\sq N\sq C=D[h]. \] Let $\tau=|P|^D$. Every sufficiently high Woodin of $C$, in particular each above the small-forcing bound, is already Woodin in $D$ by \cite{HamkinsWoodin}. Thus $D\models\ZFC+\PCW$. Since $N\models\ZF+\SVC$, the symmetric-intermediate theorem \cite[Corollary~5.10]{Usuba} implies that $N$ is a symmetric extension of $D$. Its set-forcing presentation is supplied by \cite[Proposition~4.4]{Usuba}. The presenting forcing need not be the particular $P$ used above. This is sufficient for the claimed existence of a set-symmetric presentation. \end{proof} \section{Woodin realization by set forcing}\label{sec:wd-realization} Write $\PCW$ for the assertion that the Woodin cardinals form a proper class. For a rank-restricted conclusion, recognizing an entire choice envelope is unnecessary. We shall recognize enough of that envelope to evaluate the capped-history predicate of Theorem~\ref{thm:spectrum}. This permits a construction using only set forcing over the original Woodin ground. \subsection{Keeping the original symmetric ground} \begin{lemma}[The old-ground version of local transfer] \label{wd-old-ground-transfer} Suppose $D\models\ZFC+\PCW$, and $N$ is a set-symmetric extension of $D$ satisfying $\ZF+\DC$. Given an ordinal $\alpha$, there are models and sets \[ D\subseteq N\subseteq M=D(A)\subseteq B=M[K]=D[b] \] such that \begin{enumerate} \item $V_\alpha^M=V_\alpha^N$ and $M\models\ZF+\DC+\SVC$; \item $A\subseteq\mu^\omega$ for some ordinal $\mu$; \item $B\models\ZFC+\PCW$, and $B/M$ is weakly homogeneous and adds no ordinal $\omega$-sequences; \item $B=D[b]$ is an ordinary set-forcing extension of this same $D$. \end{enumerate} There is no large-cardinal hypothesis on $N$ in this statement. \end{lemma} \begin{proof} Fix a symmetric presentation $D\subseteq N\subseteq E_0=D[G]$, with forcing $T\in D$. By \cite[Lemma~4.1 and Proposition~5.4]{Usuba}, there is $z\in N$ with $N=D(z)$, and $N$ satisfies SVC. Fix an SVC witness $S\in N$. The ground is already given; the measurable capture argument in Proposition~\ref{prop:coretransfer} is not needed. Choose an uncountable regular $D$-cardinal $\vartheta>|T|^D$ above the presentation bounds. Choose a sufficiently large ground beth fixed point $\lambda>\alpha$ of $D$-cofinality $\vartheta$, with $z,S\in V_\lambda^N$, and put $X=V_\lambda^N$. The small forcing $T$ preserves this cofinality. The old cofinal sequence belongs to $N$, and the full cover has no shorter one, so $\cf^N(\lambda)=\vartheta>\omega$. The transitive-base convention gives $N=D(X)$, and extending each SVC surjection by a default value gives $N\models\SVC(X)$. A Woodin cardinal is a limit of measurable cardinals, so $D$ has arbitrarily large measurable cardinals. After bounding the ground names for $X$ and the old collapse below, choose a $D$-measurable $\kappa>\lambda+\omega$ above these bounds. Fix a normal $D$-measure $\UU$ on $\kappa$. Let $\pp_\UU^D$ be the old Prikry poset and let \[ \cc_0=\{k:k\text{ is an }N\text{-countable partial function } \omega_1^N\longrightarrow X\}^{N}. \] Both the presentation and $\cc_0$ have size below $\kappa$ in the full cover. Take $(c,K_0)$ generic for the fixed product $\pp_\UU^D\times\cc_0$ over $E_0$, and set \[ W=N[K_0][c]=N[c][K_0],\qquad E=E_0[K_0][c]. \] Here the use of the old measure is essential. In each small choice cover $Y$ of $D$, the normal generated lift is \[ \UU_Y=\{a\in\Pow(\kappa)^Y: \exists u\in\UU\ (u\subseteq a)\}. \] Every tail in $\UU_Y$ contains an old tail, so $\pp_\UU^D$ is dense in the Prikry forcing recomputed from $\UU_Y$ in $Y$. We do not require $\UU$ itself to measure all the new subsets of $\kappa$ in $N$. In $N$, DC makes $\cc_0$ countably closed. Its generic union enumerates $X$; SVC then wellorders every old set and every set of names. Hence $N[K_0]\models\ZFC$. The generated measure in $E_0[K_0]$ restricts to the normal measure defined by the same ground-witness formula in $N[K_0]$. Product genericity makes $c$ Prikry generic over this choice model, so $W\models\ZFC$. These are exactly the hypotheses of Section~\ref{sec:ambient}. In particular Lemma~\ref{lem:ambientfacts} gives \[ {}^\omega X\cap W={}^\omega X\cap N, \qquad V_\kappa^{N[c]}=V_\kappa^N, \] and gives an $N$-wellorderable cover for every $W$-countable family of $N$-elements. The countable closure is used before adjoining $c$; closure of the old collapse after adjoining $c$ is not assumed. The old initial-segment collapse projects onto the labeling forcing of Section~\ref{sec:caps}. Let $g$ be its projected generic. The finite interpolation, paired lifting and literal comparison lemmas give $Q=Q(c,g)$ and $F=F(c,g):Q\twoheadrightarrow X$. Put $M=N(Q,F)$. Lemma~\ref{lem:eliminate} and Corollary~\ref{cor:rankpres} give $V_\lambda^M=X$; Lemmas~\ref{lem:CD} and~\ref{lem:DCM} give DC in $M$. These results use the old countable arrays and the facts just verified, rather than a measure belonging to $N$. For clarity, the SVC and seed conclusions can also be read directly from the proof of Proposition~\ref{prop:seed}. Bounded presentations and the surjection onto $X$ give surjections $\xi\times Q^{<\omega}\twoheadrightarrow Y$ for every nonempty $Y\in M$, so $Q^{<\omega}$ witnesses SVC. Code $Q$ and the relation \[ R(p,q)\quad\Longleftrightarrow\quad F(p)\in F(q) \] by differently tagged ordinal $\omega$-sequences. Equality of predecessor sets is equality of $F$-values. The quotient relation's unique Mostowski collapse recovers the literal $X$ and $F$. Thus the resulting $A\subseteq\mu^\omega$ satisfies $M=D(A)$. No measurable-tail conclusion about $M$ is needed here. Apply Lemma~\ref{lem:envelope} to $M$, taking its fresh generic $K$ over the full choice cover $E$ as well. Then $B=M[K]$ is a weakly homogeneous choice extension with no new ordinal $\omega$-sequences. Moreover \[ D\subseteq B\subseteq E[K]. \] The outer model $E[K]$ is a set-forcing extension of $D$: the posets defined in intermediate models have ground names. Since $D$ and $B$ satisfy ZFC, the ordinary intermediate-model theorem gives a set forcing $P\in D$ and a $D$-generic $b$ with $B=D[b]$; see \cite{Grigorieff}. Small forcing preserves Woodinness \cite{HamkinsWoodin}. Every $D$-Woodin above $|P|^D$ therefore survives in $B$, proving $B\models\PCW$. \end{proof} \subsection{One bounded homogeneous ordinal code} \begin{lemma}[Bounded homogeneous coding]\label{wd-bounded-code} Let $W\models\ZFC$ have a proper class of inaccessible cardinals, let $d\subseteq\delta$ be a set of ordinals, and let $\beta$ be an ordinal. There is a weakly homogeneous set forcing, uniformly defined from $d,\delta$ and an ordinal bound $b$, which preserves $V_\beta^W$, adds no ordinal $\omega$-sequences, and makes $d$ ordinal definable. No GCH hypothesis is required. \end{lemma} \begin{proof} If $\delta=0$, use trivial forcing. Assume $\delta>0$. Choose $b>\beta,\delta,\omega$ with $|V_\beta^W|\rho+\omega$. There is one such bound because the candidate family and schedule have set size. Agreement above $\rho+\omega$ includes all bounded witnesses to cardinality, cofinality and the strong-limit tests below $\rho$; thus no earlier inaccessible is introduced in the schedule computed in $C$. The complete Boolean algebras and the indicated name systems are computed identically. Every $B$-dense subset of $Q_e$ belongs to $C$, and every $C$-dense subset is a $B$-dense subset of the same poset. Hence $C$-genericity and $B$-genericity of $h$ are equivalent. For such an $h$ we have $C[h]\subseteq B[h]$. Absolute evaluation of the names in $T_e$, together with \eqref{eq:wd-cap-names}, gives equality of the two recomputed cap posets. In the convention $\Add(\rho,1)=2^{<\rho}$, membership is absolute for a sequence already present in the smaller model. In fact the full power sets of these cap posets agree. Given $Z\subseteq\Add(\rho,1)^{B[h]}$ in $B[h]$, form \[ Y=\{t\in T_e:t^h\in Z\}. \] Some member of $\mathcal N_e$ evaluates to $Y$. That name belongs to $C$, so $Y\in C[h]$, and evaluating its members reconstructs $Z$ inside $C[h]$. The opposite inclusion follows from $C[h]\subseteq B[h]$. Therefore the two models have exactly the same dense subsets of the common cap poset. Genericity of any outer filter $k$ is equivalent over them, proving the lemma. \end{proof} \begin{lemma}[A sufficient ground fragment]\label{wd-ground-fragment} Suppose $D\subseteq M=D(A)\subseteq B=D[b]$, where $D,B$ satisfy ZFC and $b$ is generic for a set forcing $P\in D$. Fix ordinals $\alpha,\chi,\eta$, with $P,b\in V_\eta^B$. There is $\theta$ such that \begin{enumerate} \item every element of $V_\chi^B$ is the value of a $P$-name in $V_\theta^D$; \item $V_\alpha^M\subseteq L(V_\theta^D,A)$. \end{enumerate} Here and below $L$ with set arguments denotes transitive-base constructibility, including all members of its arguments. \end{lemma} \begin{proof} The bounded-rank name lemma supplies the first bound. One can obtain it by recursion in $D$, using at successor stages all Boolean names whose possible members are in the preceding name set, and taking unions at limits. Their evaluations cover the corresponding ranks in every generic extension. Equivalently, in $B$ choose a ground name for each element of the set $V_\chi^B$ and bound their ranks. The ground $D$ is definable in its set extension from a set parameter; the chosen collection need not itself belong to $D$ for its ordinal rank bound to do so. For the second bound, use the convention and bounded-witness argument of Lemma~\ref{lem:presentation}. Each $y\in V_\alpha^M$ belongs to a set-sized construction level over $\TC(\{V_\xi^D,A\})$ for some $\xi$. Collection in $B$ bounds the ground ranks $\xi$ needed for the set $V_\alpha^M$. Increase $\theta$ past this bound and the name bound. The inner model $L(V_\theta^D,A)$ contains every one of the indicated levels: recursion through the definable-subset operation on set structures is absolute. This proves the second inclusion without claiming that an arbitrary directed union of inner models satisfies ZF. \end{proof} \subsection{Realizing the protected rank} \begin{theorem}[Woodin rank realization]\label{wd-set-realization} Let $D\models\ZFC+\PCW$, let $N$ be a set-symmetric extension of $D$ satisfying $\ZF+\DC$, and let $\alpha$ be an ordinal. In a common outer universe there is an ordinary set-forcing extension $U$ of $D$ such that \[ U\models\ZFC+\PCW, \qquad V_\alpha^{\Hseq^U}=V_\alpha^N. \] In particular, a rank sentence true in such a symmetric extension is true in the corresponding rank of external $\HOD_{\Ord^\omega}$ in a model of $\ZFC+\PCW$. \end{theorem} \begin{proof} Apply Lemma~\ref{wd-old-ground-transfer}. We obtain \[ D\subseteq N\subseteq M=D(A)\subseteq B=M[K]=D[b], \qquad V_\alpha^M=V_\alpha^N, \] with $A\subseteq\mu^\omega$ and the stated homogeneous sequence-preserving envelope. Fix its forcing presentation $P\in D$ and choose $\eta$ with $A,K,P,b\in V_\eta^B$. Choose an infinite $\tau$ large enough to code $(\TC(\{A\}),\in,A)$, and let $F_A\subseteq2^\tau$ be the family of all its pointed well-founded extensional presentations, with domain, root and unused-position data as in Corollary~\ref{cor:ODcoding}. This family is defined from $A,\tau$; no presentation is selected. Apply Theorem~\ref{thm:spectrum} over $B$, placing the first site above a regular bound greater than $|V_\eta^B|$. With its universal schedule and cap $\rho$, use the actual forcing \[ S=P_{F_A}= \prod_{e\in F_A}^{\mathrm{full}} \bigl(Q_e*\dot{\Add}(\rho,1)^{B[\dot h_e]}\bigr), \qquad U_0=B[G_S]. \] The terminal forcing is recomputed in its own row extension. The extension retains the evaluated row and cap generics; the larger raw termspace generics are not adjoined. Theorem~\ref{thm:spectrum} gives the spectrum $F_A$, weak homogeneity and preservation of $V_\eta^B$. Since $U_0$ is a set extension of $D$, it still has a proper class of Woodins, and hence of inaccessibles. Next choose $\chi>\eta+\omega$ satisfying Lemma~\ref{wd-bounded-history}, and choose $\theta$ by Lemma~\ref{wd-ground-fragment}. In $D$, code the transitive set $V_\theta^D$ by a set of ordinals $d\subseteq\delta$. Include domain and root information in its well-founded extensional presentation. The code $d$ belongs to $D$, hence to $M$, regardless of how these ordinal bounds were selected. In $U_0$ choose a rank bound $\zeta$ above $\eta$ and all possible capped-history witnesses for this schedule. Such a bound depends only on the set family of lower posets and on $\rho$: a lower filter is a subset of some $Q_e$, and a cap filter is a subset of $2^{<\rho}$. It bounds the ranks of all potential witnesses, not just of the generics originally planted by $S$. Enlarge it to include the candidate codes. Apply Lemma~\ref{wd-bounded-code} over $U_0$ to $d$, preserving $V_\zeta^{U_0}$, and call the resulting extension $U$. We now define the decoder inside $U$. The set $d$ is OD, and $V_\eta^U=V_\eta^B$. Thus the class \begin{equation}\label{eq:wd-envelope-cut} C=L(d,V_\eta^U) \end{equation} is definable from ordinal parameters in $U$. Its bases are sets of $B$, so the absolute transitive-base construction gives $C\subseteq B$. Decoding $d$ puts $V_\theta^D$ in $C$; the second base contains $P,b$. Evaluation of the names in Lemma~\ref{wd-ground-fragment} therefore gives \[ V_\chi^C=V_\chi^B. \] A $B$-wellordering of $V_\eta^B$ has rank below $\chi$ after the stipulated increase of $\chi$, and hence belongs to $C$. Together with the ordinal-set code $d$, it wellorders the transitive base of \eqref{eq:wd-envelope-cut}. Consequently $C\models\ZFC$. Lemma~\ref{wd-bounded-history} identifies the history predicate relative to $C$ with the predicate relative to $B$. The last forcing preserved every possible history witness and changed neither $C$ nor its ground-name and dense-set families. Thus in $U$ the spectrum of histories relative to the definable class $C$ is exactly $F_A$. Taking the pointed Mostowski collapse of any member recovers $A$ and makes $A$ OD in $U$. We have transferred a bounded predicate; we have not reapplied Theorem~\ref{thm:spectrum} to $C$, which need not have a proper class of inaccessible cardinals. Put $H=\Hseq^U$. The forcing from $M$ to $U$ is weakly homogeneous. The spectrum name is uniformly defined from the old $A$ and ordinals, and the final code name is uniformly defined from the old $d$ and ordinals. Earlier automorphisms therefore send each name to a forced equal name and lift to the iteration. The local Boolean-mixing argument in the proof of Proposition~\ref{prop:secure-realize} combines these automorphisms: a locally forced automorphism is given the identity value off its Boolean cone. This uses no global maximum principle over the choiceless $M$ and introduces no wellorder from the choice envelope as a parameter. The first stage adds no ordinal $\omega$-sequences, and both later stages are highly distributive. Lemma~\ref{lem:homdesc} gives $H\subseteq M$. Conversely, the ordinal code $d\in\HOD^U$ and its unique Mostowski collapse put $V_\theta^D$, with all its hereditary elements, in $H$. Also $A\in H$: it is OD and each of its members is an allowed ordinal $\omega$-sequence. Since $H\models\ZF$ by Lemma~\ref{lem:HDC}, it contains $L(V_\theta^D,A)$. Hence \[ V_\alpha^M\subseteq L(V_\theta^D,A) \subseteq H\subseteq M, \] which proves the required rank equality. The definability of $C$ places none of the extra choice wellorderings of $B$ in $H$. In particular $V_\eta^U$ is used as an OD set defining a class, not as a hereditarily OD parameter. This is the distinction of Remark~\ref{rem:ODnotHOD}. The object coded hereditarily is the ground fragment $V_\theta^D$, not the envelope rank $V_\chi^B$. Finally, $U/D$ is a composition of set forcings. Every sufficiently high ground Woodin survives by small-forcing preservation \cite{HamkinsWoodin}. Thus $U\models\ZFC+\PCW$. The bounds were chosen in the order \[ \eta,\quad S\text{ and }\rho,\quad\chi,\quad \theta\text{ and }d,\quad\zeta,\quad \text{the last coding block}. \] There is no demand that $S$ preserve $V_\theta^B$: the ground fragment is recovered from $d$. All preparation and coding in this proof are set forcing, and no conclusion that $N$ or $M$ has Woodin cardinals is used. \end{proof} \section{GCH realization as a symmetric ground}\label{wd-exact-section} We now strengthen the consistency conclusion by using the special ground produced in Proposition~\ref{wd-reverse}. The additional hypotheses on that ground allow a bounded GCH-preserving code to identify all its sets inside the final HOD. We then recover the sequence-generated model exactly and exhibit the ambient universe as its set-forcing extension. \subsection{The normalized choice ground} The reverse construction supplies more structure than is needed for Theorem~\ref{wd-set-realization}. We use that structure to obtain global GCH and to identify the entire external HOD. \begin{lemma}[Properties of the normalized ground] \label{wd-normalized-ground} Let $D\subseteq N$ be the models constructed in Proposition~\ref{wd-reverse}, and let $C$ be its canonical choice envelope, so that \[ D=\HOD^C,\qquad D\subseteq N\subseteq C=D[h]. \] Then $D$ satisfies eventual GCH, and there is a set of ordinals $t\in D$ such that \[ D=\HOD_{\{t\}}^D. \] Every set-forcing extension of $D$ satisfies eventual GCH. \end{lemma} \begin{proof} The model $C$ supplied by Theorem~\ref{wd-envelope} is an acceptable relative pure-extender premouse over a bounded self-wellordered base. In either branch of that construction, the usual acceptability calculation applies above the size and height of the base. Subsets of an infinite cardinal $\kappa$ occur below $J_{\kappa^+}$, and the standard surjections from the base times $\kappa$ bound the earlier levels by $\kappa$. Thus $C$ satisfies GCH above a fixed bound; compare \cite[Section~2.2]{SteelOutline}. Fix a forcing presentation $C=D[h]$ by $T\in D$. Above $|T|^D$, the relevant cardinals are preserved. If GCH failed in $D$ at an arbitrarily large cardinal $\kappa$, its old subsets of $\kappa$ would still contradict GCH in $C$. Hence $D$ satisfies eventual GCH. Conversely, for any fixed set forcing $P\in D$ and every sufficiently large cardinal $\kappa$, names for subsets of $\kappa$ can be coded by subsets of $\kappa\times P$. When GCH holds in $D$ there, this bounds their number by $(\kappa^+)^D$, which the forcing preserves. The old subsets give the opposite inequality. This proves eventual GCH in every set extension of $D$. Replace $T$ by an ordinal-coded presentation in $D$, and let $t$ be one ordinal-set code for its domain and order. If $x\in D$, then $x$ is ordinal definable in $C$. There are a formula $\varphi$, a finite tuple of ordinals $\vec\xi$, and $p\in h$ such that \[ p\forces_T \text{``$\check x$ is the unique $y$ satisfying $\varphi(y,\check{\vec\xi})$''}. \] Inside $D$, the set $x$ is therefore the unique $y$ for which $p\forces_T\varphi(\check y,\check{\vec\xi})$. The forcing relation is definable in $D$ from $T$, and $p$ is represented by an ordinal. Thus $x$ is definable over $D$ from $t$ and ordinals. The same argument applies to every member of its transitive closure, proving $D=\HOD_{\{t\}}^D$. \end{proof} \subsection{Bounded coding while preserving GCH} \label{wd3-bounded-coding-section} The continuum code of Lemma~\ref{wd-bounded-code} can be replaced, over a GCH model, by a code in the $\diamondsuit^*$ pattern. We need a bounded set product whose definition uses only the set being coded and ordinal parameters. We also need its actual closure, rather than only distributivity, for the ground-recognition argument. \begin{lemma}[Bounded GCH-preserving coding]\label{wd-gch-bounded-code} Let $W\models\ZFC+\GCH$ have a proper class of inaccessible cardinals. Suppose $d\sq\delta$, and let $\beta,\chi$ be ordinals. For every sufficiently large ordinal $b$ there is a set forcing $R(d,\delta,b)$, uniformly defined from these three parameters, which is locally homogeneous and $<\chi$-closed. It preserves all cardinals, GCH, the class of inaccessible cardinals, and $V_\beta^W$, adds no ordinal $\omega$-sequences, and makes $d$ ordinal definable from $b,\delta$. \end{lemma} \begin{proof} If $\delta=0$, use trivial forcing. Otherwise take \[ b>\delta,\beta,\chi,\omega,|V_\beta^W|, \] and let $\seq{\kappa_i:i<\delta}$ enumerate the first $\delta$ inaccessible cardinals above $b$. Put \[ \lambda_i=\kappa_i^{+++}. \] Until an extension is specified, all posets and cardinal calculations in this proof are computed in $W$. In particular $\delta<\kappa_0$. We first specify the two possible factors at an infinite successor cardinal $\lambda=\theta^+$. For the positive factor $P_\lambda$, use pairs $(X,\xi)$ with \[ \varnothing\ne X\sq{}^\lambda2, \qquad |X|\leq\theta, \qquad \xi<\lambda, \] and a separate largest condition. Declare $(Y,\zeta)\leq(X,\xi)$ if $Y\supseteq X$, $\zeta\geq\xi$, and \[ \forall f\in Y\ \exists g\in X\quad f\restr\xi=g\restr\xi. \] The nonempty-branch convention is part of this presentation. An empty branch set would give a degenerate component under the displayed order and is excluded. This is the positive coding forcing of \cite[Section~2]{BrookeTaylorCoding}. It forces $\diamondsuit^+_\lambda$, and hence $\diamondsuit^*_\lambda$. The relevant feature of its proof is that the generic tree captures every old binary $\lambda$-sequence up to a bounded modification. Indeed, below any nonempty condition, alter the initial part of a given sequence to match a represented node and then add that branch. Nice names for new binary $\lambda$-sequences use only $\lambda$ many conditions and branches, so they have old binary $\lambda$-sequence codes. The tree recovers the generic filter. Together with a code for the old $\Pow(\theta)$, these facts give the hypothesis of the positive coding theorem in \cite[Section~2]{BrookeTaylorCoding}. That argument uses only the nonempty component specified here. The negative factor is $Q_\lambda=\Add(\lambda,\lambda^+)$, which forces $\neg\diamondsuit^*_\lambda$; see \cite[Appendix, Lemma~18]{CFH}. Both factors are $<\lambda$-closed, have size $\lambda^+$, and satisfy the $\lambda^+$-chain condition under GCH. For $P_\lambda$, unions of increasing branch sets and suprema of heights give the closure. At each fixed height $\xi<\lambda$ there are at most $\lambda$ possible sets of at most $\theta$ binary $\xi$-prefixes. Conditions with the same prefix set are compatible by taking the union of their branch sets. This proves its chain condition. The size bound follows from $(2^\lambda)^\theta=2^\lambda=\lambda^+$. The usual Cohen calculation gives the same bounds for $Q_\lambda$. For either factor, closure, the chain condition, and nice-name counting preserve all cardinals and GCH. Define \[ R_i= \begin{cases} P_{\lambda_i},&i\in d,\\ Q_{\lambda_i},&i\notin d, \end{cases} \qquad R(d,\delta,b)=\prod_{i<\delta}R_i, \] using full support and the old factors. The product is $<\lambda_0$-closed by coordinatewise lower bounds in $W$. Since $\lambda_0>b>\chi,|V_\beta^W|$, it is $<\chi$-closed, adds no ordinal $\omega$-sequences, and preserves $V_\beta^W$. For the rank assertion, a first new set below that rank would be a new subset of an old set of size $<\lambda_0$, contrary to closure and Choice in $W$. \smallskip\noindent \emph{Local homogeneity.} Given two nontrivial conditions in $P_\lambda$, extend both distinguished branch sets to have size $\theta$. Choose a common height $\gamma<\lambda$ above their heights which separates every pair of distinct branches in either set. Match their $\theta$ many nodes at height $\gamma$ bijectively, together with the unique distinguished branch through each node. Within each matched pair of binary cones, replace the prefix and translate the tail by coordinatewise addition modulo two so that the distinguished branches correspond. The resulting map preserves equality of initial segments at every height at least $\gamma$. Applied to branch sets, it is an isomorphism between the two forcing cones below the strengthened conditions. Thus $P_\lambda$ is locally homogeneous. The Cohen factor $Q_\lambda$ is weakly homogeneous. Choice in $W$ combines the component cone isomorphisms into a cone isomorphism for the full product. This proves the required local homogeneity. \smallskip\noindent \emph{Factorization estimates.} For each $i<\delta$, the product below $i$ has size $<\kappa_i$. Its number of coordinates is less than $\kappa_i$, and regularity bounds their sizes below $\kappa_i$. The strong-limit property then bounds the full product below $\kappa_i$. Consequently the product through $i$ has size at most $\lambda_i^+$ and is $\lambda_i^+$-cc. To verify the latter claim, an antichain of size $\lambda_i^+$ could be thinned to have the same lower-product coordinate, contradicting the chain condition of $R_i$. If a tail remains after $i$, it is $<\lambda_{i+1}$-closed in $W$. The prefix has size $<\lambda_{i+1}$. Easton's lemma \cite[Fact~5.10]{CummingsForcing} makes this fixed old tail $<\lambda_{i+1}$-distributive over the prefix extension. Thus it adds no subsets to the cardinals at or immediately above $\lambda_i$. This use of distributivity does not require the old tail to remain closed in the intermediate model. \smallskip\noindent \emph{Cardinals and GCH.} At an active site $\lambda_i$, the preceding size and chain condition bounds give at most \[ (\lambda_i^+)^{\lambda_i}=\lambda_i^+ \] nice prefix names for subsets of $\lambda_i$. At its successor and at larger cardinals above that prefix's size, a subset name is coded by a subset of the product of the domain cardinal with the forcing. Ground GCH gives the corresponding successor bound. Upper-tail distributivity transfers these calculations to the full extension. At cardinals below the active site, one may instead force with $R_i$ first and then with the small lower product. These factors commute, the first preserves GCH, and the second preserves the continuum function above its size by the same name count. This also handles the gaps between a completed prefix and the next active site. We give the limit calculation separately. Suppose \[ \mu=\sup_{i\mu^+$, and the remaining tail is distributive beyond $\mu^+$ after this prefix. The earlier factorization calculations preserve all cardinals below $\mu$, so $\mu$ remains a cardinal. Its old short cofinal sequence shows that it remains singular. If the old $\mu^+$ ceased to be regular, its new cofinality would be a regular cardinal $\nu<\mu$. Choose $i\mu$; that every real is constructible; that $\lambda=\omega_1^L$ and $\mu=\omega_2^L$; and that $\Pow(\lambda)$ is not wellorderable. These are combined into one first-order sentence, with $\lambda,\mu,\nu$ existentially quantified. Suppose $V_\theta^W\models\sigma_0$, where $W\models\ZF$. The first clause makes $\theta$ a limit, and the guard gives $\theta>\mu+\omega$. All functions between ordinals at most $\mu$, and all subsets and binary relations on $\Pow(\lambda)$, belong to this rank whenever they belong to $W$. Thus its $\omega_1$ and $\omega_2$ are those of $W$, and its nonwellorderability assertion remains true in $W$. The local constructible hierarchy agrees with the actual one at every level below $\theta$. To verify this, code finite assignments by finite function graphs: the satisfaction relation for a set structure and a hierarchy sequence through a fixed level require only a fixed finite increase in rank. All such witnesses remain below the limit $\theta$. In particular, every real of $W$ is constructible. It remains to check the second constructible cardinal. Equality of reals gives $\lambda=\omega_1^L$ globally, and inner-model cardinal comparison gives $\gamma=\omega_2^L\leq\mu=\omega_2^W$. If $\gamma<\mu$, then $\gamma$ is also a cardinal of the rank's local $L$: a local constructible bijection collapsing it would be a global constructible bijection. This puts an $L$-cardinal strictly between the asserted first and second uncountable $L$-cardinals, a contradiction. Therefore $W\models A_L$. If $W=\Hseq^U$ for a choice universe $U$, Lemma~\ref{lem:constructible-sequences} gives Choice in $W$, contradicting the retained nonwellorderability assertion. On the other hand, the symmetric model $N$ satisfies $\sigma_0$ globally, so reflection gives a rank satisfying it. This is a formal relative-consistency construction; no transitive-model assumption is required. \end{proof} The same sentence gives a rank-conservativity obstruction: $\ZF+\KW$ proves that no rank satisfies $\sigma_0$, while $\ZF+\DC$ does not, assuming consistency. This proves that CM cannot be deleted from the stated theorem. It does not identify the weakest sufficient large-cardinal hypothesis. \section{A Ramsey obstruction}\label{app:ramsey} Let $\mathsf{CR}$ assert that the cardinals $\rho$ satisfying $\rho\longrightarrow(\rho)^{<\omega}_2$ are unbounded in the ordinals, and put $T_{\mathrm R}=\ZF+\DC+\mathsf{CR}$. In this section $\mathbb R=\Pow(\omega)$. The three sorts of arithmetic are $\omega$, $\mathbb R$, and $\Pow(\mathbb R)$. A $\Pi^2_3$ sentence has three alternating blocks of third-sort quantifiers, beginning universally, followed by a matrix with only number and real quantifiers. Finite tuples of third-sort variables may be combined by fixed recursive tags. \begin{theorem}[Ramsey obstruction]\label{thm:ramsey-obstruction} There is a parameter-free $\Pi^2_3$ sentence $\Phi$ such that \[ T_{\mathrm R}+\KW\vdash\Phi, \qquad \Con(\ZFC+\mathsf{CR}) \ \Longrightarrow\ \Con(T_{\mathrm R}+\neg\Phi). \] Consequently, relative to $\Con(\ZFC+\mathsf{CR})$, adding $\KW$ is not conservative over $T_{\mathrm R}$ for third-order arithmetic. The same example gives a structural $\Pi_2$ assertion separating these theories. \end{theorem} We use the classical Dodd--Jensen core model. In a choiceless universe $W$, set $K=(K^{\mathrm{DJ}})^{\HOD^W}$. The semantic form of the separating implication is \begin{equation}\label{eq:ramsey-semantic} \bigl[\neg\exists0^\dagger\ \wedge\ \mathbb R=\mathbb R^K\ \wedge\ \omega_2=\omega_2^K\bigr] \ \longrightarrow\ \mathsf{Fodor}(\omega_1). \end{equation} We first prove this implication with $\KW$, then give its third-order formulation and a countermodel. \begin{proof} \emph{The covering implication.} Under $\mathsf{CR}$, absence of $0^\dagger$ excludes an inner model with a measurable. Indeed, from such an inner model obtain its canonical $L[U]$, with measurable $\kappa$. Its wellordering gives an ordinal code $A\subseteq\alpha$ for the transitive closure of $U$, where $\alpha>\kappa$, $A\in L[U]$, and $L[A]=L[U]$. A Ramsey above $\alpha+\omega$ supplies indiscernibles for $L[A]$. Shifting above $\alpha$ gives a nontrivial self-embedding of $L[U]$ with critical point above $\kappa$, which implies $0^\dagger$. Here the relativized indiscernibles argument is applied to canonical structures with definable Skolem functions; it is available in ZF \cite[Propositions 7--8]{ApterKoepke} \cite[p.~262]{MitchellRamsey}. The last implication is the standard nonrigidity characterization of $0^\dagger$ \cite{CompleatDagger}. The possibly uncountable parameter sharp is not itself being identified with a real. Assume the antecedent of \eqref{eq:ramsey-semantic}, and fix $s\in(\Ord^\omega)^W$. Code its graph by a set of ordinals $\bar s$. Apter--Koepke's adjoining construction gives \[ C=(\HOD^W)[\bar s]\models\ZFC,\qquad K\subseteq C\subseteq W,\qquad K^{\mathrm{DJ},C}=K \] with $s\in C$ \cite[Proposition 9]{ApterKoepke}. The endpoint agreements give common $\omega_1$ and $\omega_2$ in these three models. Apply strong Dodd--Jensen covering inside $C$ to $\operatorname{ran}(s)\cup\omega_1$ \cite[Theorem 1.2]{MitchellCovering}. It has a cover $y\in K$ with $|y|^C=\omega_1$. Correct $\omega_2$ implies $|y|^K\leq\omega_1$. For a $K$-surjection $e:\omega_1\to y$, the sequence of least $e$-indices of the values of $s$ is bounded in $\omega_1$ in $C$. A $K$-enumeration of a countable bound codes that sequence by a real. The real belongs to $K$, so $s\in K$. Thus $(\xi^\omega)^W=(\xi^\omega)^K$ for every ordinal $\xi$. Each of these spaces has a $K$-wellordering. Under $\KW$, least preimages under a sequence-space surjection wellorder every nonempty set. Hence AC, and therefore Fodor's lemma, follows. \emph{The third-order formula.} Use the classical one-measure lower-part presentation of $K$ \cite[Section 3]{BenNeriaLuecke}. Countable mousehood has a projective definition, and the corresponding countable-hull tests use only real codes \cite[Lemma 3.32 and p.~92]{MitchellCovering}. For $A\subseteq\mathbb R$, a certificate for $\operatorname{KSet}(A)$ consists of a wellordered real domain, a well-founded extensional premouse relation on it, its measure predicate and satisfaction relation, actual-real labels, and a distinguished lower-part node whose elements are exactly $A$. Require every real-coded countable elementary hull to collapse to an iterable classical premouse. Also allow a constructible level certificate. The domain wellorder makes the entire labelled certificate ordinal-codable. In the choice model obtained by adjoining that code to HOD, the countable-hull copying criterion gives iterability, and Proposition 9 of \cite{ApterKoepke} identifies the core with $K$. This proves soundness. For completeness under $\mathbb R=\mathbb R^K$, choose the witness inside $K$, with both $\mathbb R^K$ and $A$ in its lower part. A canonical hull containing every real and these two nodes has size at most $\omega_1$ and its collapse fixes $A$. The small-mouse argument in the proof of \cite[Lemma 3.1]{BenNeriaLuecke}, applied inside $K$ at $\omega_2^K$, also gives this witness directly. CH in $K$ supplies a real-domain code. Equality of reals preserves its countable-hull tests. Consequently \[ \mathbb R=\mathbb R^K \quad\Longrightarrow\quad \bigl(\operatorname{KSet}(A)\longleftrightarrow A\in K\bigr). \] Under DC, a relation on a real domain is well-founded exactly when it has no real-coded descending omega-sequence. All the certificate conditions therefore have a second-order matrix after one existential third-sort quantifier: $\operatorname{KSet}(A)\equiv\exists P\,k(A,P)$. Let $\operatorname{CopyK}$ say that every wellorder on a subset of the reals has an isomorphic real-domain wellorder with such a core certificate. Bundling the copy, certificate and isomorphism gives \[ \operatorname{CopyK}\equiv\forall E\,\exists P\,c(E,P), \] where $c$ is second-order; malformed inputs permit a dummy certificate. On $\mathbb R=\mathbb R^K$, this is equivalent to $\omega_2=\omega_2^K$. For if the cardinals agree, every real-domain order type is below $\omega_2^K$ and has a core copy. If $\omega_2^K<\omega_2^W$, an ambient real-domain wellorder of type $\omega_2^K$ has no such copy. The old CH bijection excludes the reverse cardinal inequality. Write $B$ for the second-order guard $\neg\exists0^\dagger\wedge\forall x\in\mathbb R\,(x\in K)$. Here $0^\dagger$ uses its usual real-coded two-block indiscernible theory and countable well-foundedness tests. Let $U$ code a wellorder $w$ of all reals with countable proper initial segments, a set $S$ of its points, and a regressive function on $S$. Such a $w$ has type $\omega_1$. Fodor's assertion says either that a club avoids $S$, or that one fiber meets every club. An existential third-sort witness $V$ stores a tag and either that first club or the single real naming the fiber. Thus its real-domain version is $\forall U\,\exists V\,\forall D\,q(U,V,D)$, where $D$ tests clubs and $q$ is second-order. Invalid $U$ is accepted automatically. No family of clubs is selected. The required $\Phi$ is the following normal form: \begin{equation}\label{eq:ramsey-pi23} \forall U\,\exists(E,V)\,\forall(P,D)\, \bigl[\neg B\ \vee\ \neg c(E,P)\ \vee\ q(U,V,D)\bigr]. \end{equation} All prefix variables have the third sort. If $\operatorname{CopyK}$ fails, a single $E$ with no certificate makes the matrix true. If it holds, a certificate for the selected $E$ reduces the matrix to the Fodor clause. Thus \eqref{eq:ramsey-pi23} is equivalent, over $\ZF+\DC$, to \eqref{eq:ramsey-semantic}. This proves the advertised $\Pi^2_3$ upper bound, without claiming minimality. \emph{The countermodel.} Start with $\ZFC+\mathsf{CR}$ and pass to its classical core $D$. Mitchell's Ramsey preservation theorem gives $D\models\ZFC+\GCH+\mathsf{CR}$ \cite[Theorem 1]{MitchellRamsey}. Also $K^D=D$ and $D$ has no $0^\dagger$. Apply Karagila's local symmetric construction at $\kappa=\mu=\omega_1^D$ \cite[Section 4]{KaragilaFodor}. First add $g:\kappa\to\kappa$ by bounded conditions, and set $S_\beta=\{\xi<\kappa:g(\xi)\geq\beta\}$. Then use the countable-support product of the club-shooting orders on the $S_\beta$, with the normal filter fixing old countable sets of coordinates. Let $N$ be the symmetric model. The combined forcing has a countably closed dense presentation of size $\omega_1$. A dense condition synchronizes the club maxima and chooses the value of $g$ there above every active index. Countable unions have lower bounds of the same form, and CH bounds the number of codes. The reals and cardinals are unchanged, and the countably complete support filter gives DC in $N$. Every ordinal-coded object of $N$ belongs to a bounded head $D[G_\alpha]$, and every such head is contained in $N$. Put $T_*=\kappa\setminus\Delta_{\beta<\kappa}S_\beta$. Then $f=g\restriction T_*$ is regressive and each fiber of value $\eta$ misses the retained club through $S_{\eta+1}$. The set $T_*$ is stationary in $N$. Indeed, a retained club belongs to a head $D[G_\alpha]$. Fusion in that head produces a limit point $\delta>\alpha+1$ of the club at which one may set $g(\delta)=\alpha$. Appending $\delta$ to every active coordinate below $\alpha$ is legal, while $\delta\notin S_{\alpha+1}$. This is stationarity in $N$; the full choice extension retains an additional diagonal club. For any old Ramsey $\rho>\omega_1$, a coloring in $N$ of $[\rho]^{<\omega}$ belongs to one bounded head. That head is a choice extension by a forcing of size $\omega_1<\rho$. Small-forcing preservation supplies a homogeneous set there \cite[Theorem 4.1]{GitmanJohnstone}, so that set also belongs to $N$. Hence $N\models\mathsf{CR}$. Classical mouse absoluteness and set-forcing invariance identify $K^N=D$; unchanged reals preserve the $0^\dagger$ predicate. Thus the antecedent of \eqref{eq:ramsey-semantic} holds in $N$, while its conclusion fails. The old CH bijection transports this counterexample to the third-order formula. These forcing and inner-model constructions give the stated consistency implication. \end{proof} For the structural conclusion, use a finite signature with number and real sorts partitioning its domain, the arithmetic operations on the number sort, and a membership relation between the two sorts. A full second-order sentence asserts the Peano axioms with second-order induction on the first sort and requires every subset of that sort to be coded by exactly one element of the second. Such a structure is isomorphic to the canonical structure on $\omega\sqcup\Pow(\omega)$. Translate third-sort variables in $\Phi$ into second-order subsets of its real sort. The universal assertion that every such frame satisfies this translation is equivalent to $\Phi$ in ZF. It has the structural $\Pi_2$ form of Definition~\ref{def:structural-pi2}. The $\Pi^2_3$ bound concerns third-order arithmetic, whereas this $\Pi_2$ classification concerns the L\'evy hierarchy. In particular, the Ramsey replacement of Theorem~\ref{thm:main} fails even with Foundation retained in the starting theory, and hence also with Foundation omitted. This argument does not assert that $\KW$ alone implies Fodor's lemma, nor does it supply a Ramsey replacement counterexample for the separate external rank-equiconsistency theorem without a further rank translation. \section{A strong-cardinal separation for the Chang model}\label{app:chang} We give the separation used in the introduction to explain the choice of $\HOD_{\Ord^\omega}$ in Theorem~\ref{thm:external-main}. Throughout this appendix, $C^U=L(\Ord^\omega)^U$ is computed in an ambient universe $U\models\ZFC$. Define \[ E_1^C(\sigma)=\ZFC+\CM+ [C\models\exists\kappa\,(V_\kappa\models\sigma)]. \] Let $\CS$ assert that strong cardinals are unbounded, with strongness given by its usual first-order extender formulation, and put \[ B_{\rm str}=\ZFC+\CS+ \text{``there is an inaccessible limit of strong cardinals.''} \] The following single first-order sentence will separate the theories: \begin{equation}\label{eq:chang-strong-sentence} \begin{aligned} \sigma_{\rm str}\equiv\exists\lambda\,\exists\nu\,[& \lambda,\nu\in\Ord\ \wedge\ \lambda<\nu\\ &{}\wedge\ \nu\text{ is a limit ordinal}\\ &{}\wedge\ V_\lambda\models\ZFC+\CS]. \end{aligned} \end{equation} Here the rank and its satisfaction relation are expressed by set witnesses, including satisfaction of the recursive set of all ZFC axioms. The ordinal $\nu$ is a height guard: in a witnessing outer rank $V_\kappa$, it ensures $\lambda+\omega\leq\nu<\kappa$. \begin{theorem}[Chang rank separation]\label{thm:chang-rank-separation} If $U\models\ZFC$, no full rank $V_\lambda^{C^U}$ satisfies $\ZFC+\CS$. In particular, $E_1^C(\sigma_{\rm str})$ is inconsistent, whereas \[ \Con(B_{\rm str})\ \Longrightarrow\ \Con(E_3(\sigma_{\rm str})). \] \end{theorem} Thus, relative to $B_{\rm str}$, substituting the Chang model for $\Hseq$ destroys even the equiconsistency of theories (1) and (3). The prohibition on Chang ranks requires no ambient measurable cardinals. Strong cardinals enter the consistency bound for the separating instance of theory (3). For a tautological $\sigma$, the two Chang analogues remain consistent relative to $\ZFC+\CM$. \subsection{The imported mouse construction} We use Mitchell's Chang-sharp construction. The relevant results are \cite{MitchellChang}, Theorem 1.5, Sections 1.3 and 3, Definition 4.1, and Proposition 1.4. The construction uses a set mouse over all the reals with a sufficiently long last extender. Section 3 reduces the hypothesis to set-sized data, and Definition 4.1 specifies the additional approximation system. The relevant mice use the linear iteration theory below a strong cardinal. Iterating the final extender gives a continuous class $I=\{\kappa_\alpha:\alpha\in\Ord\}$. Definition 3.9 gives uniformly interpreted term codes from the mouse. These terms represent every element of Chang. Proposition 1.4 extends appropriate order-preserving maps of $I$ to elementary embeddings of Chang. The large cardinal existence input is that $\ZFC+\CS$ supplies such a mouse over its entire real set, with the required iterability. Gappo and Sargsyan explicitly identify this upper bound in the introduction to \cite{GappoSargsyan}. We call the full set data specified by Mitchell a \emph{Mitchell datum}. This abbreviation includes the approximation system; a bare premouse with a long extender is not sufficient. All structural requirements on a fixed datum are first-order assertions about set structures, their satisfaction relations, functions, and ordinals. Their interpretation is absolute when the data and the relevant countable sequences are shared. The remaining nonlocal requirement is iterability. The next section addresses that requirement rather than assuming it is absolute. \subsection{Countable hull iterability transfers from a Chang rank} \begin{lemma}\label{lem:chang-rank-closure} Suppose $W=V_\lambda^{C^U}\models\ZFC$. Then $W$ and $U$ have the same reals and the same $\omega_1$. If $a\in W$, every $U$-countable sequence of elements of $a$ belongs to $W$. \end{lemma} \begin{proof} The Chang model is closed under countable sequences formed in $U$. In particular it contains every real and every countable ordinal sequence of $U$. If $a\in W$ and $s:\omega\to a$ belongs to $U$, then $s\in C^U$. Its rank is bounded by $\max\{\operatorname{rank}(a),\omega\}$ plus a fixed finite ordinal. This is below $\lambda$, since $W\models\ZFC$. Hence $s\in W$. Every real has bounded finite rank above $\omega$, so the real sets agree. If an ordinal in $W$ is countable in $U$, its enumeration belongs to $W$ by the preceding argument. Applying this to $\omega_1^W$, if necessary, proves equality of $\omega_1$. \end{proof} \begin{lemma}\label{lem:chang-iterability} Let $W$ be as above. Suppose $M\in W$ is a set premouse in the linear iteration setting of \cite{MitchellChang}. If $W$ regards every countable elementary hull of $M$ as iterable through all countable linear iterations, then the same assertion holds in $U$. Moreover $M$ has no ill-founded set-length linear iteration in $U$. \end{lemma} \begin{proof} Include the extender predicates and the final extender in the structure being considered. Let $X\prec M$ be any elementary substructure countable in $U$. An enumeration of $X$ is a countable sequence from the fixed set underlying $M$, so Lemma~\ref{lem:chang-rank-closure} puts $X$ and an enumeration in $W$. Set satisfaction is absolute, so $W$ recognizes its elementarity. The two universes form the same transitive collapse $\bar M$. A countable premouse, a countable putative linear iteration, and a descending sequence witnessing ill-foundedness can be coded by reals. The relevant code relations are statements of second-order arithmetic. Since $W$ and $U$ have exactly the same reals, they agree on these relations and on the assertion that every countable legal linear iteration of $\bar M$ is well-founded. Thus every countable hull remains countably iterable in $U$. For completeness, suppose there were a bad set-length linear iteration of $M$ in $U$. Retain the iteration through a first bad model, together with a descending-sequence witness for its formal ultrapower or direct-limit relation. In $U$, take a countable elementary hull of a sufficiently large set structure containing these data and the definitions of the iteration operations. Its transitive collapse gives a countable bad linear iteration of the collapse of a countable elementary substructure of $M$. The collapse preserves the iteration rules. Formal ultrapowers use functions from the relevant source structure, and elementarity supplies representatives of their quotient elements in the hull. The same reasoning applies to the direct-limit construction. The retained descending sequence witnesses that the last relation is still ill-founded. This contradicts the preceding paragraph. This argument concerns linear iteration. It does not assert preservation or existence of a strategy for arbitrary uncountable branching iteration trees. \end{proof} \subsection{Why the datum cannot belong to Chang} \begin{proposition}\label{prop:chang-forbidden-datum} A Mitchell datum over all the reals of $U$, with the requisite external linear iterability, cannot belong to $C^U$. \end{proposition} \begin{proof} Suppose the datum belongs to $C=C^U$. Write $(M,E)$ for its mouse and final extender. The canonical linear iteration by $E$ can be computed inside $C$ at every set-length stage. Its computation agrees with that in $U$: the source structures and their functions are the same, formal ultrapowers and direct limits are the same, and well-founded collapses are unique. Transfinite recursion in $C$ supplies the set-length iteration systems. Thus the class \[ I=\{\kappa_\alpha:\alpha\in\Ord\} \] and the interpretation of Mitchell's term codes are definable over $C$ from set parameters in the datum. This last definability assertion can be read directly from Definition 3.9 of \cite{MitchellChang}. Its ingredients are the canonical iteration maps, countable sequences of term codes, composition, and satisfaction in a set-sized Chang construction stage. In particular, the apparently class-length term $i_{\Ord}(f)(a)$ is evaluated at the first set stage $\alpha$ for which all entries of the finite ordinal tuple $a$ are below $\kappa_\alpha$. The value $i_\alpha(f)(a)$ is below $\kappa_\alpha$ and is fixed by every subsequent iteration map. Thus evaluation is uniformly first-order definable from the set data. No truth predicate for the whole Chang model is required. The auxiliary approximation system and generic objects used in the proof of indiscernibility do not enter the interpretation of these terms. Define an increasing map on ordinal indices by \[ f(\alpha)= \begin{cases} \alpha,&\alpha<\omega_1,\\ \omega_1+\alpha,&\alpha\geq\omega_1, \end{cases} \qquad s(\kappa_\alpha)=\kappa_{f(\alpha)}. \] The map preserves successors and limit-index status. It is continuous at limit indices of countable cofinality. Its only initial discontinuity is at $\omega_1$, whose cofinality is uncountable in both universes. Therefore $s$ satisfies the hypotheses of Mitchell's Proposition 1.4. Using the term representation of Chang, define \[ j(\tau(B))=\tau(s[B]). \] The equality and formula preservation furnished by the sharp make this definition independent of the chosen representation and make $j:C\to C$ elementary. The relation defining $j$ quantifies over set term codes and countable suitable sets $B$; all its ingredients are definable over $C$ from the datum. In particular $j$ is a parameter-definable class of $C$. It is nontrivial because \[ j(\kappa_{\omega_1})=\kappa_{\omega_1\cdot2} >\kappa_{\omega_1}. \] Suzuki's theorem \cite{Suzuki}, which requires ZF rather than Choice, excludes such a parameter-definable nontrivial elementary self-embedding of $C$. This is a contradiction. \end{proof} \subsection{The separation} \begin{proof}[Proof of Theorem~\ref{thm:chang-rank-separation}] Suppose $W=V_\lambda^{C^U}\models\ZFC+\CS$. Inside $W$, the imported mouse construction produces a Mitchell datum over $\mathbb R^W$. Lemma~\ref{lem:chang-rank-closure} gives $\mathbb R^W=\mathbb R^U$ and the same countable sequences from each fixed set in the datum. The bijection witnessing $|M|=|\mathbb R|$ remains a bijection externally. All elementarity and internal cardinal computations in the fixed structures remain correct. The height of $M$ still has cofinality $\omega_1$: its cofinal $\omega_1$-sequence remains cofinal, while any new countable cofinal sequence would belong to $W$ by bounded closure. Thus the structural requirements hold externally. Lemma~\ref{lem:chang-iterability} transfers the required linear iterability. The datum belongs to $W\subseteq C^U$, contradicting Proposition~\ref{prop:chang-forbidden-datum}. If a rank $V_\kappa^{C^U}$ satisfies $\sigma_{\rm str}$, the height guard puts $\lambda+\omega$ below $\kappa$. Induction on the witnessed cumulative hierarchy identifies its nested rank with the actual $V_\lambda^{C^U}$. Every subset required at an earlier hierarchy stage is present in the outer rank. Finite assignments and the full set satisfaction relation also lie below $\lambda+\omega$, so satisfaction agrees. This gives precisely the impossible $W$ above, proving inconsistency of $E_1^C(\sigma_{\rm str})$. For the consistency direction, work in a model of $B_{\rm str}$, and let $\delta$ be an inaccessible limit of ambient strong cardinals. Then $V_\delta\models\ZFC$. Every ambient strong $\rho<\delta$ is strong in $V_\delta$: for each target rank $V_\eta$ below $\delta$, choose the usual bounded extender $E$ derived from an ambient strongness embedding. Inaccessibility of $\delta$ puts its support, the extender, and the required power sets below $\delta$. To check the target-rank containment, represent each $x\in V_\eta$ in the ambient extender ultrapower as $[a,f]_E$. Replace $f$ by the function that keeps its values in $V_{\eta+1}$ and uses $\varnothing$ elsewhere. It represents the same $x$, since the ultrapower image of $\eta+1$ exceeds $\eta$. The new function has rank below $\delta$. Hence the natural factor map from the ultrapower of $V_\delta$ has every element of $V_\eta$ in its range. Its transitive collapse fixes these elements by induction on rank. Thus the ultrapower of $V_\delta$ contains $V_\eta$, as required. This proves $V_\delta\models\CS$. The ambient universe satisfies $\CM$, since strong cardinals are measurable and are unbounded. It satisfies $\ZFC$, hence $\ZF+\DC$. The rank $V_{\delta+\omega\cdot2}$ satisfies $\sigma_{\rm str}$, using $\lambda=\delta$ and $\nu=\delta+\omega$. This realizes $E_3(\sigma_{\rm str})$. \end{proof} The obstruction is a set-sized iterable datum that a full Chang rank satisfying $\ZFC+\CS$ would contain. The height guard in $\sigma_{\rm str}$ ensures that the nested rank and its satisfaction relation have their intended meanings. \subsection{The anti-inner-model question} The separation above leaves open whether restricting the available inner models restores the comparison. Use the standard Mitchell-order convention, so a measurable cardinal has order at least one, and let \[ A_2\quad\equiv\quad \text{``there is no inner model of $\ZFC$ with a measurable $\nu$ satisfying $o(\nu)\geq2$.''} \] The Mitchell order is computed in the indicated inner model. Equivalently, the excluded configuration consists there of two normal measures $U_0,U_1$ on the same $\nu$ with $U_0\in\operatorname{Ult}(M,U_1)$. Here $M$ is the inner model, and the ultrapower uses its functions. We use the semantic inner-model formulation of $A_2$; any formal version of the following question must fix a corresponding mouse or scheme formulation on both sides. \begin{question}\label{q:chang-anti-inner} Can an anti-inner-model hypothesis restore the equiconsistency of theories (1) and (3) after the Chang substitution? In particular, for every fixed first-order sentence $\sigma$, is \[ \Con\bigl(E_1^C(\sigma)+A_2\bigr) \quad\longleftrightarrow\quad \Con\bigl(E_3(\sigma)+A_2\bigr)? \] \end{question} In this question $A_2$ is appended to both ambient theories. The left-hand witnessing rank is still computed inside Chang, and the right-hand rank is computed in the $\ZF+\DC+\CM$ universe. The restriction permits order-one measurable cardinals and does not exclude measurable limits of measurable cardinals. No equiconsistency under this restriction is asserted here. Whether the Chang separation itself can be obtained from ordinary measurable-cardinal strength also remains open. \clearpage \begin{thebibliography}{99} \bibitem{Roguski} S. Roguski, \emph{The theory of the class HOD}, in A. Lachlan, M. Srebrny, and A. Zarach (eds.), \emph{Set Theory and Hierarchy Theory V}, Lecture Notes in Mathematics \textbf{619}, Springer-Verlag, Berlin, Heidelberg, 1977, pp.~251--255. \href{https://doi.org/10.1007/BFb0067656}{doi:10.1007/BFb0067656}. \bibitem{ResearchArchive} \emph{Core-model rank reduction and removal of Foundation}, Unpublished research notes, 23 September 2026, 05:13--06:07 UTC. \bibitem{Benhamou} T. Benhamou, \emph{Prikry forcing and tree Prikry forcing of various filters}, \href{https://arxiv.org/abs/1801.04424}{arXiv:1801.04424}, version 2. \bibitem{Grigorieff} S. Grigorieff, \emph{Intermediate submodels and generic extensions in set theory}, Annals of Mathematics (2) \textbf{101} (1975), no.~3, 447--490. \bibitem{GitikHayutKaragila} M. Gitik, Y. Hayut, and A. Karagila, \emph{The first measurable can be the first inaccessible cardinal}, \href{https://arxiv.org/abs/2401.02757}{arXiv:2401.02757}, version 2. \bibitem{HamkinsGap} J. D. Hamkins, \emph{Gap forcing: generalizing the L\'evy--Solovay theorem}, \href{https://arxiv.org/abs/math/9901108}{arXiv:math/9901108}. \bibitem{Usuba} T. Usuba, \emph{Geology of symmetric grounds}, \href{https://arxiv.org/abs/1912.10246}{arXiv:1912.10246}, version 3. \bibitem{MitchellCovering} W. J. Mitchell, \emph{The Covering Lemma}, in \emph{Handbook of Set Theory}, Springer, 2010. \href{https://people.clas.ufl.edu/wjm/files/covering.pdf}{Author's draft}, Sections 1--4, in particular Theorem~2.5. \bibitem{MiceMachetes} C. Henney-Turner and P. Welch, \emph{Of Mice and Machetes}, \href{https://arxiv.org/abs/2407.21562}{arXiv:2407.21562}, Definition~1.4 and Proposition~1.6. \bibitem{WelchHartig} P. Welch, \emph{Closed and unbounded classes and the H\"artig quantifier model}, Journal of Symbolic Logic \textbf{87} (2022), 564--584. \href{https://doi.org/10.1017/jsl.2021.21}{doi:10.1017/jsl.2021.21}. \href{https://arxiv.org/abs/1903.02663}{Author's preprint}, Section~2. \bibitem{ZemanInnerModels} M. Zeman, \emph{Inner Models and Large Cardinals}, De Gruyter Series in Logic and Its Applications \textbf{5}, Walter de Gruyter, Berlin and New York, 2002. \bibitem{SteelUltrapowers} J. R. Steel, \emph{An Introduction to Iterated Ultrapowers}, \href{https://www.math.cmu.edu/users/jcumming/Appalachian/steel_cmu_2015_files/Iteration-Ultrapowers.pdf}{Lecture notes}, Lectures 1 and 5. \bibitem{HayutKaragila} Y. Hayut and A. Karagila, \emph{Small measurable cardinals}, \href{https://arxiv.org/abs/2212.07973}{arXiv:2212.07973}, version 2. \bibitem{Jech} T. Jech, \emph{Set Theory}, Third Millennium Edition, revised and expanded, Springer, 2003. Theorem~13.9 and Lemma~19.35. \bibitem{GoldbergChoiceless} G. Goldberg, \emph{Choiceless Cardinals and the Continuum Problem}, \href{https://math.berkeley.edu/~goldberg/Papers/ChoicelessCardinalsContinuum.pdf}{Author's manuscript}, Lemma~3.6. \bibitem{Jakob} H. Jakob, \emph{Slender trees and the approximation property}, preprint, \href{https://arxiv.org/abs/2401.13446}{arXiv:2401.13446}, version 2. The iteration-like criterion is Theorem~3.8 in the HTML version consulted September 23, 2026. \bibitem{ReitzCohen} J. Reitz, \emph{Cohen forcing and inner models}, preprint, \href{https://arxiv.org/abs/1809.10092}{arXiv:1809.10092}, version 2. \bibitem{CFH} Y. Cheng, S.-D. Friedman, and J. D. Hamkins, \emph{Large cardinals need not be large in HOD}, \href{https://arxiv.org/abs/1407.6335}{arXiv:1407.6335}, Appendix, Lemmas~16 and~18--20. \bibitem{BrookeTaylorCoding} A. D. Brooke-Taylor, \emph{Large cardinals and definable well-orderings of the universe}, Journal of Symbolic Logic \textbf{74} (2009), no.~2, 641--654. \href{https://doi.org/10.2178/jsl/1243948331}{doi:10.2178/jsl/1243948331}. \href{https://arxiv.org/abs/0711.2591}{arXiv:0711.2591}, Section~2, especially Lemma~2 and Definition~3. \bibitem{FuchsHamkinsReitz} G. Fuchs, J. D. Hamkins, and J. Reitz, \emph{Set-theoretic geology}, \href{https://arxiv.org/abs/1107.4776v2}{arXiv:1107.4776}, version~2, Theorem~6 and Lemma~8. \bibitem{ReitzGA} J. Reitz, \emph{The Ground Axiom}, preprint, \href{https://arxiv.org/abs/math/0609064}{arXiv:math/0609064}. \bibitem{UsubaGrounds} T. Usuba, \emph{The downward directed grounds hypothesis and very large cardinals}, preprint, \href{https://arxiv.org/abs/1707.05132}{arXiv:1707.05132}. \bibitem{CarlSchlichtWelch} M. Carl, P. Schlicht, and P. Welch, \emph{Recognizable sets and Woodin cardinals: computation beyond the constructible universe}, Annals of Pure and Applied Logic \textbf{169} (2018), no.~4, 312--332. \href{https://doi.org/10.1016/j.apal.2017.12.007}{doi:10.1016/j.apal.2017.12.007}. \bibitem{MitchellChang} W. J. Mitchell, \emph{The sharp for the Chang model is small}, Archive for Mathematical Logic \textbf{56} (2017), 935--982. \href{https://arxiv.org/pdf/1705.00208}{Final arXiv manuscript}. \bibitem{GappoSargsyan} T. Gappo and G. Sargsyan, \emph{Determinacy in the Chang model}, Proceedings of the American Mathematical Society \textbf{154} (2026), 1763--1769. \href{https://arxiv.org/pdf/2302.06487}{arXiv manuscript}. \bibitem{Suzuki} A. Suzuki, \emph{No elementary embedding from $V$ into $V$ is definable from parameters}, Journal of Symbolic Logic \textbf{64} (1999), 1591--1594. \href{https://doi.org/10.2307/2586799}{doi:10.2307/2586799}. \bibitem{KaragilaDC} A. Karagila, \emph{Preserving dependent choice}, Bulletin of the Polish Academy of Sciences. Mathematics \textbf{67} (2019), 19--29. \href{https://doi.org/10.4064/ba8169-12-2018}{doi:10.4064/ba8169-12-2018}. \bibitem{MitchellRamsey} W. J. Mitchell, \emph{Ramsey cardinals and constructibility}, J. Symbolic Logic \textbf{44} (1979), no.~2, 260--266. \href{https://doi.org/10.2307/2273732}{doi:10.2307/2273732}. \bibitem{ApterKoepke} A. W. Apter and P. Koepke, \emph{Making all cardinals almost Ramsey}, Arch. Math. Logic \textbf{47} (2008), 769--783. \href{https://doi.org/10.1007/s00153-008-0107-1}{doi:10.1007/s00153-008-0107-1}. \href{https://www.math.uni-bonn.de/people/koepke/Preprints/Making_all_cardinals_almost_Ramsey.pdf}{Author's version}. \bibitem{CompleatDagger} A. Kanamori and T. Awerbuch-Friedlander, \emph{The compleat $0^\dagger$}, Math. Logic Quart. \textbf{36} (1990), no.~2, 133--141. \href{https://doi.org/10.1002/malq.19900360206}{doi:10.1002/malq.19900360206}. \bibitem{KaragilaFodor} A. Karagila, \emph{Fodor's lemma can fail everywhere}, Acta Math. Hungar. \textbf{154} (2018), no.~1, 231--242. \href{https://arxiv.org/abs/1610.03985}{arXiv:1610.03985}. \bibitem{GitmanJohnstone} V. Gitman and T. A. Johnstone, \emph{Indestructibility properties of Ramsey and Ramsey-like cardinals}, Ann. Pure Appl. Logic \textbf{173} (2022), no.~6, 103106. \href{https://doi.org/10.1016/j.apal.2022.103106}{doi:10.1016/j.apal.2022.103106}. \href{https://victoriagitman.github.io/files/indestructibleramseycardinalsnew.pdf}{Author's version}. \bibitem{BenNeriaLuecke} O. Ben-Neria and P. L\"ucke, \emph{On $\Sigma_1$-definable closed unbounded sets}, Canad. J. Math. \textbf{78} (2026), no.~3, 769--801. \href{https://doi.org/10.4153/S0008414X24000567}{doi:10.4153/S0008414X24000567}. \bibitem{MSFine} W. J. Mitchell and J. R. Steel, \emph{Fine Structure and Iteration Trees}, Lecture Notes in Logic \textbf{3}, Springer-Verlag, 1994; reprinted by Cambridge University Press, 2017. \href{https://doi.org/10.1017/9781316718315}{doi:10.1017/9781316718315}. \bibitem{SchimmerlingSteelTame} E. Schimmerling and J. R. Steel, \emph{Fine structure for tame inner models}, Journal of Symbolic Logic \textbf{61} (1996), no.~2, 621--639. \href{https://doi.org/10.2307/2275679}{doi:10.2307/2275679}. \bibitem{SteelCMIP} J. R. Steel, \emph{The Core Model Iterability Problem}, Lecture Notes in Logic \textbf{8}, Springer-Verlag, 1996; reprinted by Cambridge University Press, 2017. \href{https://doi.org/10.1017/9781316716892}{doi:10.1017/9781316716892}. \bibitem{SteelOutline} J. R. Steel, \emph{An outline of inner model theory}, in M. Foreman and A. Kanamori (eds.), \emph{Handbook of Set Theory}, Springer, 2010, pp.~1595--1684. \href{https://doi.org/10.1007/978-1-4020-5764-9_20}{doi:10.1007/978-1-4020-5764-9\_20}. \href{https://math.berkeley.edu/~steel/papers/steel1.pdf}{Author's version}. \bibitem{SteelLocalKc} J. R. Steel, \emph{Local $K^c$ constructions}, unpublished notes, 14 November 2003. \href{https://math.berkeley.edu/~steel/papers/localkc.nov03.pdf}{Author's manuscript}. \bibitem{LNSBackground} D. Levinson, I. Neeman, and G. Sargsyan, \emph{Unreachability of inductive-like pointclasses in $L(\mathbb R)$}, Journal of Symbolic Logic \textbf{91} (2026), 175--209. \href{https://doi.org/10.1017/jsl.2025.10170}{doi:10.1017/jsl.2025.10170}. \href{https://arxiv.org/abs/2210.10076v3}{arXiv:2210.10076}, version~3, Section~2.3. \bibitem{SteelCoreBook} R. Schindler and J. R. Steel, \emph{The core model induction}, unpublished seminar notes, 25 July 2007. \href{https://math.berkeley.edu/~steel/papers/corebookjul07.pdf}{Authors' manuscript}, Section~1.1. \bibitem{SteelTutorial} J. R. Steel, \emph{Derived models associated to mice}. \href{https://math.berkeley.edu/~steel/papers/tutorial3.pdf}{Author's version}, Section~2.5, pp.~114--115. \bibitem{SchlutzenbergCondensation} F. Schlutzenberg, \emph{A premouse inheriting strong cardinals from $V$}, Annals of Pure and Applied Logic \textbf{171} (2020), no.~9, article~102826. \href{https://doi.org/10.1016/j.apal.2020.102826}{doi:10.1016/j.apal.2020.102826}. \href{https://arxiv.org/abs/1506.04116v3}{arXiv:1506.04116}, version~3, Section~5, especially Theorem~5.2. \bibitem{SchlutzenbergDefinability} F. Schlutzenberg, \emph{The definability of the extender sequence $\mathbb E$ from $\mathbb E\upharpoonright\aleph_1$ in $L[\mathbb E]$}, Journal of Symbolic Logic \textbf{89} (2024), no.~2, 427--459. \href{https://doi.org/10.1017/jsl.2024.27}{doi:10.1017/jsl.2024.27}. \href{https://arxiv.org/abs/1906.00276v2}{arXiv:1906.00276}, version~2, Lemma~2.3 and Theorem~4.1. \bibitem{SchlutzenbergOrdinal} F. Schlutzenberg, \emph{Ordinal definability in $L[\mathbb E]$}, \href{https://arxiv.org/abs/2012.07185v2}{arXiv:2012.07185}, version~2, 13 May 2025. \bibitem{HamkinsWoodin} J. D. Hamkins and W. H. Woodin, \emph{Small forcing creates neither strong nor Woodin cardinals}, Proceedings of the American Mathematical Society \textbf{128} (2000), no.~10, 3025--3029. \href{https://doi.org/10.1090/S0002-9939-00-05347-8}{doi:10.1090/S0002-9939-00-05347-8}. \href{https://arxiv.org/abs/math/9808124}{arXiv:math/9808124}. \bibitem{CummingsForcing} J. Cummings, \emph{Iterated forcing and elementary embeddings}, in M. Foreman and A. Kanamori (eds.), \emph{Handbook of Set Theory}, Springer, 2010, pp.~775--883. \href{https://doi.org/10.1007/978-1-4020-5764-9_13}{doi:10.1007/978-1-4020-5764-9\_13}. \href{https://www.math.cmu.edu/users/jcumming/papers/repaper_finished_june_2008.pdf}{Author's June 2008 version}, Fact~5.10 (Easton's lemma). \end{thebibliography} \end{document}