Add Erdős Problem 1172 (partition relations under GCH)

[henrykmichalewski]

Formalizes Erdős Problem 1172 on ordinal partition relations under GCH.

Contents

• Uses OrdinalRamsey (defined locally in this file as the standard α → (β, γ)² ordinal Ramsey predicate).
• Local encodings of GCH and CH as Props (no Mathlib axiom is assumed).
• Main open theorem with 5 variants covering the 4 sub-conjectures of Problem 1172:
  • Under GCH: ω_3 → (ω_2, ω_1 + 2)²
  • Under GCH: ω_3 → (ω_2 + ω_1, ω_2 + ω)²
  • Under GCH: ω_2 → (ω_1^{ω+2} + 2, ω_1 + 2)²
  • Under CH: ω_2 → (ω_1 + ω)²_2
• gch_implies_ch proved as a small auxiliary lemma.
• A related instance of the Erdős–Rado theorem included for context.

Closes #1995

Assisted by Claude (Anthropic).