The Dodd-Jensen covering and square package

Work in $\mathrm{Z}\mathrm{F}\mathrm{C}$ and let $K$ denote the Dodd-Jensen core model, an inner model containing the constructible universe and contained in $V$ (Cardinal (initial ordinal) and cardinality). The Dodd-Jensen covering and square package for $K$ consists of the following interface statements.

1. Covering. $\mathrm{Cov}(V,K)$: every uncountable set $X$ of ordinals in $V$ is contained in a set $Y\in K$ with $\mathrm{\mid }Y\mathrm{\mid }=\mathrm{\mid }X\mathrm{\mid }$ (the covering lemma of Dodd-Jensen).
2. GCH in $K$ and square. $K$ satisfies the generalised continuum hypothesis, and for every infinite cardinal $\lambda$ of $K$ there is a square sequence ${\mathrm{\square }}_{\lambda }$ in $K$: a sequence $⟨C_{\alpha }:\alpha <{\lambda }^{+},\lim (\alpha )⟩$ with each $C_{\alpha }$ club in $\alpha$, $\mathrm{otp}(C_{\alpha })<\lambda$ whenever $\mathrm{cf}(\alpha )<\lambda$, and $C_{\beta }=\beta \cap C_{\alpha }$ whenever $\beta <\alpha$ is a limit point of $C_{\alpha }$ (Cardinal (initial ordinal) and cardinality).
3. Singular strong limits. $\mathrm{Cov}(V,K)$ implies that there is an uncountable strong limit cardinal $\kappa$ of countable cofinality with $2^{\kappa }={\kappa }^{+}$ and with a square sequence ${\mathrm{\square }}_{\kappa }$ (Good, Lemma 8).
4. Weak diamond on the countable-cofinality points. Let $W:=\{\alpha <{\kappa }^{+}:\mathrm{cf}(\alpha )=\omega \}$. From ${\mathrm{\square }}_{\kappa }$ and $2^{\kappa }={\kappa }^{+}$ one has ${\mathrm{♢}}_{{\kappa }^{+}}(W)$: a sequence $⟨S_{\alpha }:\alpha \in W⟩$ with $S_{\alpha }\subseteq \alpha$ such that for every $X\subseteq {\kappa }^{+}$ the set $\{\alpha \in W:X\cap \alpha =S_{\alpha }\}$ is stationary in ${\kappa }^{+}$ (Good, Lemma 11, after Devlin).
5. Nonreflecting stationary set. From ${\mathrm{\square }}_{\kappa }$ and ${\mathrm{♢}}_{{\kappa }^{+}}(W)$ there is a stationary $E\subseteq W$ with ${\mathrm{\square }}_{\kappa }(E)$, the assertion of Good's Definition 3: there is a sequence $⟨C_{\alpha }:\alpha <{\kappa }^{+},\lim (\alpha )⟩$ with each $C_{\alpha }$ club in $\alpha$, $\mathrm{otp}(C_{\alpha })<\kappa$ whenever $\mathrm{cf}(\alpha )<\kappa$, and such that for every limit point $\beta$ of $C_{\alpha }$ one has $\beta \mathrm{\notin }E$ and $C_{\beta }=\beta \cap C_{\alpha }$; the clause $\beta \mathrm{\notin }E$ is the one from which Good derives that a stationary $E$ with ${\mathrm{\square }}_{\kappa }(E)$ is nonreflecting. In addition $\{\alpha \in E:X\cap \alpha =S_{\alpha }\}$ is stationary for every $X\subseteq {\kappa }^{+}$ (Good, Lemma 12, exactly item IV.2.10 of Devlin's Constructibility).

Statement 1 is the covering theorem of Dodd-Jensen; statements 2, 4 and 5 are fine-structural consequences recorded with the exact citations above. The package is the input of Dodd-Jensen covering supplies Fleissner HYP data; the deep covering theorem itself is not reproved in this library, and no clause of the package is asserted to be a theorem of $\mathrm{Z}\mathrm{F}\mathrm{C}$ without the hypothesis "no inner model with a measurable cardinal" that supplies it.

• No measurable cardinal is constructed here. The package is a conditional consequence of the nonexistence of inner models with measurable cardinals; the definition records the objects and their properties, not the inner-model construction that produces them.

• Ordinals and clubs. Clubs and stationarity are taken in the ordinal spaces ${\lambda }^{+}$ with the order topology; "nonreflecting" means $E\cap \beta$ is nonstationary in $\beta$ for every $\beta <{\kappa }^{+}$ (Cardinal (initial ordinal) and cardinality).

• AC is used throughout, in the comparison of cardinalities, the choice of nonlimit ladders and the standard cardinal arithmetic (The Axiom of Choice).