Existence of a Model of $o(\kappa)=\kappa^{++}$ from Failure of GCH at a Measurable Cardinal

TL;DR

This paper provides a detailed expository proof establishing that the failure of the Generalized Continuum Hypothesis at a measurable cardinal implies the existence of a model with a measurable cardinal of order 0(0)1(0)=0(0)^{++}, filling a gap in the literature.

Contribution

It offers a complete, detailed proof of the equiconsistency between GCH failure at a measurable cardinal and the existence of a certain large cardinal model.

Findings

Confirmed the equiconsistency between GCH failure at a measurable cardinal and a model with o(0)=0^{++}

Filled a gap in the literature with a detailed proof

Clarified the relationship between GCH failure and large cardinal properties

Abstract

It is well-known that the consistency strength of the GCH failing at a measurable cardinal is the existence of a cardinal $\kappa$ with $o(\kappa)=\kappa^{++}$. As the literature does not contain more than a proof sketch of the lower bound of this equiconsistency, we give an expository proof which fills in the details in order to fill this gap in the literature.