The least counterexample to SCH has countable cofinality

Open

SingularCardinals.cf_eq_aleph0_of_least_sch_counterexample

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

cardinal-arithmeticset-theorysingular-cardinals

Let $\kappa$ be the least counterexample to the singular cardinals hypothesis: $\kappa$ is a singular strong limit cardinal with $2^\kappa\neq\kappa^+$ , and every singular strong limit cardinal $\mu<\kappa$ satisfies $2^\mu=\mu^+$ . Then

\operatorname{cf}\kappa=\aleph_0.

This is the "in particular" consequence of Silver's theorem recorded in the source.

Preamble

import Mathlib
import Definitions.Def_JechStationary
import Definitions.Def_SingularCardinals_basic

universe u

open Cardinal

Formal statement

namespace SingularCardinals

theorem cf_eq_aleph0_of_least_sch_counterexample (κ : Cardinal.{u})
    (hsing : κ.IsSingular) (hlim : IsStrongLimit κ) (hfail : 2 ^ κ ≠ Order.succ κ)
    (hleast : ∀ μ : Cardinal.{u}, μ < κ → μ.IsSingular → IsStrongLimit μ →
      2 ^ μ = Order.succ μ) :
    κ.ord.cof = ℵ₀ := 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, paragraph beginning "Jack Silver proved ...": "In particular, then, if κ is the least counterexample to the singular cardinals hypothesis, then cf(κ) = ℵ₀."

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