Add Erdős Problem 1167 (stepping-down partition relation)

[henrykmichalewski]

Formalizes Erdős Problem 1167 concerning a stepping-down partition relation for cardinals.

Contents

• New definition CardinalPartitionRel μ r γ ν: an r-uniform generalization of the cardinal partition relation μ → (ν)^r_γ, asserting that for every coloring of r-element subsets of μ with γ colors there is a monochromatic subset of size ν.
• The main open theorem statement for Problem 1167.
• Four variants exploring boundary cases:
  • finite_targets: behavior with finite target cardinalities
  • binary_colors: the two-color specialization
  • infinite_targets: behavior for infinite targets
  • r_eq_two: the r = 2 (graph) specialization

Closes #1991

Assisted by Claude (Anthropic).