Patai: a uniform gap $2^\kappa=\kappa^{+\gamma}$ forces $\gamma<\omega$

Proved

ContinuumHypothesis.patai_gap_finite

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

cardinal-arithmeticset-theory

(Patai, 1930.) Let $\gamma$ be an ordinal such that for each infinite cardinal $\kappa$ , $2^\kappa$ is the $\gamma$ -th successor of $\kappa$ , i.e.

2^{\aleph_\alpha}=\aleph_{\alpha+\gamma}\quad\text{for every ordinal }\alpha.

Then $\gamma$ is finite.

Preamble

import Definitions.Def_CH_CardinalArithmetic
open Cardinal
universe u

Formal statement

namespace ContinuumHypothesis

theorem patai_gap_finite (γ : Ordinal.{u})
    (h : ∀ α : Ordinal.{u}, (2 : Cardinal.{u}) ^ ℵ_ α = ℵ_ (α + γ)) :
    γ < Ordinal.omega0 := by sorry

end ContinuumHypothesis

Source

Wikipedia, "Continuum hypothesis" (revision oldid=1376315189), https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189; section 'Generalized continuum hypothesis', paragraph 4 ('László Patai proved that if γ is an ordinal and for each infinite cardinal κ, 2^κ is the γth successor of κ, then γ is finite'); Patai 1930.

Human review

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

View graph

Patai: a uniform gap 2κ=κ+γ2^\kappa=\kappa^{+\gamma}2κ=κ+γ forces γ<ω\gamma<\omegaγ<ω

Patai: a uniform gap $2^\kappa=\kappa^{+\gamma}$ forces $\gamma<\omega$