Дмитро, can you expand a bit on how you prove that every ℵ_α+ω is measurable in the HOD of L[Card] and why the sequence of the ℵ_α+ns is Prikry generic, assuming there is a sharp for an inner model with a proper class of measurable cardinals? Thanks, Ralf.

Дмитро, can you expand a bit on how you prove that every ℵ_α+ω is measurable in the HOD of L[Card] and why the sequence of the ℵ_α+ns is Prikry generic, assuming there is a sharp for an inner model with a proper class of measurable cardinals? Thanks, Ralf. Regardless of that, the result is correct: if L[Card] doesn't have an inner model with a proper class of measurable cardinals, then we may compare K^L[Card] with the sharp for an inner model with a proper class of measurable cardinals; a half-open interval from Card may then be used to produce a measure on an iterate of K^L[Card] which may be pulled back to K^L[Card]; this measure is in L[Card], which gives a contradiction. Your question about the complexity of the reals of L[cf] is related to the question: which reals does C* have (where C* is the least inner model which knows which ordinals have countable cofinality)? Magidor showed C* has 0^† and more, and with him I showed (assuming a measurable cardinal above a Woodin cardinal in V) that all the reals of C* are in M₁, the least inner model with one Wodin cardinal (so that K^C* exists and is 1-small).