Add Erdős Problem 1168 (ℵ_{ω+1} partition without GCH)

[henrykmichalewski]

Formalizes Erdős Problem 1168 on a partition relation for ℵ_{ω+1} that does not assume GCH.

Contents

• New definition CardinalCountableColorRamsey κ: generalizes the partition statement to ℵ_0 colors.
• The main open theorem statement for Problem 1168.
• An under_GCH variant relating the statement to its form under the Generalized Continuum Hypothesis.
• Four proved sanity checks verifying expected behavior of the defined relation.

Closes #1992

Assisted by Claude (Anthropic).