Solovay: SCH holds above a strongly compact cardinal

Open

SingularCardinals.solovay

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

cardinal-arithmeticlarge-cardinalsset-theory

Let $\kappa$ be a strongly compact cardinal. Then the singular cardinals hypothesis holds above $\kappa$ : for every singular strong limit cardinal $\mu>\kappa$ ,

2^\mu=\mu^+.

This is the source's example of large cardinals "almost" implying SCH.

Preamble

import Mathlib
import Definitions.Def_SingularCardinals_largeCardinals

universe u

open Cardinal

Formal statement

namespace SingularCardinals

theorem solovay (κ : Cardinal.{u}) (hκ : IsStronglyCompact κ) (μ : Cardinal.{u})
    (hμ : κ < μ) (hsing : μ.IsSingular) (hlim : IsStrongLimit μ) :
    2 ^ μ = Order.succ μ := by sorry

end SingularCardinals

Source

Wikipedia, "Singular cardinals hypothesis", revision oldid=1349753131, https://en.wikipedia.org/w/index.php?title=Singular_cardinals_hypothesis&oldid=1349753131, last paragraph: "Solovay showed that large cardinals almost imply SCH—in particular, if κ is strongly compact cardinal, then the SCH holds above κ."

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph