FormalConjecturesForMathlib.Combinatorics.Ramsey

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Data.Finset.Basic
public import Mathlib.Data.Fintype.Card
public import Mathlib.Order.Lattice.Nat

@[expose] public section

Hypergraph Ramsey Numbers

This file defines the r-uniform hypergraph Ramsey number R_r(n).

namespace Combinatorics

The r-uniform hypergraph Ramsey number R_r(n). The smallest natural number m such that every 2-coloring of the r-subsets of a set of size m contains a monochromatic subset of size n.

noncomputable def hypergraphRamsey (r n : ℕ) : ℕ :=
  sInf { m | ∀ (c : Finset (Fin m) → Bool),
    ∃ (S : Finset (Fin m)), S.card = n ∧
      ∃ (color : Bool), ∀ (e : Finset (Fin m)), e ⊆ S → e.card = r → c e = color }

n ≤ hypergraphRamsey r n when the set is nonempty.

theorem le_hypergraphRamsey (r n : ℕ) (hne : { m | ∀ (c : Finset (Fin m) → Bool),
    ∃ (S : Finset (Fin m)), S.card = n ∧
      ∃ (color : Bool), ∀ (e : Finset (Fin m)), e ⊆ S → e.card = r → c e = color }.Nonempty) :
    n ≤ hypergraphRamsey r n := byr:ℕn:ℕhne:{m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}.Nonempty⊢ n ≤ hypergraphRamsey r n
  apply le_csInf hner:ℕn:ℕhne:{m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}.Nonempty⊢ ∀ b ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}, n ≤ b
  intro m hmr:ℕn:ℕhne:{m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}.Nonemptym:ℕhm:m ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ n ≤ m
  have : ∃ (S : Finset (Fin m)), S.card = n ∧ _ := hm (fun _ ↦ false)r:ℕn:ℕhne:{m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}.Nonemptym:ℕhm:m ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}this:∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → false = color⊢ n ≤ m
  obtain ⟨S, hS, -⟩ := thisr:ℕn:ℕhne:{m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}.Nonemptym:ℕhm:m ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = n ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}S:Finset (Fin m)hS:S.card = n⊢ n ≤ m
  calc n = S.card := hS.symm
    _ ≤ Fintype.card (Fin m) := Finset.card_le_univ S
    _ = m := Fintype.card_fin m

hypergraphRamsey r r = r for any r.


theorem hypergraphRamsey_self (r : ℕ) : hypergraphRamsey r r = r := byr:ℕ⊢ hypergraphRamsey r r = r
  have h_mem : r ∈ { m | ∀ (c : Finset (Fin m) → Bool),
      ∃ (S : Finset (Fin m)), S.card = m ∧
        ∃ (color : Bool), ∀ (e : Finset (Fin m)), e ⊆ S → e.card = r → c e = color } := by
    intro cr:ℕc:Finset (Fin r) → Bool⊢ ∃ S, S.card = r ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = colorr:ℕh_mem:r ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = m ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ hypergraphRamsey r r = r
    refine ⟨Finset.univ, ?_, c Finset.univ, ?_⟩refine_1r:ℕc:Finset (Fin r) → Bool⊢ Finset.univ.card = rrefine_2r:ℕc:Finset (Fin r) → Bool⊢ ∀ e ⊆ Finset.univ, e.card = r → c e = c Finset.univr:ℕh_mem:r ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = m ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ hypergraphRamsey r r = r
    ·refine_1r:ℕc:Finset (Fin r) → Bool⊢ Finset.univ.card = rr:ℕh_mem:r ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = m ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ hypergraphRamsey r r = r simp [Fintype.card_fin]All goals completed! 🐙r:ℕh_mem:r ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = m ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ hypergraphRamsey r r = r
    ·refine_2r:ℕc:Finset (Fin r) → Bool⊢ ∀ e ⊆ Finset.univ, e.card = r → c e = c Finset.univr:ℕh_mem:r ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = m ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ hypergraphRamsey r r = r intro e _ he_cardrefine_2r:ℕc:Finset (Fin r) → Boole:Finset (Fin r)a✝:e ⊆ Finset.univhe_card:e.card = r⊢ c e = c Finset.univr:ℕh_mem:r ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = m ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ hypergraphRamsey r r = r
      congr 1refine_2r:ℕc:Finset (Fin r) → Boole:Finset (Fin r)a✝:e ⊆ Finset.univhe_card:e.card = r⊢ e = Finset.univr:ℕh_mem:r ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = m ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ hypergraphRamsey r r = r
      exact Finset.eq_univ_of_card e (he_card.trans (Fintype.card_fin r).symm)r:ℕh_mem:r ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = m ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ hypergraphRamsey r r = rr:ℕh_mem:r ∈ {m | ∀ (c : Finset (Fin m) → Bool), ∃ S, S.card = m ∧ ∃ color, ∀ e ⊆ S, e.card = r → c e = color}⊢ hypergraphRamsey r r = r
  exact le_antisymm (Nat.sInf_le h_mem) (le_hypergraphRamsey r r ⟨r, h_mem⟩)All goals completed! 🐙

end Combinatorics