GCH and the two forms of the singular cardinals hypothesis

Three cardinal-arithmetic hypotheses, stated for cardinals $\kappa$ of a fixed universe. Write $\kappa^+$ for the successor cardinal of $\kappa$ and $\operatorname{cf}\kappa$ for its cofinality. A cardinal $\kappa$ is singular if it is infinite and $\operatorname{cf}\kappa<\kappa$; it is a strong limit if $\kappa\neq 0$ and $2^\lambda<\kappa$ for every $\lambda<\kappa$.

1. GCH (generalized continuum hypothesis): for every infinite cardinal $\kappa$,

2. SCH (singular cardinals hypothesis, in the form quoted from Mitchell 1992): for every singular strong limit cardinal $\kappa$,

3. SCH$_2$ (second form): for every singular cardinal $\kappa$,

These are the hypotheses compared throughout the mission: GCH implies SCH, and the second form implies the first.

Formalization Note Singularity is Mathlib's Cardinal.IsSingular (infinite and not regular), cofinality is κ.ord.cof, strong limit is Mathlib's Cardinal.IsStrongLimit (which counts $\aleph_0$ as a strong limit, harmless here since $\aleph_0$ is regular), and $\kappa^+$ is Order.succ κ. The second form reuses the published predicate JechSetTheory.SCHAt from Def_JechStationary.