From 77e9f671a13845f7fda29678071fa0cfb63c2183 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 13 Oct 2026 09:34:36 +0000 Subject: [PATCH 1/2] =?UTF-8?q?Import=20the=20Hajnal=E2=80=93Szemer=C3=A9d?= =?UTF-8?q?i=20equitable=20colouring=20theorem?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanPool/HajnalSzemeredi.lean | 34 ++ LeanPool/HajnalSzemeredi/Cases.lean | 575 ++++++++++++++++++ LeanPool/HajnalSzemeredi/Count.lean | 312 ++++++++++ .../HajnalSzemeredi/CountDefinitions.lean | 81 +++ LeanPool/HajnalSzemeredi/Defs.lean | 205 +++++++ LeanPool/HajnalSzemeredi/Final.lean | 148 +++++ LeanPool/HajnalSzemeredi/Imports.lean | 18 + LeanPool/HajnalSzemeredi/Main.lean | 274 +++++++++ LeanPool/HajnalSzemeredi/Reach.lean | 55 ++ LeanPool/HajnalSzemeredi/Shift.lean | 121 ++++ LeanPool/HajnalSzemeredi/Structure.lean | 345 +++++++++++ LeanPool/projects/hajnal-szemeredi.yaml | 52 ++ 12 files changed, 2220 insertions(+) create mode 100644 LeanPool/HajnalSzemeredi.lean create mode 100644 LeanPool/HajnalSzemeredi/Cases.lean create mode 100644 LeanPool/HajnalSzemeredi/Count.lean create mode 100644 LeanPool/HajnalSzemeredi/CountDefinitions.lean create mode 100644 LeanPool/HajnalSzemeredi/Defs.lean create mode 100644 LeanPool/HajnalSzemeredi/Final.lean create mode 100644 LeanPool/HajnalSzemeredi/Imports.lean create mode 100644 LeanPool/HajnalSzemeredi/Main.lean create mode 100644 LeanPool/HajnalSzemeredi/Reach.lean create mode 100644 LeanPool/HajnalSzemeredi/Shift.lean create mode 100644 LeanPool/HajnalSzemeredi/Structure.lean create mode 100644 LeanPool/projects/hajnal-szemeredi.yaml diff --git a/LeanPool/HajnalSzemeredi.lean b/LeanPool/HajnalSzemeredi.lean new file mode 100644 index 0000000000..ca1bf7225b --- /dev/null +++ b/LeanPool/HajnalSzemeredi.lean @@ -0,0 +1,34 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ + +module + +public import LeanPool.HajnalSzemeredi.Defs +public import LeanPool.HajnalSzemeredi.Reach +public import LeanPool.HajnalSzemeredi.Shift +public import LeanPool.HajnalSzemeredi.Count +public import LeanPool.HajnalSzemeredi.Structure +public import LeanPool.HajnalSzemeredi.Cases +public import LeanPool.HajnalSzemeredi.Main +public import LeanPool.HajnalSzemeredi.Final + +/-! +# The Hajnal–Szemerédi theorem on equitable vertex colourings + +Source: doi:10.1017/S0963548307008619, url:https://github.com/jtraverso/hajnal-szemeredi/tree/ba34061e3cf12dfc8297610d5d7b3f0afac7ec54 +Authors: Juan Pablo Traverso Gianini +Status: verified +Main declarations: `HajnalSzemeredi.hajnalSzemeredi`, `HajnalSzemeredi.hajnalSzemeredi_exact` +Tags: graph-theory, equitable-colouring, extremal-combinatorics +MSC: 05C15, 05C35 +-/ + +/-! +# Hajnal–Szemerédi equitable colourings + +Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit +`ba34061e3cf12dfc8297610d5d7b3f0afac7ec54`; import paths adapted. +-/ diff --git a/LeanPool/HajnalSzemeredi/Cases.lean b/LeanPool/HajnalSzemeredi/Cases.lean new file mode 100644 index 0000000000..051ebfeb76 --- /dev/null +++ b/LeanPool/HajnalSzemeredi/Cases.lean @@ -0,0 +1,575 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.HajnalSzemeredi.Shift +public import LeanPool.HajnalSzemeredi.Structure + +/-! +Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit +`ba34061e3cf12dfc8297610d5d7b3f0afac7ec54`; import paths adapted. + +# Los dos casos de recoloreo del Teorema 2.4 de Kierstead–Kostochka + +Contexto: `Ctx G S P c r s lo hi` (clase grande inaccesible), `U` y `𝒜' = T_U` como en +`Ctx.exists_TU`, un vértice solo `z` con color `W = c z ∈ 𝒜'`, un vecino especial +`y₁ ∈ S_z ⊆ B`, y una coloración equitativa `g` de `B⁻ = B \ {y₁}` con la paleta `ℬ = P \ 𝒜` +(dada por la hipótesis de inducción primaria). + +* **Caso 1** (`case1`): `z` es movible a una clase `X ∈ 𝒜 \ {W}`. Se mueve `z` a `X` y `y₁` a + `W`; la coloración de `A⁺ = A ∪ {y₁}` es equitativa o casi equitativa con clase grande + `X ∪ {z}` accesible (porque `W` es terminal), y por el Lema 2.1 se vuelve equitativa; junto con + `g` da una coloración equitativa de `S`. +* **Caso 2** (`case2`): `z` no es movible a ninguna clase de `𝒜` y tiene dos vecinos especiales + `y₁ ≠ y₂` no adyacentes. Se mueve `y₁` a `W` y `z` a una clase `Y` de `g` sin vecinos de `z`; + se obtiene una coloración casi equitativa con estrictamente más clases accesibles. +-/ + +@[expose] public section + +noncomputable section + +open Finset Relation + +namespace HajnalSzemeredi + +variable {V : Type*} {G : SimpleGraph V} + +open Classical in +private lemma proper_mono' {S T : Finset V} {f : V → ℕ} (h : Proper G S f) (hT : T ⊆ S) : + Proper G T f := + fun v hv w hw => h v (hT hv) w (hT hw) + +open Classical in +private lemma proper_insert_update {T : Finset V} {f : V → ℕ} {v : V} {j : ℕ} + (h : Proper G T f) (hmov : Movable G T f v j) : + Proper G (insert v T) (Function.update f v j) := by + intro a ha b hb hab + by_cases hav : a = v + · subst hav + have hba : b ≠ a := fun h => G.loopless.irrefl _ (h ▸ hab) + have hbT : b ∈ T := (mem_insert.mp hb).resolve_left hba + simp only [Function.update_self, Function.update_of_ne hba] + intro hjb + exact hmov b (mem_cls.mpr ⟨hbT, hjb.symm⟩) hab + · have haT : a ∈ T := (mem_insert.mp ha).resolve_left hav + by_cases hbv : b = v + · subst hbv + simp only [Function.update_self, Function.update_of_ne hav] + intro hja + exact hmov a (mem_cls.mpr ⟨haT, hja⟩) hab.symm + · have hbT : b ∈ T := (mem_insert.mp hb).resolve_left hbv + simpa [Function.update_of_ne hav, Function.update_of_ne hbv] using h a haT b hbT hab + +open Classical in +private lemma cls_insert_update_self {T : Finset V} {f : V → ℕ} {v : V} {j : ℕ} : + cls (insert v T) (Function.update f v j) j = insert v (cls T f j) := by + ext w + by_cases hw : w = v + · subst hw; simp + · simp [hw] + +open Classical in +private lemma cls_insert_update_ne {T : Finset V} {f : V → ℕ} {v : V} {i j : ℕ} + (hv : v ∉ T) (hij : i ≠ j) : + cls (insert v T) (Function.update f v j) i = cls T f i := by + ext w + by_cases hw : w = v + · subst hw; simp [hv, Ne.symm hij] + · simp [hw] + +open Classical in +private lemma cls_erase' {T : Finset V} {f : V → ℕ} {v : V} {i : ℕ} : + cls (T.erase v) f i = (cls T f i).erase v := by + ext w + simp [and_assoc] + +open Classical in +private lemma cls_part {S : Finset V} {c : V → ℕ} {Q : Finset ℕ} {i : ℕ} (hi : i ∈ Q) : + cls (part S c Q) c i = cls S c i := by + ext w + simp only [mem_cls, part, mem_filter] + constructor + · rintro ⟨⟨hw, -⟩, hc⟩; exact ⟨hw, hc⟩ + · rintro ⟨hw, hc⟩; exact ⟨⟨hw, hc ▸ hi⟩, hc⟩ + +open Classical in +private lemma solo_eq {S : Finset V} {c : V → ℕ} {y z u : V} {W : ℕ} + (h : nIn G S c y W = {z}) (hu : u ∈ S) (hcu : c u = W) (hadj : G.Adj y u) : u = z := by + have : u ∈ nIn G S c y W := mem_inter.mpr ⟨mem_nbr.mpr ⟨hu, hadj⟩, mem_cls.mpr ⟨hu, hcu⟩⟩ + rw [h] at this + exact mem_singleton.mp this + +open Classical in +private lemma proper_comb {S SA SB : Finset V} {PA PB : Finset ℕ} {cA cB : V → ℕ} + (hA : Proper G SA cA) (hB : Proper G SB cB) (hiA : Into SA cA PA) (hiB : Into SB cB PB) + (hS : SA ∪ SB = S) (hPdisj : Disjoint PA PB) : + Proper G S (fun v => if v ∈ SA then cA v else cB v) := by + intro v hv w hw hvw + have hv' : v ∈ SA ∪ SB := hS ▸ hv + have hw' : w ∈ SA ∪ SB := hS ▸ hw + by_cases hvA : v ∈ SA <;> by_cases hwA : w ∈ SA <;> simp only [hvA, hwA, ite_true, ite_false] + · exact hA v hvA w hwA hvw + · have hwB : w ∈ SB := (mem_union.mp hw').resolve_left hwA + intro heq + exact disjoint_left.mp hPdisj (hiA v hvA) (heq ▸ hiB w hwB) + · have hvB : v ∈ SB := (mem_union.mp hv').resolve_left hvA + intro heq + exact disjoint_left.mp hPdisj (hiA w hwA) (heq ▸ hiB v hvB) + · exact hB v ((mem_union.mp hv').resolve_left hvA) w ((mem_union.mp hw').resolve_left hwA) hvw + +open Classical in +private lemma into_comb {S SA SB : Finset V} {P PA PB : Finset ℕ} {cA cB : V → ℕ} + (hiA : Into SA cA PA) (hiB : Into SB cB PB) (hS : SA ∪ SB = S) (hP : PA ∪ PB = P) : + Into S (fun v => if v ∈ SA then cA v else cB v) P := by + intro v hv + have hv' : v ∈ SA ∪ SB := hS ▸ hv + rw [← hP] + by_cases hvA : v ∈ SA + · simp only [hvA, ite_true]; exact mem_union_left _ (hiA v hvA) + · simp only [hvA, ite_false] + exact mem_union_right _ (hiB v ((mem_union.mp hv').resolve_left hvA)) + +open Classical in +private lemma cls_comb_A {S SA SB : Finset V} {PA PB : Finset ℕ} {cA cB : V → ℕ} {i : ℕ} + (hiB : Into SB cB PB) (hS : SA ∪ SB = S) (hPdisj : Disjoint PA PB) (hi : i ∈ PA) : + cls S (fun v => if v ∈ SA then cA v else cB v) i = cls SA cA i := by + ext v + simp only [mem_cls] + constructor + · rintro ⟨hv, hc⟩ + by_cases hvA : v ∈ SA + · simp only [hvA, ite_true] at hc; exact ⟨hvA, hc⟩ + · simp only [hvA, ite_false] at hc + have hvB : v ∈ SB := (mem_union.mp (hS ▸ hv : v ∈ SA ∪ SB)).resolve_left hvA + exact absurd (hc ▸ hiB v hvB) (disjoint_left.mp hPdisj hi) + · rintro ⟨hv, hc⟩ + exact ⟨hS ▸ mem_union_left _ hv, by simp only [hv, ite_true]; exact hc⟩ + +open Classical in +private lemma cls_comb_B {S SA SB : Finset V} {PA PB : Finset ℕ} {cA cB : V → ℕ} {i : ℕ} + (hiA : Into SA cA PA) (hS : SA ∪ SB = S) (hdisj : Disjoint SA SB) + (hPdisj : Disjoint PA PB) (hi : i ∈ PB) : + cls S (fun v => if v ∈ SA then cA v else cB v) i = cls SB cB i := by + ext v + simp only [mem_cls] + constructor + · rintro ⟨hv, hc⟩ + by_cases hvA : v ∈ SA + · simp only [hvA, ite_true] at hc + exact absurd hi (disjoint_left.mp hPdisj (hc ▸ hiA v hvA)) + · simp only [hvA, ite_false] at hc + exact ⟨(mem_union.mp (hS ▸ hv : v ∈ SA ∪ SB)).resolve_left hvA, hc⟩ + · rintro ⟨hv, hc⟩ + have hvA : v ∉ SA := fun h => disjoint_left.mp hdisj h hv + exact ⟨hS ▸ mem_union_right _ hv, by simp only [hvA, ite_false]; exact hc⟩ + +open Classical in +private lemma reach_restrict {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} + (h : Ctx G S P c r s lo hi) {R : ℕ → ℕ → Prop} + (hR : ∀ a b, R a b → Mov G S c a b) {X : ℕ} (hX : ReflTransGen R X lo) : + ReflTransGen (fun a b => R a b ∧ a ∈ acc G S P c lo ∧ b ∈ acc G S P c lo) X lo := by + have key : ∀ a, ReflTransGen R a lo → a ∈ acc G S P c lo ∧ + ReflTransGen (fun a b => R a b ∧ a ∈ acc G S P c lo ∧ b ∈ acc G S P c lo) a lo := by + intro a ha + induction ha using ReflTransGen.head_induction_on with + | refl => exact ⟨h.lo_mem_acc, ReflTransGen.refl⟩ + | head hab _ ih => + have hm := h.mem_acc_of_mov (hR _ _ hab) ih.1 + exact ⟨hm, ReflTransGen.head ⟨hab, hm, ih.1⟩ ih.2⟩ + exact (key X hX).2 + +open Classical in +/-- Pegado de dos coloraciones equitativas de partes disjuntas con paletas disjuntas. -/ +theorem isEq_combine {S SA SB : Finset V} {P PA PB : Finset ℕ} {cA cB : V → ℕ} {s : ℕ} + (hA : IsEq G SA PA cA s) (hB : IsEq G SB PB cB s) (hS : SA ∪ SB = S) + (hdisj : Disjoint SA SB) (hP : PA ∪ PB = P) (hPdisj : Disjoint PA PB) : + IsEq G S P (fun v => if v ∈ SA then cA v else cB v) s := by + refine ⟨proper_comb hA.proper hB.proper hA.into hB.into hS hPdisj, + into_comb hA.into hB.into hS hP, fun i hi => ?_⟩ + rcases mem_union.mp (hP ▸ hi : i ∈ PA ∪ PB) with hi' | hi' + · rw [cls_comb_A hB.into hS hPdisj hi']; exact hA.card i hi' + · rw [cls_comb_B hA.into hS hdisj hPdisj hi']; exact hB.card i hi' + +open Classical in +theorem case1 {S : Finset V} {P : Finset ℕ} {c g : V → ℕ} {r s lo hi U : ℕ} {z y₁ : V} + (h : Ctx G S P c r s lo hi) + (hterm : ∀ W ∈ T G S P c lo U, ∀ X ∈ (acc G S P c lo).erase W, + ReflTransGen (avoid G S c W) X lo) + (hzS : z ∈ S) (hzT : c z ∈ T G S P c lo U) + (hy₁ : y₁ ∈ Sz G S c (T G S P c lo U) (part S c (P \ acc G S P c lo)) z) + (hX : ∃ X ∈ acc G S P c lo, X ≠ c z ∧ Movable G S c z X) + (hg : IsEq G ((part S c (P \ acc G S P c lo)).erase y₁) (P \ acc G S P c lo) g s) : + ∃ c', IsEq G S P c' s := by + obtain ⟨X, hXacc, hXW, hXmov⟩ := hX + set PA := acc G S P c lo with hPA + set PB := P \ PA with hPB + set A := part S c PA with hA + set B := part S c PB with hB + have hWacc : c z ∈ PA := (mem_erase.mp (Ctx.T_subset U hzT)).2 + have hWlo : c z ≠ lo := by + intro e + have hz' := hzT + rw [e] at hz' + exact Ctx.lo_notMem_T U hz' + have hWhi : c z ≠ hi := fun e => h.hi_not (e ▸ hWacc) + have hWcard : (cls S c (c z)).card = s := h.near.card _ (Ctx.acc_subset hWacc) hWlo hWhi + obtain ⟨hy₁B, hsolo⟩ := mem_filter.mp hy₁ + obtain ⟨-, -, -, hsolo₁⟩ := hsolo + have hy₁S : y₁ ∈ S := (mem_filter.mp hy₁B).1 + have hy₁PB : c y₁ ∈ PB := (mem_filter.mp hy₁B).2 + have hy₁PA : c y₁ ∉ PA := (mem_sdiff.mp hy₁PB).2 + have hzA : z ∈ A := mem_filter.mpr ⟨hzS, hWacc⟩ + have hy₁A : y₁ ∉ A := fun hh => hy₁PA (mem_filter.mp hh).2 + have hXlo_hi : X ≠ hi := fun e => h.hi_not (e ▸ hXacc) + set c1 := Function.update c z X with hc1 + set φ := Function.update c1 y₁ (c z) with hφ + set SA := insert y₁ A with hSA + have hc1prop : Proper G A c1 := + proper_mono' (proper_update h.near.proper hXmov) (filter_subset _ _) + have hmov1 : Movable G A c1 y₁ (c z) := by + intro w hw hadj + rw [mem_cls] at hw + have hwz : w ≠ z := by + rintro rfl + rw [hc1, Function.update_self] at hw + exact hXW hw.2 + rw [hc1, Function.update_of_ne hwz] at hw + exact hwz (solo_eq hsolo₁ (mem_filter.mp hw.1).1 hw.2 hadj) + have hprop : Proper G SA φ := proper_insert_update hc1prop hmov1 + have hinto : Into SA φ PA := by + intro v hv + by_cases hvy : v = y₁ + · subst hvy; simpa [hφ] using hWacc + · have hvA : v ∈ A := (mem_insert.mp hv).resolve_left hvy + rw [hφ, Function.update_of_ne hvy] + by_cases hvz : v = z + · subst hvz; simpa [hc1] using hXacc + · rw [hc1, Function.update_of_ne hvz]; exact (mem_filter.mp hvA).2 + have hclsW : cls SA φ (c z) = insert y₁ ((cls S c (c z)).erase z) := by + rw [hSA, hφ, cls_insert_update_self, hc1, cls_update_old hzA hXW.symm, cls_part hWacc] + have hclsWcard : (cls SA φ (c z)).card = s := by + rw [hclsW, card_insert_of_notMem, card_erase_of_mem (mem_cls.mpr ⟨hzS, rfl⟩), hWcard] + · have : 0 < s := hWcard ▸ card_pos.mpr ⟨z, mem_cls.mpr ⟨hzS, rfl⟩⟩ + omega + · intro hm + exact hy₁PA ((mem_cls.mp (mem_erase.mp hm).2).2 ▸ hWacc) + have hclsX : cls SA φ X = insert z (cls S c X) := by + rw [hSA, hφ, cls_insert_update_ne hy₁A hXW, hc1, cls_update_self hzA, cls_part hXacc] + have hclsXcard : (cls SA φ X).card = (cls S c X).card + 1 := by + rw [hclsX, card_insert_of_notMem] + intro hm + exact hXW (mem_cls.mp hm).2.symm + have hclsO : ∀ i ∈ PA, i ≠ c z → i ≠ X → cls SA φ i = cls S c i := by + intro i hi hiW hiX + rw [hSA, hφ, cls_insert_update_ne hy₁A hiW, hc1, cls_update_other hiX hiW, cls_part hi] + have hEqA : ∃ cA, IsEq G SA PA cA s := by + by_cases hXlo : X = lo + · refine ⟨φ, hprop, hinto, fun i hi' => ?_⟩ + by_cases hiW : i = c z + · rw [hiW]; exact hclsWcard + by_cases hiX : i = X + · rw [hiX, hclsXcard, hXlo]; exact h.near.card_lo + rw [hclsO i hi' hiW hiX] + exact h.near.card i (Ctx.acc_subset hi') (hXlo ▸ hiX) (fun e => h.hi_not (e ▸ hi')) + · have hXcard : (cls S c X).card = s := h.near.card X (Ctx.acc_subset hXacc) hXlo hXlo_hi + have hnear : IsNear G SA PA φ s lo X := by + refine ⟨hprop, hinto, h.lo_mem_acc, hXacc, Ne.symm hXlo, ?_, ?_, ?_⟩ + · rw [hclsO lo h.lo_mem_acc (Ne.symm hWlo) (Ne.symm hXlo)]; exact h.near.card_lo + · rw [hclsXcard, hXcard] + · intro i hi' hilo hiX + by_cases hiW : i = c z + · rw [hiW]; exact hclsWcard + rw [hclsO i hi' hiW hiX] + exact h.near.card i (Ctx.acc_subset hi') hilo (fun e => h.hi_not (e ▸ hi')) + refine shift_of_acc hnear ?_ + have hp := reach_restrict h (fun a b hab => hab.1) + (hterm (c z) hzT X (mem_erase.mpr ⟨hXW, hXacc⟩)) + refine transfer hp fun a b hab hbX => ?_ + obtain ⟨⟨⟨v, hv, hvmov⟩, haW, hbW⟩, haA, hbA⟩ := hab + rw [mem_cls] at hv + have hvz : v ≠ z := by rintro rfl; exact haW hv.2.symm + have hvy : v ≠ y₁ := by rintro rfl; exact hy₁PA (hv.2 ▸ haA) + refine ⟨v, mem_cls.mpr ⟨mem_insert_of_mem (mem_filter.mpr ⟨hv.1, hv.2 ▸ haA⟩), ?_⟩, ?_⟩ + · rw [hφ, Function.update_of_ne hvy, hc1, Function.update_of_ne hvz]; exact hv.2 + · intro u hu + rw [hclsO b hbA hbW hbX] at hu + exact hvmov u hu + obtain ⟨cA, hcA⟩ := hEqA + refine ⟨_, isEq_combine hcA hg ?_ ?_ (union_sdiff_of_subset Ctx.acc_subset) disjoint_sdiff⟩ + · ext v + constructor + · intro hv + rcases mem_union.mp hv with hv | hv + · rcases mem_insert.mp hv with rfl | hv + · exact hy₁S + · exact (mem_filter.mp hv).1 + · exact (mem_filter.mp (mem_erase.mp hv).2).1 + · intro hv + by_cases hvy : v = y₁ + · subst hvy; exact mem_union_left _ (mem_insert_self _ _) + by_cases hvA : c v ∈ PA + · exact mem_union_left _ (mem_insert_of_mem (mem_filter.mpr ⟨hv, hvA⟩)) + · exact mem_union_right _ + (mem_erase.mpr ⟨hvy, mem_filter.mpr ⟨hv, mem_sdiff.mpr ⟨h.near.into v hv, hvA⟩⟩⟩) + · rw [disjoint_left] + intro v hv1 hv2 + obtain ⟨hvy, hvB⟩ := mem_erase.mp hv2 + rcases mem_insert.mp hv1 with rfl | hvA + · exact hvy rfl + · exact (mem_sdiff.mp (mem_filter.mp hvB).2).2 (mem_filter.mp hvA).2 + +open Classical in +/-- A blocked vertex has a free class after one neighbor is removed. -/ +private lemma exists_free_class {S : Finset V} {P : Finset ℕ} {c : V → ℕ} + {r s lo hi : ℕ} {z y₁ : V} (h : Ctx G S P c r s lo hi) + (hzS : z ∈ S) (hWacc : c z ∈ acc G S P c lo) (hy₁S : y₁ ∈ S) + (hy₁PA : c y₁ ∉ acc G S P c lo) (hadjzy : G.Adj z y₁) + (hnot : ∀ X ∈ acc G S P c lo, X ≠ c z → ¬ Movable G S c z X) (g : V → ℕ) : + ∃ Y ∈ P \ acc G S P c lo, + Movable G ((part S c (P \ acc G S P c lo)).erase y₁) g z Y := by + set PA := acc G S P c lo + set PB := P \ PA + set A := part S c PA + set B := part S c PB + by_contra hcon + simp only [not_exists, not_and] at hcon + have hN1 : (PA.erase (c z)).card ≤ (nbr G A z).card := by + refine le_trans (card_le_card ?_) (card_image_le (f := c)) + intro X hX + obtain ⟨hXW, hXA⟩ := mem_erase.mp hX + have := hnot X hXA hXW + simp only [Movable, not_forall, not_not] at this + obtain ⟨w, hw, hadj⟩ := this + rw [mem_cls] at hw + exact mem_image.mpr ⟨w, mem_nbr.mpr ⟨mem_filter.mpr ⟨hw.1, hw.2 ▸ hXA⟩, hadj⟩, hw.2⟩ + have hN2 : PB.card ≤ (nbr G (B.erase y₁) z).card := by + refine le_trans (card_le_card ?_) (card_image_le (f := g)) + intro Y hY + have := hcon Y hY + simp only [Movable, not_forall, not_not] at this + obtain ⟨w, hw, hadj⟩ := this + rw [mem_cls] at hw + exact mem_image.mpr ⟨w, mem_nbr.mpr ⟨hw.1, hadj⟩, hw.2⟩ + have hsub : nbr G A z ∪ insert y₁ (nbr G (B.erase y₁) z) ⊆ nbr G S z := by + intro w hw + rcases mem_union.mp hw with hw | hw + · obtain ⟨hwA, hadj⟩ := mem_nbr.mp hw + exact mem_nbr.mpr ⟨(mem_filter.mp hwA).1, hadj⟩ + · rcases mem_insert.mp hw with rfl | hw + · exact mem_nbr.mpr ⟨hy₁S, hadjzy⟩ + · obtain ⟨hwB, hadj⟩ := mem_nbr.mp hw + exact mem_nbr.mpr ⟨(mem_filter.mp (mem_erase.mp hwB).2).1, hadj⟩ + have hdis : Disjoint (nbr G A z) (insert y₁ (nbr G (B.erase y₁) z)) := by + rw [disjoint_left] + intro w hw1 hw2 + have hwA := (mem_filter.mp (mem_nbr.mp hw1).1).2 + rcases mem_insert.mp hw2 with rfl | hw2 + · exact hy₁PA hwA + · exact (mem_sdiff.mp (mem_filter.mp (mem_erase.mp (mem_nbr.mp hw2).1).2).2).2 hwA + have hy₁n : y₁ ∉ nbr G (B.erase y₁) z := by simp + have hc := card_le_card hsub + rw [card_union_of_disjoint hdis, card_insert_of_notMem hy₁n] at hc + have hdeg := h.deg z hzS + have hr := h.card_r + have he := card_erase_add_one hWacc + have hk1 : PA.card = (acc G S P c lo).card := rfl + have hk2 : PB.card = (P \ acc G S P c lo).card := rfl + omega + +open Classical in +theorem case2 {S : Finset V} {P : Finset ℕ} {c g : V → ℕ} {r s lo hi U : ℕ} {z y₁ y₂ : V} + (h : Ctx G S P c r s lo hi) + (hterm : ∀ W ∈ T G S P c lo U, ∀ X ∈ (acc G S P c lo).erase W, + ReflTransGen (avoid G S c W) X lo) + (hzS : z ∈ S) (hzT : c z ∈ T G S P c lo U) + (hnot : ∀ X ∈ acc G S P c lo, X ≠ c z → ¬ Movable G S c z X) + (hy₁ : y₁ ∈ Sz G S c (T G S P c lo U) (part S c (P \ acc G S P c lo)) z) + (hy₂ : y₂ ∈ Sz G S c (T G S P c lo U) (part S c (P \ acc G S P c lo)) z) + (hne : y₁ ≠ y₂) (hnadj : ¬ G.Adj y₁ y₂) + (hg : IsEq G ((part S c (P \ acc G S P c lo)).erase y₁) (P \ acc G S P c lo) g s) : + ∃ c' hi', IsNear G S P c' s lo hi' ∧ + (acc G S P c lo).card < (acc G S P c' lo).card := by + set PA := acc G S P c lo with hPA + set PB := P \ PA with hPB + set A := part S c PA with hA + set B := part S c PB with hB + have hWacc : c z ∈ PA := (mem_erase.mp (Ctx.T_subset U hzT)).2 + have hWlo : c z ≠ lo := by + intro e + have hz' := hzT + rw [e] at hz' + exact Ctx.lo_notMem_T U hz' + have hWhi : c z ≠ hi := fun e => h.hi_not (e ▸ hWacc) + have hWcard : (cls S c (c z)).card = s := h.near.card _ (Ctx.acc_subset hWacc) hWlo hWhi + obtain ⟨hy₁B, hsolo⟩ := mem_filter.mp hy₁ + obtain ⟨-, -, -, hsolo₁⟩ := hsolo + obtain ⟨hy₂B, hsolo'⟩ := mem_filter.mp hy₂ + obtain ⟨-, -, -, hsolo₂⟩ := hsolo' + have hy₁S : y₁ ∈ S := (mem_filter.mp hy₁B).1 + have hy₁PB : c y₁ ∈ PB := (mem_filter.mp hy₁B).2 + have hy₁PA : c y₁ ∉ PA := (mem_sdiff.mp hy₁PB).2 + have hzA : z ∈ A := mem_filter.mpr ⟨hzS, hWacc⟩ + have hzB : z ∉ B := fun hh => (mem_sdiff.mp (mem_filter.mp hh).2).2 hWacc + have hy₁A : y₁ ∉ A := fun hh => hy₁PA (mem_filter.mp hh).2 + have hzy : z ≠ y₁ := by rintro rfl; exact hy₁A hzA + have hadjzy : G.Adj z y₁ := by + have : z ∈ nIn G S c y₁ (c z) := by rw [hsolo₁]; exact mem_singleton_self _ + exact (mem_nbr.mp (mem_inter.mp this).1).2.symm + have hPdisj : Disjoint PA PB := disjoint_sdiff + have hPU : PA ∪ PB = P := union_sdiff_of_subset Ctx.acc_subset + have hYex := exists_free_class h hzS hWacc hy₁S hy₁PA hadjzy hnot g + obtain ⟨Y, hYPB, hYmov⟩ := hYex + change Y ∈ PB at hYPB + have hYPA : Y ∉ PA := (mem_sdiff.mp hYPB).2 + -- the new colouring + set SA := insert y₁ (A.erase z) with hSA + set φ := Function.update c y₁ (c z) with hφ + set SB := insert z (B.erase y₁) with hSB + set g' := Function.update g z Y with hg' + have hy₁SA : y₁ ∉ A.erase z := fun hh => hy₁A (mem_erase.mp hh).2 + have hzSB : z ∉ B.erase y₁ := fun hh => hzB (mem_erase.mp hh).2 + have hpropA : Proper G SA φ := by + refine proper_insert_update (proper_mono' h.near.proper + (fun v hv => (mem_filter.mp (mem_erase.mp hv).2).1)) ?_ + intro w hw hadj + rw [mem_cls] at hw + obtain ⟨hwz, hwA⟩ := mem_erase.mp hw.1 + exact hwz (solo_eq hsolo₁ (mem_filter.mp hwA).1 hw.2 hadj) + have hintoA : Into SA φ PA := by + intro v hv + by_cases hvy : v = y₁ + · subst hvy; simpa [hφ] using hWacc + · have hvA : v ∈ A.erase z := (mem_insert.mp hv).resolve_left hvy + rw [hφ, Function.update_of_ne hvy] + exact (mem_filter.mp (mem_erase.mp hvA).2).2 + have hpropB : Proper G SB g' := proper_insert_update hg.proper hYmov + have hintoB : Into SB g' PB := by + intro v hv + by_cases hvz : v = z + · subst hvz; simpa [hg'] using hYPB + · have hvB : v ∈ B.erase y₁ := (mem_insert.mp hv).resolve_left hvz + rw [hg', Function.update_of_ne hvz] + exact hg.into v hvB + have hS : SA ∪ SB = S := by + ext v + constructor + · intro hv + rcases mem_union.mp hv with hv | hv + · rcases mem_insert.mp hv with rfl | hv + · exact hy₁S + · exact (mem_filter.mp (mem_erase.mp hv).2).1 + · rcases mem_insert.mp hv with rfl | hv + · exact hzS + · exact (mem_filter.mp (mem_erase.mp hv).2).1 + · intro hv + by_cases hvy : v = y₁ + · subst hvy; exact mem_union_left _ (mem_insert_self _ _) + by_cases hvz : v = z + · subst hvz; exact mem_union_right _ (mem_insert_self _ _) + by_cases hvA : c v ∈ PA + · exact mem_union_left _ (mem_insert_of_mem (mem_erase.mpr ⟨hvz, mem_filter.mpr ⟨hv, hvA⟩⟩)) + · exact mem_union_right _ (mem_insert_of_mem + (mem_erase.mpr ⟨hvy, mem_filter.mpr ⟨hv, mem_sdiff.mpr ⟨h.near.into v hv, hvA⟩⟩⟩)) + have hdisj : Disjoint SA SB := by + rw [disjoint_left] + intro v hv1 hv2 + rcases mem_insert.mp hv1 with rfl | hv1 + · rcases mem_insert.mp hv2 with e | hv2 + · exact hzy e.symm + · exact (mem_erase.mp hv2).1 rfl + · obtain ⟨hvz, hvA⟩ := mem_erase.mp hv1 + rcases mem_insert.mp hv2 with rfl | hv2 + · exact hvz rfl + · exact (mem_sdiff.mp (mem_filter.mp (mem_erase.mp hv2).2).2).2 (mem_filter.mp hvA).2 + set ψ : V → ℕ := fun v => if v ∈ SA then φ v else g' v with hψ + have hclsA : ∀ i ∈ PA, cls S ψ i = cls SA φ i := fun i hi => + cls_comb_A hintoB hS hPdisj hi + have hclsB : ∀ i ∈ PB, cls S ψ i = cls SB g' i := fun i hi => + cls_comb_B hintoA hS hdisj hPdisj hi + have hclsW : cls S ψ (c z) = insert y₁ ((cls S c (c z)).erase z) := by + rw [hclsA _ hWacc, hSA, hφ, cls_insert_update_self, cls_erase', cls_part hWacc] + have hclsA_ne : ∀ i ∈ PA, i ≠ c z → cls S ψ i = cls S c i := by + intro i hi hiW + rw [hclsA i hi, hSA, hφ, cls_insert_update_ne hy₁SA hiW, cls_erase', cls_part hi] + refine erase_eq_of_notMem fun hm => hiW ?_ + exact (mem_cls.mp hm).2.symm + have hnear : IsNear G S P ψ s lo Y := by + refine ⟨proper_comb hpropA hpropB hintoA hintoB hS hPdisj, + into_comb hintoA hintoB hS hPU, h.near.lo_mem, (mem_sdiff.mp hYPB).1, + fun e => hYPA (e ▸ h.lo_mem_acc), ?_, ?_, ?_⟩ + · rw [hclsA_ne lo h.lo_mem_acc (Ne.symm hWlo)]; exact h.near.card_lo + · rw [hclsB Y hYPB, hSB, hg', cls_insert_update_self, card_insert_of_notMem, hg.card Y hYPB] + exact fun hm => hzSB (mem_cls.mp hm).1 + · intro i hi hilo hiY + by_cases hiA : i ∈ PA + · by_cases hiW : i = c z + · rw [hiW, hclsW, card_insert_of_notMem, card_erase_of_mem (mem_cls.mpr ⟨hzS, rfl⟩), + hWcard] + · have : 0 < s := hWcard ▸ card_pos.mpr ⟨z, mem_cls.mpr ⟨hzS, rfl⟩⟩ + omega + · intro hm + exact hy₁PA ((mem_cls.mp (mem_erase.mp hm).2).2 ▸ hWacc) + · rw [hclsA_ne i hiA hiW] + exact h.near.card i hi hilo (fun e => h.hi_not (e ▸ hiA)) + · have hiB : i ∈ PB := mem_sdiff.mpr ⟨hi, hiA⟩ + rw [hclsB i hiB, hSB, hg', cls_insert_update_ne hzSB hiY] + exact hg.card i hiB + -- accessibility + have hreachA : ∀ X ∈ PA, X ≠ c z → ReflTransGen (Mov G S ψ) X lo := by + intro X hX hXW + have hp := reach_restrict h (fun a b hab => hab.1) + (hterm (c z) hzT X (mem_erase.mpr ⟨hXW, hX⟩)) + refine rtgMono hp fun a b hab => ?_ + obtain ⟨⟨⟨v, hv, hvmov⟩, haW, hbW⟩, haA, hbA⟩ := hab + refine ⟨v, ?_, ?_⟩ + · rw [hclsA_ne a haA haW]; exact hv + · intro u hu + rw [hclsA_ne b hbA hbW] at hu + exact hvmov u hu + have hreachW : ReflTransGen (Mov G S ψ) (c z) lo := by + obtain ⟨j, ⟨w, hw, hwmov⟩, hjW, hjp⟩ := exists_step_avoid (mem_filter.mp hWacc).2 hWlo + have hjr : ReflTransGen (Mov G S c) j lo := rtgMono hjp fun a b hab => hab.1 + have hjacc : j ∈ PA := by + have hjP : j ∈ P := by + by_cases hjl : j = lo + · rw [hjl]; exact h.near.lo_mem + · exact mem_palette_of_reach h.near.into (fun a b h => h) hjr hjl + exact mem_filter.mpr ⟨hjP, hjr⟩ + rw [mem_cls] at hw + have hwz : w ≠ z := by + rintro rfl + exact hnot j hjacc hjW hwmov + refine ReflTransGen.head ⟨w, ?_, ?_⟩ (hreachA j hjacc hjW) + · rw [hclsW]; exact mem_insert_of_mem (mem_erase.mpr ⟨hwz, mem_cls.mpr hw⟩) + · intro u hu + rw [hclsA_ne j hjacc hjW] at hu + exact hwmov u hu + have hsub : PA ⊆ acc G S P ψ lo := by + intro X hX + refine mem_filter.mpr ⟨Ctx.acc_subset hX, ?_⟩ + by_cases hXW : X = c z + · rw [hXW]; exact hreachW + · exact hreachA X hX hXW + have hy₂B' : y₂ ∈ B.erase y₁ := mem_erase.mpr ⟨hne.symm, hy₂B⟩ + have hZPB : g y₂ ∈ PB := hg.into y₂ hy₂B' + have hy₂z : y₂ ≠ z := by rintro rfl; exact hzB hy₂B + have hZ : g y₂ ∈ acc G S P ψ lo := by + refine mem_filter.mpr ⟨(mem_sdiff.mp hZPB).1, ReflTransGen.head ⟨y₂, ?_, ?_⟩ hreachW⟩ + · rw [hclsB _ hZPB, hSB, hg'] + exact mem_cls.mpr ⟨mem_insert_of_mem hy₂B', by rw [Function.update_of_ne hy₂z]⟩ + · intro u hu hadj + rw [hclsW] at hu + rcases mem_insert.mp hu with rfl | hu + · exact hnadj hadj.symm + · obtain ⟨huz, hu⟩ := mem_erase.mp hu + exact huz (solo_eq hsolo₂ (mem_cls.mp hu).1 (mem_cls.mp hu).2 hadj) + refine ⟨ψ, Y, hnear, ?_⟩ + have hc := card_le_card (insert_subset hZ hsub) + rw [card_insert_of_notMem (mem_sdiff.mp hZPB).2] at hc + omega + +end HajnalSzemeredi diff --git a/LeanPool/HajnalSzemeredi/Count.lean b/LeanPool/HajnalSzemeredi/Count.lean new file mode 100644 index 0000000000..e94b440af3 --- /dev/null +++ b/LeanPool/HajnalSzemeredi/Count.lean @@ -0,0 +1,312 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.HajnalSzemeredi.CountDefinitions +public import Mathlib.Algebra.Order.Field.Basic +public import Mathlib.Algebra.BigOperators.Ring.Finset +public import Mathlib.Tactic.Linarith +public import Mathlib.Tactic.FieldSimp +public import Mathlib.Algebra.Order.BigOperators.Group.Finset + +/-! +# Counting inequalities for equitable recolouring + +Split from the upstream counting module to let the structural lemmas build independently. +-/ + +@[expose] public section + +noncomputable section + +open Finset + +namespace HajnalSzemeredi + +variable {V : Type*} {G : SimpleGraph V} + +namespace CountHyp + +variable {S : Finset V} {c : V → ℕ} {PA PB TU : Finset ℕ} {r s : ℕ} + +open Classical in +private theorem mem_part' {Q : Finset ℕ} {v : V} : v ∈ part S c Q ↔ v ∈ S ∧ c v ∈ Q := by + simp [part] + +open Classical in +private theorem card_nbr_split (h : CountHyp G S c PA PB TU r s) (v : V) : + (nbr G S v).card = (nbr G (part S c PA) v).card + (nbr G (part S c PB) v).card := by + rw [← card_union_of_disjoint] + · congr 1 + ext w + simp only [mem_union, mem_nbr, mem_part'] + constructor + · rintro ⟨hw, ha⟩ + rcases mem_union.1 (h.cover w hw) with h1 | h1 + · exact Or.inl ⟨⟨hw, h1⟩, ha⟩ + · exact Or.inr ⟨⟨hw, h1⟩, ha⟩ + · rintro (⟨⟨hw, _⟩, ha⟩ | ⟨⟨hw, _⟩, ha⟩) <;> exact ⟨hw, ha⟩ + · rw [disjoint_left] + intro w h1 h2 + simp only [mem_nbr, mem_part'] at h1 h2 + exact disjoint_left.1 h.disj h1.1.2 h2.1.2 + +open Classical in +private theorem card_nbr_part (v : V) (Q : Finset ℕ) : + (nbr G (part S c Q) v).card = ∑ X ∈ Q, (nIn G S c v X).card := by + rw [← card_biUnion] + · congr 1 + ext w + simp only [mem_nbr, mem_part', mem_biUnion, nIn, mem_inter, mem_cls] + constructor + · rintro ⟨⟨hw, hc⟩, ha⟩ + exact ⟨c w, hc, ⟨hw, ha⟩, hw, rfl⟩ + · rintro ⟨X, hX, ⟨hw, ha⟩, _, rfl⟩ + exact ⟨⟨hw, hX⟩, ha⟩ + · intro i _ j _ hij + exact (cls_disjoint hij).mono inter_subset_right inter_subset_right + +open Classical in +private theorem card_le_nbr_part {v : V} {Q : Finset ℕ} (hQ : Q ⊆ PA) + (hne : ∀ X ∈ Q, (nIn G S c v X).Nonempty) : Q.card ≤ (nbr G (part S c PA) v).card := by + rw [card_nbr_part] + calc Q.card = ∑ X ∈ Q, 1 := by simp + _ ≤ ∑ X ∈ Q, (nIn G S c v X).card := sum_le_sum fun X hX => (hne X hX).card_pos + _ ≤ _ := sum_le_sum_of_subset hQ + +open Classical in +private theorem two_le_nIn_add (h : CountHyp G S c PA PB TU r s) {y : V} + (hy : y ∈ part S c PB) {W : ℕ} (hW : W ∈ TU) : + 2 ≤ (nIn G S c y W).card + + ((cls S c W).filter fun z => IsSolo G S c TU (part S c PB) z y).card := by + have hpos := (h.h21 y hy W (h.sub hW)).card_pos + by_cases h2 : 2 ≤ (nIn G S c y W).card + · omega + · have h1 : (nIn G S c y W).card = 1 := by omega + obtain ⟨a, ha⟩ := card_eq_one.1 h1 + have haW : a ∈ cls S c W := by + have : a ∈ nIn G S c y W := by rw [ha]; exact mem_singleton_self a + exact (mem_inter.1 this).2 + rw [mem_cls] at haW + have : 0 < ((cls S c W).filter fun z => IsSolo G S c TU (part S c PB) z y).card := by + refine card_pos.2 ⟨a, mem_filter.2 ⟨mem_cls.2 haW, haW.1, haW.2 ▸ hW, hy, ?_⟩⟩ + rw [haW.2]; exact ha + omega + +open Classical in +private theorem nIn_eq_filter (y : V) (W : ℕ) : + nIn G S c y W = (cls S c W).filter fun z => G.Adj y z := by + ext z + simp only [nIn, mem_inter, mem_nbr, mem_filter, mem_cls] + tauto + +open Classical in +/-- Desigualdad (2.3): `|S^y| ≥ t - q + 1 + d_B(y)`. -/ +theorem card_Sy (h : CountHyp G S c PA PB TU r s) {y : V} (hy : y ∈ part S c PB) : + TU.card + 1 + (nbr G (part S c PB) y).card ≤ + (Sy G S c TU (part S c PB) y).card + PB.card := by + have hsum : ∑ X ∈ TU, ((cls S c X).filter fun z => IsSolo G S c TU (part S c PB) z y).card ≤ + (Sy G S c TU (part S c PB) y).card := by + rw [← card_biUnion] + · apply card_le_card + intro z hz + simp only [mem_biUnion, mem_filter, mem_cls] at hz + obtain ⟨X, _, ⟨hzS, _⟩, hs⟩ := hz + exact mem_filter.2 ⟨hzS, hs⟩ + · intro i _ j _ hij + exact (cls_disjoint hij).mono (filter_subset _ _) (filter_subset _ _) + have hTU : ∑ X ∈ TU, 2 ≤ ∑ X ∈ TU, ((nIn G S c y X).card + + ((cls S c X).filter fun z => IsSolo G S c TU (part S c PB) z y).card) := + sum_le_sum fun X hX => h.two_le_nIn_add hy hX + rw [sum_add_distrib, sum_const, smul_eq_mul] at hTU + have hrest : (PA \ TU).card ≤ ∑ X ∈ PA \ TU, (nIn G S c y X).card := by + calc (PA \ TU).card = ∑ X ∈ PA \ TU, 1 := by simp + _ ≤ _ := sum_le_sum fun X hX => (h.h21 y hy X (mem_sdiff.1 hX).1).card_pos + have hA := card_nbr_part (G := G) (S := S) (c := c) y PA + rw [← sum_sdiff h.sub] at hA + have hc := card_sdiff_add_card_eq_card h.sub + have h1 := h.card_nbr_split y + have h3 := h.deg y (mem_part'.1 hy).1 + have := h.card_r + omega + +open Classical in +/-- (2.1), forma de grado: `d_B(y) ≤ q - 1` para `y ∈ B`. -/ +theorem deg_B (h : CountHyp G S c PA PB TU r s) {y : V} (hy : y ∈ part S c PB) : + (nbr G (part S c PB) y).card + 1 ≤ PB.card := by + have h1 := h.card_nbr_split y + have h2 := card_le_nbr_part (G := G) (S := S) (c := c) (v := y) (subset_refl PA) (h.h21 y hy) + have h3 := h.deg y (mem_part'.1 hy).1 + have := h.card_r + omega + +open Classical in +/-- **Lema 2.2.** Si ningún vértice solo de `W ∈ TU` es movible a otra clase de `PA`, entonces +`q + 1 ≤ t` y todo `y ∈ B` es solo. -/ +theorem lemma_2_2 (h : CountHyp G S c PA PB TU r s) {W : ℕ} (hW : W ∈ TU) + (hW' : ∀ z ∈ cls S c W, (Sz G S c TU (part S c PB) z).Nonempty → + ∀ X ∈ PA, X ≠ W → ¬ Movable G S c z X) : + PB.card + 1 ≤ TU.card ∧ ∀ y ∈ part S c PB, (Sy G S c TU (part S c PB) y).Nonempty := by + have hq : PB.card + 1 ≤ TU.card := by + by_contra hlt + have hz : ∀ z ∈ cls S c W, (Sz G S c TU (part S c PB) z).card + + (nbr G (part S c PB) z).card ≤ 2 * PB.card := by + intro z hz + have hzS := (mem_cls.1 hz).1 + have hzc := (mem_cls.1 hz).2 + have h1 := h.card_nbr_split z + have h3 := h.deg z hzS + have := h.card_r + by_cases hne : (Sz G S c TU (part S c PB) z).Nonempty + · have hA : (PA.erase W).card ≤ (nbr G (part S c PA) z).card := by + apply card_le_nbr_part (erase_subset _ _) + intro X hX + obtain ⟨hXW, hXP⟩ := mem_erase.1 hX + have hm := hW' z hz hne X hXP hXW + simp only [Movable, not_forall, not_not] at hm + obtain ⟨w, hw, hadj⟩ := hm + exact ⟨w, mem_inter.2 ⟨mem_nbr.2 ⟨(mem_cls.1 hw).1, hadj⟩, hw⟩⟩ + have hsub : Sz G S c TU (part S c PB) z ⊆ nbr G (part S c PB) z := by + intro y hy + obtain ⟨hyB, hs⟩ := mem_filter.1 hy + have : z ∈ nIn G S c y (c z) := by rw [hs.2.2.2]; exact mem_singleton_self z + exact mem_nbr.2 ⟨hyB, ((mem_nbr.1 (mem_inter.1 this).1).2).symm⟩ + have := card_le_card hsub + have := card_erase_of_mem (h.sub hW) + have := card_pos.2 ⟨W, h.sub hW⟩ + omega + · rw [not_nonempty_iff_eq_empty.1 hne, card_empty] + have := h.h22 z hzS (hzc ▸ hW) + omega + have hupper := sum_le_sum hz + rw [sum_const, smul_eq_mul, h.size W hW, sum_add_distrib] at hupper + have hlow : ∑ y ∈ part S c PB, 2 ≤ ∑ y ∈ part S c PB, ((nIn G S c y W).card + + ((cls S c W).filter fun z => IsSolo G S c TU (part S c PB) z y).card) := + sum_le_sum fun y hy => h.two_le_nIn_add hy hW + rw [sum_const, smul_eq_mul, h.card_B, sum_add_distrib] at hlow + have e1 : ∑ z ∈ cls S c W, (nbr G (part S c PB) z).card = + ∑ y ∈ part S c PB, (nIn G S c y W).card := by + simp only [nIn_eq_filter, nbr, card_filter] + rw [sum_comm] + refine sum_congr rfl fun y _ => sum_congr rfl fun z _ => ?_ + simp only [G.adj_comm] + have e2 : ∑ z ∈ cls S c W, (Sz G S c TU (part S c PB) z).card = + ∑ y ∈ part S c PB, + ((cls S c W).filter fun z => IsSolo G S c TU (part S c PB) z y).card := by + simp only [Sz, card_filter] + rw [sum_comm] + rw [e1, e2] at hupper + rw [Nat.mul_left_comm s 2 PB.card, Nat.mul_comm s PB.card] at hupper + omega + refine ⟨hq, fun y hy => ?_⟩ + have := h.card_Sy hy + exact card_pos.1 (by omega) + +open Classical in +/-- **Lema 2.3.** Existe un vértice solo `z` (con color en `TU`) que es movible a otra clase de +`PA`, o que tiene dos vecinos especiales distintos no adyacentes. -/ +theorem lemma_2_3 (h : CountHyp G S c PA PB TU r s) : + ∃ z ∈ S, c z ∈ TU ∧ (Sz G S c TU (part S c PB) z).Nonempty ∧ + ((∃ X ∈ PA, X ≠ c z ∧ Movable G S c z X) ∨ + ∃ y₁ ∈ Sz G S c TU (part S c PB) z, ∃ y₂ ∈ Sz G S c TU (part S c PB) z, + y₁ ≠ y₂ ∧ ¬ G.Adj y₁ y₂) := by + by_contra hcon + have hnm : ∀ z ∈ S, c z ∈ TU → (Sz G S c TU (part S c PB) z).Nonempty → + ∀ X ∈ PA, X ≠ c z → ¬ Movable G S c z X := + fun z hz hc hne X hX hXz hm => hcon ⟨z, hz, hc, hne, Or.inl ⟨X, hX, hXz, hm⟩⟩ + have hcl : ∀ z ∈ S, c z ∈ TU → ∀ y₁ ∈ Sz G S c TU (part S c PB) z, + ∀ y₂ ∈ Sz G S c TU (part S c PB) z, y₁ ≠ y₂ → G.Adj y₁ y₂ := + fun z hz hc y₁ h₁ y₂ h₂ hne => + by_contra fun ha => hcon ⟨z, hz, hc, ⟨y₁, h₁⟩, Or.inr ⟨y₁, h₁, y₂, h₂, hne, ha⟩⟩ + obtain ⟨W, hW⟩ := h.ne + obtain ⟨hq, -⟩ := h.lemma_2_2 hW fun z hz hne X hX hXW => + hnm z (mem_cls.1 hz).1 ((mem_cls.1 hz).2 ▸ hW) hne X hX (by rw [(mem_cls.1 hz).2]; exact hXW) + have hswap : ∑ y ∈ part S c PB, ∑ z ∈ Sy G S c TU (part S c PB) y, + ((PB.card : ℚ) / (Sz G S c TU (part S c PB) z).card) = + ∑ z ∈ S.filter (fun z => c z ∈ TU), ∑ y ∈ Sz G S c TU (part S c PB) z, + ((PB.card : ℚ) / (Sz G S c TU (part S c PB) z).card) := by + apply sum_comm' + intro y z + simp only [Sy, Sz, mem_filter] + constructor + · rintro ⟨hy, hzS, hs⟩ + exact ⟨⟨hy, hs⟩, hzS, hs.2.1⟩ + · rintro ⟨⟨hy, hs⟩, hzS, _⟩ + exact ⟨hy, hzS, hs⟩ + have hup : ∑ z ∈ S.filter (fun z => c z ∈ TU), ∑ y ∈ Sz G S c TU (part S c PB) z, + ((PB.card : ℚ) / (Sz G S c TU (part S c PB) z).card) ≤ + ∑ z ∈ S.filter (fun z => c z ∈ TU), (PB.card : ℚ) := by + apply sum_le_sum + intro z _ + rw [sum_const, nsmul_eq_mul] + rcases Nat.eq_zero_or_pos (Sz G S c TU (part S c PB) z).card with h0 | h0 + · rw [h0]; simp + · apply le_of_eq + have : ((Sz G S c TU (part S c PB) z).card : ℚ) ≠ 0 := by positivity + field_simp + have hA' : (S.filter fun z => c z ∈ TU).card = TU.card * s := by + rw [card_eq_sum_card_fiberwise (f := c) (s := S.filter fun z => c z ∈ TU) (t := TU) + (fun z hz => (mem_filter.1 hz).2)] + rw [sum_congr rfl (g := fun _ => s)] + · simp + intro X hX + rw [← h.size X hX] + congr 1 + ext z + simp only [mem_filter, mem_cls] + constructor + · rintro ⟨⟨a, _⟩, b⟩; exact ⟨a, b⟩ + · rintro ⟨a, b⟩; exact ⟨⟨a, b ▸ hX⟩, b⟩ + have hlo : ∀ y ∈ part S c PB, (TU.card : ℚ) ≤ ∑ z ∈ Sy G S c TU (part S c PB) y, + ((PB.card : ℚ) / (Sz G S c TU (part S c PB) z).card) := by + intro y hy + have hSy := h.card_Sy hy + have hdB := h.deg_B hy + have hle : ∀ z ∈ Sy G S c TU (part S c PB) y, (Sz G S c TU (part S c PB) z).card ≤ + (nbr G (part S c PB) y).card + 1 ∧ 0 < (Sz G S c TU (part S c PB) z).card := by + intro z hz + obtain ⟨hzS, hs⟩ := mem_filter.1 hz + have hyz : y ∈ Sz G S c TU (part S c PB) z := mem_filter.2 ⟨hy, hs⟩ + refine ⟨?_, card_pos.2 ⟨y, hyz⟩⟩ + have hsub : Sz G S c TU (part S c PB) z ⊆ insert y (nbr G (part S c PB) y) := by + intro y' hy' + by_cases e : y' = y + · rw [e]; exact mem_insert_self _ _ + · exact mem_insert_of_mem (mem_nbr.2 ⟨(mem_filter.1 hy').1, + hcl z hzS hs.2.1 y hyz y' hy' (Ne.symm e)⟩) + exact (card_le_card hsub).trans (card_insert_le _ _) + have hSyq : (TU.card : ℚ) + 1 + (nbr G (part S c PB) y).card ≤ + (Sy G S c TU (part S c PB) y).card + PB.card := by exact_mod_cast hSy + have hdBq : ((nbr G (part S c PB) y).card : ℚ) + 1 ≤ PB.card := by exact_mod_cast hdB + have hqq : (PB.card : ℚ) + 1 ≤ TU.card := by exact_mod_cast hq + calc (TU.card : ℚ) ≤ (Sy G S c TU (part S c PB) y).card * + ((PB.card : ℚ) / ((nbr G (part S c PB) y).card + 1)) := by + rw [mul_div_assoc', le_div_iff₀ (by positivity)] + nlinarith [mul_nonneg (show (0:ℚ) ≤ TU.card - PB.card by linarith) + (show (0:ℚ) ≤ PB.card - ((nbr G (part S c PB) y).card + 1) by linarith), + mul_le_mul_of_nonneg_right hSyq (Nat.cast_nonneg (α := ℚ) PB.card)] + _ = ∑ z ∈ Sy G S c TU (part S c PB) y, + ((PB.card : ℚ) / ((nbr G (part S c PB) y).card + 1)) := by + rw [sum_const, nsmul_eq_mul] + _ ≤ _ := sum_le_sum fun z hz => div_le_div_of_nonneg_left (by positivity) + (by exact_mod_cast (hle z hz).2) (by exact_mod_cast (hle z hz).1) + have hL : (TU.card : ℚ) * (part S c PB).card ≤ ∑ y ∈ part S c PB, + ∑ z ∈ Sy G S c TU (part S c PB) y, + ((PB.card : ℚ) / (Sz G S c TU (part S c PB) z).card) := by + calc + _ = ∑ y ∈ part S c PB, (TU.card : ℚ) := by + rw [sum_const, nsmul_eq_mul, mul_comm] + _ ≤ _ := sum_le_sum hlo + rw [hswap] at hL + have key := hL.trans hup + rw [sum_const, nsmul_eq_mul, hA', h.card_B] at key + push_cast at key + have : (1 : ℚ) ≤ TU.card := by exact_mod_cast (show 1 ≤ TU.card by omega) + nlinarith only [key, this] + +end CountHyp + +end HajnalSzemeredi diff --git a/LeanPool/HajnalSzemeredi/CountDefinitions.lean b/LeanPool/HajnalSzemeredi/CountDefinitions.lean new file mode 100644 index 0000000000..faa8a44b79 --- /dev/null +++ b/LeanPool/HajnalSzemeredi/CountDefinitions.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.HajnalSzemeredi.Defs + +/-! +Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit +`ba34061e3cf12dfc8297610d5d7b3f0afac7ec54`; import paths adapted. + +# Definitions for the equitable-colouring counting argument + +Abstraemos la situación del artículo en `CountHyp`: + +* `PA` (clases accesibles) y `PB` (inaccesibles) son paletas disjuntas que cubren los colores de + `S`; `A`, `B` son los vértices con color en `PA`, `PB`; +* `TU ⊆ PA` es la familia `𝒜'`, con `t = |TU|` clases, todas de tamaño `s`; +* `q = |PB|`, `|B| = q s + 1`, grado máximo `r` con `r + 1 = |PA| + |PB|`; +* (2.1): todo `y ∈ B` tiene un vecino en cada clase de `PA`; +* (2.2): todo `x` con color en `TU` tiene al menos `|PA| - 1 - t` vecinos en `A`. + +Una arista `zy` (`z` con color `W ∈ TU`, `y ∈ B`) es *solo* si `z` es el único vecino de `y` en +la clase `W`. `Sz z` son los vecinos especiales de `z` (en `B`) y `Sy y` los de `y` (en `A'`). +-/ + +@[expose] public section + +noncomputable section + +open Finset + +namespace HajnalSzemeredi + +variable {V : Type*} {G : SimpleGraph V} + +open Classical in +/-- Vértices de `S` con color en la paleta `Q`. -/ +def part (S : Finset V) (c : V → ℕ) (Q : Finset ℕ) : Finset V := S.filter fun v => c v ∈ Q + +open Classical in +/-- Vecinos de `y` en la clase `W`. -/ +def nIn (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (y : V) (W : ℕ) : Finset V := + nbr G S y ∩ cls S c W + +open Classical in +/-- `zy` es una arista solo (respecto a la familia `TU` y al conjunto `B`). -/ +def IsSolo (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (TU : Finset ℕ) (B : Finset V) + (z y : V) : Prop := + z ∈ S ∧ c z ∈ TU ∧ y ∈ B ∧ nIn G S c y (c z) = {z} + +open Classical in +/-- Vecinos especiales de `z`. -/ +def Sz (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (TU : Finset ℕ) (B : Finset V) (z : V) : + Finset V := B.filter fun y => IsSolo G S c TU B z y + +open Classical in +/-- Vecinos especiales de `y`. -/ +def Sy (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (TU : Finset ℕ) (B : Finset V) (y : V) : + Finset V := S.filter fun z => IsSolo G S c TU B z y + +open Classical in +/-- Hipótesis de la parte de conteo. -/ +structure CountHyp (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (PA PB TU : Finset ℕ) + (r s : ℕ) : Prop where + disj : Disjoint PA PB + cover : ∀ v ∈ S, c v ∈ PA ∪ PB + sub : TU ⊆ PA + ne : TU.Nonempty + card_r : r + 1 = PA.card + PB.card + deg : DegLe G S r + size : ∀ W ∈ TU, (cls S c W).card = s + card_B : (part S c PB).card = PB.card * s + 1 + /-- (2.1) -/ + h21 : ∀ y ∈ part S c PB, ∀ X ∈ PA, (nIn G S c y X).Nonempty + /-- (2.2) -/ + h22 : ∀ x ∈ S, c x ∈ TU → PA.card ≤ (nbr G (part S c PA) x).card + TU.card + 1 + +end HajnalSzemeredi diff --git a/LeanPool/HajnalSzemeredi/Defs.lean b/LeanPool/HajnalSzemeredi/Defs.lean new file mode 100644 index 0000000000..2bfefa7a1f --- /dev/null +++ b/LeanPool/HajnalSzemeredi/Defs.lean @@ -0,0 +1,205 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Basic +public import Mathlib.Data.Finset.Card +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Logic.Relation +public import Mathlib.Order.Interval.Finset.Nat + +/-! +Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit +`ba34061e3cf12dfc8297610d5d7b3f0afac7ec54`; import paths adapted. + +# Definiciones para la prueba de Kierstead–Kostochka del teorema de Hajnal–Szemerédi + +Trabajamos con un grafo `G` sobre un tipo ambiente `V` y un conjunto finito de vértices +`S : Finset V` (el grafo considerado es el inducido `G[S]`). Una coloración es una función +`c : V → ℕ`; sólo importan sus valores sobre `S`, y la paleta es un `Finset ℕ`. + +Esto permite pasar a subgrafos inducidos (`A ∪ {y₁}`, `B \ {y₁}` en el artículo) y cambiar la +paleta sin cambiar de tipo. + +Referencia: H. A. Kierstead, A. V. Kostochka, *A short proof of the Hajnal–Szemerédi theorem on +equitable colouring*, Combin. Probab. Comput. 17 (2008) 265–270. +-/ + +@[expose] public section + +noncomputable section + +open Finset + +namespace HajnalSzemeredi + +variable {V : Type*} (G : SimpleGraph V) + +open Classical in +/-- La clase de color `i` de `c` dentro de `S`. -/ +def cls (S : Finset V) (c : V → ℕ) (i : ℕ) : Finset V := S.filter fun v => c v = i + +open Classical in +/-- Vecinos de `v` dentro de `S`. -/ +def nbr (S : Finset V) (v : V) : Finset V := S.filter fun w => G.Adj v w + +open Classical in +/-- `c` es propia sobre `S`. -/ +def Proper (S : Finset V) (c : V → ℕ) : Prop := ∀ v ∈ S, ∀ w ∈ S, G.Adj v w → c v ≠ c w + +open Classical in +/-- `c` toma valores en la paleta `P` sobre `S`. -/ +def Into (S : Finset V) (c : V → ℕ) (P : Finset ℕ) : Prop := ∀ v ∈ S, c v ∈ P + +open Classical in +/-- Grado máximo de `G[S]` a lo más `r`. -/ +def DegLe (S : Finset V) (r : ℕ) : Prop := ∀ v ∈ S, (nbr G S v).card ≤ r + +open Classical in +/-- Número de pares ordenados adyacentes en `S` (el doble del número de aristas de `G[S]`). -/ +def edgeCount (S : Finset V) : ℕ := (S.offDiag.filter fun p => G.Adj p.1 p.2).card + +open Classical in +/-- Coloración equitativa de `S` con paleta `P`, todas las clases de tamaño exactamente `s`. -/ +structure IsEq (S : Finset V) (P : Finset ℕ) (c : V → ℕ) (s : ℕ) : Prop where + proper : Proper G S c + into : Into S c P + card : ∀ i ∈ P, (cls S c i).card = s + +open Classical in +/-- Coloración casi equitativa: todas las clases de tamaño `s`, salvo una clase pequeña `lo` +de tamaño `s - 1` y una clase grande `hi` de tamaño `s + 1`. -/ +structure IsNear (S : Finset V) (P : Finset ℕ) (c : V → ℕ) (s lo hi : ℕ) : Prop where + proper : Proper G S c + into : Into S c P + lo_mem : lo ∈ P + hi_mem : hi ∈ P + lo_ne_hi : lo ≠ hi + card_lo : (cls S c lo).card + 1 = s + card_hi : (cls S c hi).card = s + 1 + card : ∀ i ∈ P, i ≠ lo → i ≠ hi → (cls S c i).card = s + +open Classical in +/-- `v` es *movible* a la clase `j`: no tiene vecinos en ella. -/ +def Movable (S : Finset V) (c : V → ℕ) (v : V) (j : ℕ) : Prop := + ∀ w ∈ cls S c j, ¬ G.Adj v w + +open Classical in +/-- Arco `i → j` del digrafo auxiliar `H(G, c)`: algún vértice de la clase `i` es movible a `j`. -/ +def Mov (S : Finset V) (c : V → ℕ) (i j : ℕ) : Prop := ∃ v ∈ cls S c i, Movable G S c v j + +open Classical in +/-- Clases accesibles: las que alcanzan a `lo` en `H(G, c)`. -/ +def acc (S : Finset V) (P : Finset ℕ) (c : V → ℕ) (lo : ℕ) : Finset ℕ := + P.filter fun i => Relation.ReflTransGen (Mov G S c) i lo + +/-! ### Lemas básicos sobre clases -/ + +variable {G} + +open Classical in +@[simp] lemma mem_cls {S : Finset V} {c : V → ℕ} {i : ℕ} {v : V} : + v ∈ cls S c i ↔ v ∈ S ∧ c v = i := by + simp [cls] + +open Classical in +lemma cls_subset (S : Finset V) (c : V → ℕ) (i : ℕ) : cls S c i ⊆ S := filter_subset _ _ + +open Classical in +@[simp] lemma mem_nbr {S : Finset V} {v w : V} : w ∈ nbr G S v ↔ w ∈ S ∧ G.Adj v w := by + simp [nbr] + +open Classical in +lemma cls_disjoint {S : Finset V} {c : V → ℕ} {i j : ℕ} (h : i ≠ j) : + Disjoint (cls S c i) (cls S c j) := by + rw [Finset.disjoint_left] + intro v hi hj + rw [mem_cls] at hi hj + exact h (hi.2.symm.trans hj.2) + +open Classical in +/-- Las clases de la paleta particionan `S`: la suma de sus tamaños es `|S|`. -/ +lemma sum_card_cls {S : Finset V} {c : V → ℕ} {P : Finset ℕ} (h : Into S c P) : + ∑ i ∈ P, (cls S c i).card = S.card := by + rw [← Finset.card_biUnion] + · congr 1 + ext v + simp only [mem_biUnion, mem_cls] + exact ⟨fun ⟨_, _, hv, _⟩ => hv, fun hv => ⟨c v, h v hv, hv, rfl⟩⟩ + · intro i _ j _ hij + exact cls_disjoint hij + +/-! ### Mover un vértice a otra clase -/ + +section Move + +variable {S : Finset V} {c : V → ℕ} {v : V} {j : ℕ} + +open Classical in +lemma cls_update_self (hv : v ∈ S) : + cls S (Function.update c v j) j = insert v (cls S c j) := by + ext w + by_cases hw : w = v + · subst hw; simp [hv] + · simp [hw] + +open Classical in +lemma cls_update_old (hv : v ∈ S) (hj : c v ≠ j) : + cls S (Function.update c v j) (c v) = (cls S c (c v)).erase v := by + ext w + by_cases hw : w = v + · subst hw; simp [Ne.symm hj] + · simp [hw] + +open Classical in +lemma cls_update_other {k : ℕ} (hk : k ≠ j) (hk' : k ≠ c v) : + cls S (Function.update c v j) k = cls S c k := by + ext w + by_cases hw : w = v + · subst hw; simp [Ne.symm hk, Ne.symm hk'] + · simp [hw] + +open Classical in +lemma card_cls_update_self (hv : v ∈ S) (hj : c v ≠ j) : + (cls S (Function.update c v j) j).card = (cls S c j).card + 1 := by + rw [cls_update_self hv, card_insert_of_notMem] + simp [hj] + +open Classical in +lemma card_cls_update_old (hv : v ∈ S) (hj : c v ≠ j) : + (cls S (Function.update c v j) (c v)).card + 1 = (cls S c (c v)).card := by + rw [cls_update_old hv hj, card_erase_add_one] + simp [hv] + +open Classical in +lemma into_update {P : Finset ℕ} (h : Into S c P) (hj : j ∈ P) : + Into S (Function.update c v j) P := by + intro w hw + by_cases hwv : w = v + · subst hwv; simpa using hj + · simpa [hwv] using h w hw + +open Classical in +/-- Mover un vértice movible preserva la propiedad. -/ +lemma proper_update (h : Proper G S c) (hmov : Movable G S c v j) : + Proper G S (Function.update c v j) := by + intro a ha b hb hab + by_cases hav : a = v + · subst hav + have hbv : b ≠ a := fun h => G.loopless.irrefl _ (h ▸ hab) + simp only [Function.update_self, Function.update_of_ne hbv] + intro hjb + exact hmov b (mem_cls.mpr ⟨hb, hjb.symm⟩) hab + · by_cases hbv : b = v + · subst hbv + simp only [Function.update_self, Function.update_of_ne hav] + intro hja + exact hmov a (mem_cls.mpr ⟨ha, hja⟩) hab.symm + · simpa [Function.update_of_ne hav, Function.update_of_ne hbv] using h a ha b hb hab + +end Move + +end HajnalSzemeredi diff --git a/LeanPool/HajnalSzemeredi/Final.lean b/LeanPool/HajnalSzemeredi/Final.lean new file mode 100644 index 0000000000..fc5424a7fd --- /dev/null +++ b/LeanPool/HajnalSzemeredi/Final.lean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.HajnalSzemeredi.Main +public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex +public import Mathlib.Combinatorics.SimpleGraph.Finite +public import Mathlib.Data.Fintype.Sum + +/-! +Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit +`ba34061e3cf12dfc8297610d5d7b3f0afac7ec54`; import paths adapted. + +# Teorema de Hajnal–Szemerédi + +* `hajnalSzemeredi_exact`: si `|V| = s (r + 1)` y `Δ(G) ≤ r`, hay una `(r+1)`-coloración propia + cuyas clases tienen todas exactamente `s` vértices (forma del problema de Erdős #914). +* `hajnalSzemeredi`: si `Δ(G) ≤ r`, hay una `(r+1)`-coloración propia equitativa (los tamaños de + dos clases cualesquiera difieren en a lo más uno). + +La forma general se reduce a la exacta agregando un `K_p` disjunto (`p < r + 1`) para que el +número de vértices sea divisible por `r + 1`; cada clase contiene a lo más un vértice agregado. +-/ + +@[expose] public section + +noncomputable section + +open Finset + +namespace HajnalSzemeredi + +variable {V : Type*} [Fintype V] + +open Classical in +/-- Pasar del grado de Mathlib a `DegLe` sobre `univ`. -/ +lemma degLe_univ (G : SimpleGraph V) [DecidableRel G.Adj] {r : ℕ} (h : ∀ v, G.degree v ≤ r) : + DegLe G univ r := by + intro v _ + refine le_trans (card_le_card fun w hw => ?_) ((G.card_neighborFinset_eq_degree v).le.trans (h v)) + rw [SimpleGraph.mem_neighborFinset] + exact (mem_nbr.mp hw).2 + +open Classical in +/-- Forma exacta. -/ +theorem hajnalSzemeredi_exact (G : SimpleGraph V) [DecidableRel G.Adj] (r s : ℕ) + (hcard : Fintype.card V = s * (r + 1)) (h : ∀ v, G.degree v ≤ r) : + ∃ C : G.Coloring (Fin (r + 1)), ∀ i, (univ.filter fun v => C v = i).card = s := by + obtain ⟨c, hc⟩ := core _ G univ (range (r + 1)) r s rfl (card_range _) + (by rw [card_univ, hcard]) (degLe_univ G h) + have hlt : ∀ v, c v < r + 1 := fun v => mem_range.mp (hc.into v (mem_univ v)) + refine ⟨SimpleGraph.Coloring.mk (fun v => ⟨c v, hlt v⟩) fun {u v} huv heq => + hc.proper u (mem_univ u) v (mem_univ v) huv (congrArg Fin.val heq), fun i => ?_⟩ + refine Eq.trans ?_ (hc.card i (mem_range.mpr i.isLt)) + congr 1 + +open Classical in +/-- Adyacencia del grafo con un `K_p` disjunto agregado. -/ +def padAdj (G : SimpleGraph V) (p : ℕ) : V ⊕ Fin p → V ⊕ Fin p → Prop + | .inl u, .inl v => G.Adj u v + | .inr i, .inr j => i ≠ j + | _, _ => False + +open Classical in +/-- `G ⊔ K_p` (unión disjunta). -/ +def pad (G : SimpleGraph V) (p : ℕ) : SimpleGraph (V ⊕ Fin p) where + Adj := padAdj G p + symm := ⟨fun a b h => by + cases a <;> cases b <;> simp only [padAdj] at h ⊢ + · exact h.symm + · exact Ne.symm h⟩ + loopless := ⟨fun a h => by + cases a <;> simp only [padAdj] at h + · exact G.loopless.irrefl _ h + · exact h rfl⟩ + +open Classical in +lemma card_classes_split {W : Type*} [DecidableEq W] {p : ℕ} (f : V ⊕ Fin p → W) (i : W) : + (univ.filter fun w => f w = i).card = + (univ.filter fun v => f (.inl v) = i).card + (univ.filter fun j => f (.inr j) = i).card := by + simp only [card_filter, Fintype.sum_sum_type] + +open Classical in +/-- **Teorema de Hajnal–Szemerédi.** -/ +theorem hajnalSzemeredi (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℕ) + (h : ∀ v, G.degree v ≤ r) : + ∃ C : G.Coloring (Fin (r + 1)), ∀ i j : Fin (r + 1), + (univ.filter fun v => C v = i).card ≤ (univ.filter fun v => C v = j).card + 1 := by + -- `n + p = s (r + 1)` con `p ≤ r` + obtain ⟨s, p, hsp, hp⟩ : ∃ s p : ℕ, Fintype.card V + p = s * (r + 1) ∧ p ≤ r := by + have e := Nat.div_add_mod (Fintype.card V + r) (r + 1) + have hm := Nat.mod_lt (Fintype.card V + r) (by omega : 0 < r + 1) + refine ⟨(Fintype.card V + r) / (r + 1), + (r + 1) * ((Fintype.card V + r) / (r + 1)) - Fintype.card V, ?_, ?_⟩ + · have e' : (r + 1) * ((Fintype.card V + r) / (r + 1)) = + (Fintype.card V + r) / (r + 1) * (r + 1) := Nat.mul_comm _ _ + omega + · omega + have hdeg : ∀ w, (pad G p).degree w ≤ r := by + intro w + rw [← (pad G p).card_neighborFinset_eq_degree] + cases w with + | inl u => + refine le_trans (card_le_card (t := (G.neighborFinset u).map Function.Embedding.inl) + fun x hx => ?_) ?_ + · rw [SimpleGraph.mem_neighborFinset] at hx + cases x with + | inl v => + exact mem_map_of_mem _ ((G.mem_neighborFinset u v).mpr hx) + | inr j => exact absurd hx (by simp [pad, padAdj]) + · rw [card_map, G.card_neighborFinset_eq_degree]; exact h u + | inr i => + refine le_trans (card_le_card (t := (univ.erase i).map Function.Embedding.inr) + fun x hx => ?_) ?_ + · rw [SimpleGraph.mem_neighborFinset] at hx + cases x with + | inl v => exact absurd hx (by simp [pad, padAdj]) + | inr j => + have : i ≠ j := hx + exact mem_map_of_mem _ (mem_erase.mpr ⟨Ne.symm this, mem_univ _⟩) + · rw [card_map, card_erase_of_mem (mem_univ _), card_univ, Fintype.card_fin]; omega + obtain ⟨C', hC'⟩ := hajnalSzemeredi_exact (pad G p) r s + (by rw [Fintype.card_sum, Fintype.card_fin, hsp]) hdeg + -- restricción a `V` + refine ⟨SimpleGraph.Coloring.mk (fun v => C' (.inl v)) fun {u v} huv => + C'.valid (show (pad G p).Adj (.inl u) (.inl v) from huv), fun i j => ?_⟩ + -- cada clase tiene a lo más un vértice agregado + have hb : ∀ i, (univ.filter fun t : Fin p => C' (.inr t) = i).card ≤ 1 := by + intro i + refine card_le_one.mpr fun a ha b hb => ?_ + by_contra hab + have hadj : (pad G p).Adj (.inr a) (.inr b) := hab + exact C'.valid hadj (by rw [(mem_filter.mp ha).2, (mem_filter.mp hb).2]) + have ai : ∀ i, (univ.filter fun v : V => C' (.inl v) = i).card + + (univ.filter fun t : Fin p => C' (.inr t) = i).card = s := by + intro i + rw [← hC' i] + convert (card_classes_split C' i).symm + have key : (univ.filter fun v : V => C' (.inl v) = i).card ≤ + (univ.filter fun v : V => C' (.inl v) = j).card + 1 := by + have := ai i; have := ai j; have := hb i; have := hb j + omega + convert key using 3 <;> rfl + +end HajnalSzemeredi diff --git a/LeanPool/HajnalSzemeredi/Imports.lean b/LeanPool/HajnalSzemeredi/Imports.lean new file mode 100644 index 0000000000..8619aa9d85 --- /dev/null +++ b/LeanPool/HajnalSzemeredi/Imports.lean @@ -0,0 +1,18 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +module -- shake: keep-all --deprecated_module: ignore + +-- Generated project imports; run `lake exe mk_all`. +public import LeanPool.HajnalSzemeredi +public import LeanPool.HajnalSzemeredi.Cases +public import LeanPool.HajnalSzemeredi.Count +public import LeanPool.HajnalSzemeredi.CountDefinitions +public import LeanPool.HajnalSzemeredi.Defs +public import LeanPool.HajnalSzemeredi.Final +public import LeanPool.HajnalSzemeredi.Main +public import LeanPool.HajnalSzemeredi.Reach +public import LeanPool.HajnalSzemeredi.Shift +public import LeanPool.HajnalSzemeredi.Structure diff --git a/LeanPool/HajnalSzemeredi/Main.lean b/LeanPool/HajnalSzemeredi/Main.lean new file mode 100644 index 0000000000..ce952d5a21 --- /dev/null +++ b/LeanPool/HajnalSzemeredi/Main.lean @@ -0,0 +1,274 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.HajnalSzemeredi.Cases +public import LeanPool.HajnalSzemeredi.Count + +/-! +Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit +`ba34061e3cf12dfc8297610d5d7b3f0afac7ec54`; import paths adapted. + +# Teorema 2.4 de Kierstead–Kostochka (forma divisible) + +`core`: si `|S| = s (r + 1)`, `|P| = r + 1` y `G[S]` tiene grado máximo `≤ r`, existe una +coloración propia de `S` con paleta `P` cuyas clases tienen todas tamaño `s`. + +Inducción primaria en el número de aristas de `G[S]`; inducción secundaria (`main_lemma`) en el +número `q` de clases inaccesibles de una coloración casi equitativa. +-/ + +@[expose] public section + +noncomputable section + +open Finset Relation + +namespace HajnalSzemeredi + +variable {V : Type*} {G : SimpleGraph V} + +open Classical in +/-- Hechos sobre `B⁻ = B \ {y₁}` necesarios para aplicar la hipótesis de inducción primaria. -/ +lemma bminus {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} {TU : Finset ℕ} + (h : Ctx G S P c r s lo hi) + (hch : CountHyp G S c (acc G S P c lo) (P \ acc G S P c lo) TU r s) {y₁ : V} + (hy₁ : y₁ ∈ part S c (P \ acc G S P c lo)) : + (part S c (P \ acc G S P c lo)).erase y₁ ⊆ S ∧ + edgeCount G ((part S c (P \ acc G S P c lo)).erase y₁) < edgeCount G S ∧ + ((part S c (P \ acc G S P c lo)).erase y₁).card = + s * ((P \ acc G S P c lo).card - 1 + 1) ∧ + DegLe G ((part S c (P \ acc G S P c lo)).erase y₁) ((P \ acc G S P c lo).card - 1) := by + set PB := P \ acc G S P c lo + set B := part S c PB + have hBS : B.erase y₁ ⊆ S := (erase_subset _ _).trans (filter_subset _ _) + have hPB : 1 ≤ PB.card := card_pos.mpr ⟨hi, h.hi_mem_B⟩ + have hs : 1 ≤ s := by have := h.near.card_lo; omega + have hcard : (B.erase y₁).card = s * (PB.card - 1 + 1) := by + have hB : B.card = PB.card * s + 1 := h.card_B + rw [card_erase_of_mem hy₁, hB, Nat.sub_add_cancel hPB, Nat.add_sub_cancel, Nat.mul_comm] + refine ⟨hBS, ?_, hcard, ?_⟩ + · -- hay una arista entre `B⁻` y la clase `lo` + obtain ⟨y, hy⟩ : (B.erase y₁).Nonempty := by + rw [← card_pos, hcard]; exact Nat.mul_pos hs (Nat.succ_pos _) + have hyB := (mem_erase.mp hy).2 + obtain ⟨w, hw⟩ := h.h21 hyB h.lo_mem_acc + rw [nIn, mem_inter, mem_nbr, mem_cls] at hw + have hwB : w ∉ B.erase y₁ := by + intro hwB + have := (mem_filter.mp (mem_erase.mp hwB).2).2 + rw [hw.2.2] at this + exact (mem_sdiff.mp this).2 h.lo_mem_acc + apply card_lt_card + refine ⟨fun p hp => ?_, fun hsub => ?_⟩ + · obtain ⟨hp, hadj⟩ := mem_filter.mp hp + obtain ⟨h1, h2, h3⟩ := mem_offDiag.mp hp + exact mem_filter.mpr ⟨mem_offDiag.mpr ⟨hBS h1, hBS h2, h3⟩, hadj⟩ + · have hyw : (y, w) ∈ (S.offDiag.filter fun p => G.Adj p.1 p.2) := + mem_filter.mpr ⟨mem_offDiag.mpr ⟨hBS hy, hw.1.1, hw.1.2.ne⟩, hw.1.2⟩ + exact hwB (mem_offDiag.mp (mem_filter.mp (hsub hyw)).1).2.1 + · intro y hy + have hyB := (mem_erase.mp hy).2 + have h1 : (nbr G B y).card + 1 ≤ PB.card := hch.deg_B hyB + have h2 : (nbr G (B.erase y₁) y).card ≤ (nbr G B y).card := + card_le_card fun w hw => mem_nbr.mpr ⟨(mem_erase.mp (mem_nbr.mp hw).1).2, (mem_nbr.mp hw).2⟩ + omega + +open Classical in +/-- Lema principal (inducción secundaria en el número de clases inaccesibles). -/ +theorem main_lemma {S : Finset V} {P : Finset ℕ} {r s lo : ℕ} + (IH : ∀ S' ⊆ S, edgeCount G S' < edgeCount G S → ∀ (P' : Finset ℕ) (r' : ℕ), + P'.card = r' + 1 → S'.card = s * (r' + 1) → DegLe G S' r' → ∃ c, IsEq G S' P' c s) + (hdeg : DegLe G S r) (hP : P.card = r + 1) : + ∀ (c : V → ℕ) (hi : ℕ), IsNear G S P c s lo hi → ∃ c', IsEq G S P c' s := by + intro c hi hc + induction hk : P.card - (acc G S P c lo).card using Nat.strong_induction_on + generalizing c hi with + | _ k ih => + by_cases hacc : hi ∈ acc G S P c lo + · exact shift_of_acc hc (mem_filter.mp hacc).2 + have h : Ctx G S P c r s lo hi := ⟨hc, hdeg, hP, hacc⟩ + obtain ⟨U, hU, hne, hterm, hP2⟩ := h.exists_TU + have hch := h.countHyp hU hne hP2 + obtain ⟨z, hzS, hzT, ⟨y₀, hy₀⟩, hcase⟩ := hch.lemma_2_3 + -- la coloración `g` de `B \ {y}` por la hipótesis de inducción primaria + have getg : ∀ y ∈ part S c (P \ acc G S P c lo), ∃ g, IsEq G + ((part S c (P \ acc G S P c lo)).erase y) (P \ acc G S P c lo) g s := by + intro y hy + obtain ⟨h1, h2, h3, h4⟩ := bminus h hch hy + exact IH _ h1 h2 _ _ (Nat.succ_pred_eq_of_pos (card_pos.mpr ⟨hi, h.hi_mem_B⟩)).symm h3 h4 + have memB : ∀ y ∈ Sz G S c (T G S P c lo U) (part S c (P \ acc G S P c lo)) z, + y ∈ part S c (P \ acc G S P c lo) := fun y hy => (mem_filter.mp hy).1 + by_cases hmov : ∃ X ∈ acc G S P c lo, X ≠ c z ∧ Movable G S c z X + · obtain ⟨g, hg⟩ := getg y₀ (memB y₀ hy₀) + exact case1 h hterm hzS hzT hy₀ hmov hg + · rcases hcase with hX | ⟨y₁, hy₁, y₂, hy₂, hne12, hnadj⟩ + · exact absurd hX hmov + · push Not at hmov + obtain ⟨g, hg⟩ := getg y₁ (memB y₁ hy₁) + obtain ⟨c', hi', hnear, hlt⟩ := + case2 h hterm hzS hzT (fun X hX hXz => hmov X hX hXz) hy₁ hy₂ hne12 hnadj hg + have hle : (acc G S P c' lo).card ≤ P.card := card_le_card (filter_subset _ _) + exact ih _ (by omega) c' hi' hnear rfl + +open Classical in +/-- Existencia de una partición de `S` en clases de tamaño `s` indexadas por `P`. -/ +theorem exists_equipartition (P : Finset ℕ) (s : ℕ) : + ∀ S : Finset V, S.card = s * P.card → ∃ c : V → ℕ, Into S c P ∧ + ∀ i ∈ P, (cls S c i).card = s := by + induction P using Finset.induction_on with + | empty => + intro S hS + refine ⟨fun _ => 0, fun v hv => ?_, fun i hi => absurd hi (notMem_empty i)⟩ + simp only [card_empty, mul_zero, card_eq_zero] at hS + subst hS + simp only [notMem_empty] at hv + | insert a P ha ih => + intro S hS + rw [card_insert_of_notMem ha, Nat.mul_succ] at hS + obtain ⟨Tₐ, hTS, hTcard⟩ := exists_subset_card_eq (s := S) (n := s) (by omega) + obtain ⟨c, hc, hcard⟩ := ih (S \ Tₐ) (by rw [card_sdiff_of_subset hTS]; omega) + refine ⟨fun v => if v ∈ Tₐ then a else c v, fun v hv => ?_, fun i hi => ?_⟩ + · by_cases hvT : v ∈ Tₐ + · simp [hvT] + · simp only [hvT, ite_false] + exact mem_insert_of_mem (hc v (mem_sdiff.mpr ⟨hv, hvT⟩)) + · rcases mem_insert.mp hi with rfl | hi + · rw [← hTcard] + congr 1 + ext v + simp only [mem_cls] + constructor + · rintro ⟨hv, hva⟩ + by_contra hvT + simp only [hvT, ite_false] at hva + exact ha (hva ▸ hc v (mem_sdiff.mpr ⟨hv, hvT⟩)) + · intro hvT + exact ⟨hTS hvT, by simp [hvT]⟩ + · rw [← hcard i hi] + congr 1 + ext v + simp only [mem_cls, mem_sdiff] + constructor + · rintro ⟨hv, hvi⟩ + have hvT : v ∉ Tₐ := by + intro hvT + simp only [hvT, ite_true] at hvi + exact ha (hvi ▸ hi) + simp only [hvT, ite_false] at hvi + exact ⟨⟨hv, hvT⟩, hvi⟩ + · rintro ⟨⟨hv, hvT⟩, hvi⟩ + exact ⟨hv, by simp [hvT, hvi]⟩ + +open Classical in +/-- **Teorema 2.4** (forma divisible). -/ +theorem core (n : ℕ) : ∀ (G : SimpleGraph V) (S : Finset V) (P : Finset ℕ) (r s : ℕ), + edgeCount G S = n → P.card = r + 1 → S.card = s * (r + 1) → DegLe G S r → + ∃ c, IsEq G S P c s := by + induction n using Nat.strong_induction_on with + | _ n ih => + intro G S P r s hn hP hS hdeg + by_cases h0 : n = 0 + · -- sin aristas: cualquier equipartición sirve + obtain ⟨c, hc, hcard⟩ := exists_equipartition P s S (by rw [hS, hP]) + refine ⟨c, fun v hv w hw hadj => ?_, hc, hcard⟩ + exfalso + have : (v, w) ∈ S.offDiag.filter fun p => G.Adj p.1 p.2 := + mem_filter.mpr ⟨mem_offDiag.mpr ⟨hv, hw, hadj.ne⟩, hadj⟩ + rw [edgeCount, h0] at hn + rw [card_eq_zero.mp hn] at this + exact notMem_empty _ this + -- hay una arista `xy` + obtain ⟨⟨x, y⟩, hxy⟩ : (S.offDiag.filter fun p => G.Adj p.1 p.2).Nonempty := by + rw [← card_pos]; unfold edgeCount at hn; omega + obtain ⟨hxyS, hadj⟩ := mem_filter.mp hxy + obtain ⟨hx, hy, -⟩ := mem_offDiag.mp hxyS + obtain ⟨G', hG'⟩ : ∃ G' : SimpleGraph V, ∀ a b, G'.Adj a b ↔ G.Adj a b ∧ s(a, b) ≠ s(x, y) := + ⟨{ Adj := fun a b => G.Adj a b ∧ s(a, b) ≠ s(x, y) + symm := ⟨fun a b h => ⟨h.1.symm, by rw [Sym2.eq_swap]; exact h.2⟩⟩ + loopless := ⟨fun a h => G.loopless.irrefl a h.1⟩ }, fun _ _ => Iff.rfl⟩ + have hG'le : ∀ a b, G'.Adj a b → G.Adj a b := fun a b h => ((hG' a b).mp h).1 + have hG'adj : ∀ a b, G.Adj a b → s(a, b) ≠ s(x, y) → G'.Adj a b := + fun a b hab hne => (hG' a b).mpr ⟨hab, hne⟩ + -- menos aristas en `G'` + have hlt : edgeCount G' S < edgeCount G S := by + apply card_lt_card + refine ⟨fun p hp => ?_, fun hsub => ?_⟩ + · obtain ⟨hp, hpadj⟩ := mem_filter.mp hp + exact mem_filter.mpr ⟨hp, hG'le _ _ hpadj⟩ + · have := (mem_filter.mp (hsub hxy)).2 + exact ((hG' x y).mp this).2 rfl + have hdeg' : DegLe G' S r := fun v hv => + le_trans (card_le_card fun w hw => + mem_nbr.mpr ⟨(mem_nbr.mp hw).1, hG'le _ _ (mem_nbr.mp hw).2⟩) (hdeg v hv) + obtain ⟨f₀, hf₀⟩ := ih _ (hn ▸ hlt) G' S P r s rfl hP hS hdeg' + -- hipótesis de inducción para subconjuntos (mismo grafo `G`) + have IH : ∀ S' ⊆ S, edgeCount G S' < edgeCount G S → ∀ (P' : Finset ℕ) (r' : ℕ), + P'.card = r' + 1 → S'.card = s * (r' + 1) → DegLe G S' r' → ∃ c, IsEq G S' P' c s := + fun S' _ hS' P' r' hP' hcard hdeg'' => ih _ (hn ▸ hS') G S' P' r' s rfl hP' hcard hdeg'' + by_cases hcol : f₀ x = f₀ y + · -- `x` e `y` en la misma clase: mover `x` a una clase sin vecinos de `x` + -- vecinos de `x` en colores distintos de `f₀ x`: a lo más `r - 1` + set N := (nbr G S x).filter fun w => f₀ w ≠ f₀ x + have hN : N.card + 1 ≤ r := by + have hsub : insert y N ⊆ nbr G S x := by + intro w hw + rcases mem_insert.mp hw with rfl | hw + · exact mem_nbr.mpr ⟨hy, hadj⟩ + · exact (mem_filter.mp hw).1 + have hyN : y ∉ N := fun h => (mem_filter.mp h).2 hcol.symm + have := card_le_card hsub + rw [card_insert_of_notMem hyN] at this + exact le_trans this (hdeg x hx) + have hfree : ∃ j ∈ P.erase (f₀ x), ∀ w ∈ N, f₀ w ≠ j := by + by_contra hno + push Not at hno + have hsub : P.erase (f₀ x) ⊆ N.image f₀ := by + intro j hj + obtain ⟨w, hw, hwj⟩ := hno j hj + exact mem_image.mpr ⟨w, hw, hwj⟩ + have h1 := le_trans (card_le_card hsub) card_image_le + rw [card_erase_of_mem (hf₀.into x hx), hP] at h1 + omega + obtain ⟨j, hjP, hjfree⟩ := hfree + obtain ⟨hjx, hjP⟩ := mem_erase.mp hjP + have hmov : Movable G S f₀ x j := by + intro w hw hxw + rw [mem_cls] at hw + exact hjfree w (mem_filter.mpr ⟨mem_nbr.mpr ⟨hw.1, hxw⟩, hw.2 ▸ hjx⟩) hw.2 + have hcx : f₀ x ≠ j := Ne.symm hjx + have hproper : Proper G S (Function.update f₀ x j) := by + have hp' : Proper G' S (Function.update f₀ x j) := + proper_update hf₀.proper fun w hw hxw => hmov w hw (hG'le _ _ hxw) + intro a ha b hb hab + by_cases he : s(a, b) = s(x, y) + · rcases Sym2.eq_iff.mp he with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · have hab' : a ≠ b := hab.ne + simp only [Function.update_self, Function.update_of_ne hab'.symm] + rw [← hcol]; exact Ne.symm hcx + · have hab' : a ≠ b := hab.ne + simp only [Function.update_self, Function.update_of_ne hab'] + rw [← hcol]; exact hcx + · exact hp' a ha b hb (hG'adj a b hab he) + have hs1 : (cls S f₀ (f₀ x)).card = s := hf₀.card _ (hf₀.into x hx) + have hnear : IsNear G S P (Function.update f₀ x j) s (f₀ x) j := by + refine ⟨hproper, into_update hf₀.into hjP, hf₀.into x hx, hjP, hcx, ?_, ?_, ?_⟩ + · have h1 : (cls S (Function.update f₀ x j) (f₀ x)).card + 1 = (cls S f₀ (f₀ x)).card := + card_cls_update_old hx hcx + omega + · rw [card_cls_update_self hx hcx, hf₀.card j hjP] + · intro i hi hix hij + rw [cls_update_other hij hix, hf₀.card i hi] + exact main_lemma IH hdeg hP _ j hnear + · -- `f₀` ya es propia para `G` + refine ⟨f₀, fun a ha b hb hab => ?_, hf₀.into, hf₀.card⟩ + by_cases he : s(a, b) = s(x, y) + · rcases Sym2.eq_iff.mp he with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · exact hcol + · exact Ne.symm hcol + · exact hf₀.proper a ha b hb (hG'adj a b hab he) + +end HajnalSzemeredi diff --git a/LeanPool/HajnalSzemeredi/Reach.lean b/LeanPool/HajnalSzemeredi/Reach.lean new file mode 100644 index 0000000000..0fc119f6b5 --- /dev/null +++ b/LeanPool/HajnalSzemeredi/Reach.lean @@ -0,0 +1,55 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import Mathlib.Logic.Relation + +/-! +Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit +`ba34061e3cf12dfc8297610d5d7b3f0afac7ec54`; import paths adapted. + +# Lemas genéricos de alcanzabilidad + +Dos herramientas sobre `Relation.ReflTransGen` que reemplazan el uso de "caminos simples" en el +argumento de Kierstead–Kostochka: + +* `transfer`: si `x` alcanza `z` por `R`, y `R'` contiene todos los arcos de `R` cuyo destino no es + `x`, entonces `x` alcanza `z` por `R'` (se usa la última visita a `x`). +* `exists_step_avoid`: si `x ≠ z` y `x` alcanza `z`, hay un primer paso `x → j` con `j ≠ x` tal + que `j` alcanza `z` sin pasar por `x`. +-/ + +@[expose] public section + +namespace HajnalSzemeredi + +open Relation + +variable {α : Type*} + +open Classical in +theorem transfer {R R' : α → α → Prop} {x z : α} (h : ReflTransGen R x z) + (hR : ∀ a b, R a b → b ≠ x → R' a b) : ReflTransGen R' x z := by + induction h with + | refl => exact ReflTransGen.refl + | @tail b c _ hab ih => + by_cases hc : c = x + · subst hc; exact ReflTransGen.refl + · exact ih.tail (hR _ _ hab hc) + +open Classical in +theorem exists_step_avoid {R : α → α → Prop} {x z : α} (h : ReflTransGen R x z) (hxz : x ≠ z) : + ∃ j, R x j ∧ j ≠ x ∧ ReflTransGen (fun a b => R a b ∧ a ≠ x ∧ b ≠ x) j z := by + induction h with + | refl => exact absurd rfl hxz + | @tail a b hxa hab ih => + by_cases ha : a = x + · subst ha + exact ⟨b, hab, Ne.symm hxz, ReflTransGen.refl⟩ + · obtain ⟨j, hj, hjx, hjb⟩ := ih (Ne.symm ha) + exact ⟨j, hj, hjx, hjb.tail ⟨hab, ha, Ne.symm hxz⟩⟩ + +end HajnalSzemeredi diff --git a/LeanPool/HajnalSzemeredi/Shift.lean b/LeanPool/HajnalSzemeredi/Shift.lean new file mode 100644 index 0000000000..dc9eb960ca --- /dev/null +++ b/LeanPool/HajnalSzemeredi/Shift.lean @@ -0,0 +1,121 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.HajnalSzemeredi.Defs +public import LeanPool.HajnalSzemeredi.Reach + +/-! +Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit +`ba34061e3cf12dfc8297610d5d7b3f0afac7ec54`; import paths adapted. + +# Lema 2.1 de Kierstead–Kostochka + +Si la clase grande `hi` de una coloración casi equitativa es accesible (alcanza a la clase +pequeña `lo` en el digrafo auxiliar `H`), moviendo un vértice a lo largo de un camino de `hi` a +`lo` se obtiene una coloración equitativa. + +Para evitar caminos simples, inducimos sobre un conjunto `K` de clases permitidas: tras mover un +vértice de `hi` a la siguiente clase `j`, el resto del camino evita `hi`, y basta con `K \ {hi}`. +-/ + +@[expose] public section + +noncomputable section + +open Finset Relation + +namespace HajnalSzemeredi + +variable {V : Type*} {G : SimpleGraph V} + +open Classical in +/-- Si `j ≠ lo` alcanza a `lo`, la clase `j` es no vacía y por tanto está en la paleta. -/ +lemma mem_palette_of_reach {S : Finset V} {P : Finset ℕ} {c : V → ℕ} (hc : Into S c P) + {R : ℕ → ℕ → Prop} (hR : ∀ a b, R a b → Mov G S c a b) {j lo : ℕ} + (h : ReflTransGen R j lo) (hj : j ≠ lo) : j ∈ P := by + rcases h.cases_head with h | ⟨k, hjk, -⟩ + · exact absurd h hj + · obtain ⟨v, hv, -⟩ := hR _ _ hjk + rw [mem_cls] at hv + exact hv.2 ▸ hc v hv.1 + +open Classical in +theorem shift {S : Finset V} {P : Finset ℕ} {s lo : ℕ} (K : Finset ℕ) : + ∀ (c : V → ℕ) (hi : ℕ), IsNear G S P c s lo hi → + ReflTransGen (fun a b => Mov G S c a b ∧ a ∈ K ∧ b ∈ K) hi lo → + ∃ c', IsEq G S P c' s := by + induction K using Finset.strongInduction with + | H K ih => + intro c hi hc hpath + obtain ⟨j, ⟨⟨v, hv, hmov⟩, hiK, hjK⟩, hjhi, hjpath⟩ := + exists_step_avoid hpath (Ne.symm hc.lo_ne_hi) + rw [mem_cls] at hv + obtain ⟨hvS, hvc⟩ := hv + have hcvj : c v ≠ j := hvc ▸ Ne.symm hjhi + set c' := Function.update c v j with hc' + have hproper : Proper G S c' := proper_update hc.proper hmov + -- tamaños tras el movimiento + have hcard_j : (cls S c' j).card = (cls S c j).card + 1 := card_cls_update_self hvS hcvj + have hcard_hi : (cls S c' hi).card + 1 = (cls S c hi).card := by + have := card_cls_update_old (j := j) hvS hcvj + rwa [hvc] at this + have hcard_other : ∀ k, k ≠ j → k ≠ hi → (cls S c' k).card = (cls S c k).card := by + intro k hkj hkhi + rw [cls_update_other hkj (hvc ▸ hkhi)] + by_cases hjlo : j = lo + · -- llegamos a la clase pequeña: la coloración es equitativa + subst hjlo + refine ⟨c', hproper, into_update hc.into hc.lo_mem, fun k hk => ?_⟩ + by_cases hkj : k = j + · subst hkj; rw [hcard_j, hc.card_lo] + · by_cases hkhi : k = hi + · subst hkhi; have := hc.card_hi; omega + · rw [hcard_other k hkj hkhi, hc.card k hk hkj hkhi] + · -- `j` pasa a ser la clase grande; el camino restante evita `hi` + have hjP : j ∈ P := mem_palette_of_reach hc.into (fun a b h => h.1.1) hjpath hjlo + have hlohi : lo ≠ hi := hc.lo_ne_hi + have hnear : IsNear G S P c' s lo j := by + refine ⟨hproper, into_update hc.into hjP, hc.lo_mem, hjP, Ne.symm hjlo, ?_, ?_, ?_⟩ + · rw [hcard_other lo (Ne.symm hjlo) hlohi, hc.card_lo] + · rw [hcard_j, hc.card j hjP hjlo hjhi] + · intro k hk hklo hkj + by_cases hkhi : k = hi + · subst hkhi; have := hc.card_hi; omega + · rw [hcard_other k hkj hkhi, hc.card k hk hklo hkhi] + refine ih (K.erase hi) (erase_ssubset hiK) c' j hnear ?_ + refine transfer hjpath fun a b hab hbj => ?_ + obtain ⟨⟨⟨w, hw, hwmov⟩, haK, hbK⟩, hahi, hbhi⟩ := hab + rw [mem_cls] at hw + have hwv : w ≠ v := by + rintro rfl + exact hahi (hw.2.symm.trans hvc) + refine ⟨⟨w, ?_, ?_⟩, mem_erase.mpr ⟨hahi, haK⟩, mem_erase.mpr ⟨hbhi, hbK⟩⟩ + · rw [mem_cls, hc', Function.update_of_ne hwv] + exact hw + · intro u hu + rw [cls_update_other hbj (hvc ▸ hbhi)] at hu + exact hwmov u hu + +open Classical in +/-- **Lema 2.1.** Si la clase grande es accesible, hay una coloración equitativa. -/ +theorem shift_of_acc {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {s lo hi : ℕ} + (hc : IsNear G S P c s lo hi) (hacc : ReflTransGen (Mov G S c) hi lo) : + ∃ c', IsEq G S P c' s := by + set K : Finset ℕ := insert lo (S.image c) + have key : ∀ a, ReflTransGen (Mov G S c) a lo → + a ∈ K ∧ ReflTransGen (fun a b => Mov G S c a b ∧ a ∈ K ∧ b ∈ K) a lo := by + intro a h + induction h using ReflTransGen.head_induction_on with + | refl => exact ⟨mem_insert_self _ _, ReflTransGen.refl⟩ + | head hab _ ih => + obtain ⟨v, hv, -⟩ := id hab + rw [mem_cls] at hv + have haK : _ ∈ K := mem_insert_of_mem (mem_image.mpr ⟨v, hv.1, hv.2⟩) + exact ⟨haK, ReflTransGen.head ⟨hab, haK, ih.1⟩ ih.2⟩ + exact shift K c hi hc (key hi hacc).2 + +end HajnalSzemeredi diff --git a/LeanPool/HajnalSzemeredi/Structure.lean b/LeanPool/HajnalSzemeredi/Structure.lean new file mode 100644 index 0000000000..38127bb723 --- /dev/null +++ b/LeanPool/HajnalSzemeredi/Structure.lean @@ -0,0 +1,345 @@ +/- +Copyright (c) 2026 Juan Pablo Traverso Gianini. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Juan Pablo Traverso Gianini +-/ +module + +public import LeanPool.HajnalSzemeredi.CountDefinitions +public import LeanPool.HajnalSzemeredi.Reach +public import Mathlib.Combinatorics.Enumerative.DoubleCounting +public import Mathlib.Algebra.Order.BigOperators.Group.Finset +public import Mathlib.Tactic.Ring + +/-! +Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit +`ba34061e3cf12dfc8297610d5d7b3f0afac7ec54`; import paths adapted. + +# Estructura de una coloración casi equitativa con clase grande inaccesible + +Contexto (`Ctx`): `c` es casi equitativa en `S` con paleta `P` (`|P| = r + 1`), grado máximo +`≤ r`, y la clase grande `hi` no es accesible. Sea `𝒜 = acc` la familia de clases accesibles y +`ℬ = P \ 𝒜`. + +* `h21`: todo `y ∈ B` tiene un vecino en cada clase de `𝒜` (desigualdad (2.1)); +* `card_B`, `card_A`: `|B| = |ℬ| s + 1`, `|A| + 1 = |𝒜| s`; +* `two_le_card_acc`: `|𝒜| ≥ 2`; +* clases terminales y la familia `𝒜' = T_U` (`exists_TU`), con la propiedad (2.2); +* `countHyp`: las hipótesis de la parte de conteo. +-/ + +@[expose] public section + +noncomputable section + +open Finset Relation + +namespace HajnalSzemeredi + +variable {V : Type*} {G : SimpleGraph V} + +open Classical in +/-- Contexto del lema principal. -/ +structure Ctx (G : SimpleGraph V) (S : Finset V) (P : Finset ℕ) (c : V → ℕ) + (r s lo hi : ℕ) : Prop where + near : IsNear G S P c s lo hi + deg : DegLe G S r + card_P : P.card = r + 1 + hi_not : hi ∉ acc G S P c lo + +open Classical in +/-- Arcos de `H - W`. -/ +def avoid (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (W : ℕ) (a b : ℕ) : Prop := + Mov G S c a b ∧ a ≠ W ∧ b ≠ W + +open Classical in +/-- `T_W`: clases accesibles distintas de `W` que no alcanzan `lo` en `H - W`. -/ +def T (G : SimpleGraph V) (S : Finset V) (P : Finset ℕ) (c : V → ℕ) (lo W : ℕ) : Finset ℕ := + ((acc G S P c lo).erase W).filter fun X => ¬ ReflTransGen (avoid G S c W) X lo + +open Classical in +lemma card_part (S : Finset V) (c : V → ℕ) (Q : Finset ℕ) : + (part S c Q).card = ∑ i ∈ Q, (cls S c i).card := by + rw [← card_biUnion] + · congr 1 + ext v + simp [part, mem_cls, and_comm] + · intro i _ j _ hij + exact cls_disjoint hij + +open Classical in +/-- `x ∈ T` y `x` alcanza un objetivo: si el camino pasa por `x'`, o lo evita o `x'` alcanza. -/ +theorem split_avoid {α : Type*} {R : α → α → Prop} {x z : α} : + ∀ {a}, ReflTransGen R a z → a ≠ x → + ReflTransGen (fun u v => R u v ∧ u ≠ x ∧ v ≠ x) a z ∨ ReflTransGen R x z := by + intro a h + induction h using ReflTransGen.head_induction_on with + | refl => exact fun _ => Or.inl ReflTransGen.refl + | head hab hbz ih => + rename_i a b + intro hax + by_cases hbx : b = x + · subst hbx; exact Or.inr hbz + · rcases ih hbx with h | h + · exact Or.inl (ReflTransGen.head ⟨hab, hax, hbx⟩ h) + · exact Or.inr h + +open Classical in +/-- Transport reachability along inclusion of relations. -/ +theorem rtgMono {α : Type*} {R R' : α → α → Prop} {a b : α} (h : ReflTransGen R a b) + (hR : ∀ x y, R x y → R' x y) : ReflTransGen R' a b := + ReflTransGen.mono hR a b h + +namespace Ctx + +variable {S : Finset V} {P : Finset ℕ} {c : V → ℕ} {r s lo hi : ℕ} + +open Classical in +lemma acc_subset : acc G S P c lo ⊆ P := filter_subset _ _ + +open Classical in +lemma lo_mem_acc (h : Ctx G S P c r s lo hi) : lo ∈ acc G S P c lo := + mem_filter.mpr ⟨h.near.lo_mem, ReflTransGen.refl⟩ + +open Classical in +lemma mem_acc_of_mov (h : Ctx G S P c r s lo hi) {a b : ℕ} (hab : Mov G S c a b) + (hb : b ∈ acc G S P c lo) : a ∈ acc G S P c lo := by + obtain ⟨v, hv, -⟩ := id hab + rw [mem_cls] at hv + exact mem_filter.mpr ⟨hv.2 ▸ h.near.into v hv.1, ReflTransGen.head hab (mem_filter.mp hb).2⟩ + +open Classical in +lemma hi_mem_B (h : Ctx G S P c r s lo hi) : hi ∈ P \ acc G S P c lo := + mem_sdiff.mpr ⟨h.near.hi_mem, h.hi_not⟩ + +open Classical in +lemma cover (h : Ctx G S P c r s lo hi) : + ∀ v ∈ S, c v ∈ acc G S P c lo ∪ (P \ acc G S P c lo) := by + intro v hv + rw [union_sdiff_of_subset acc_subset] + exact h.near.into v hv + +open Classical in +lemma card_r (h : Ctx G S P c r s lo hi) : + r + 1 = (acc G S P c lo).card + (P \ acc G S P c lo).card := by + have h1 := card_sdiff_of_subset (acc_subset (G := G) (S := S) (P := P) (c := c) (lo := lo)) + have h2 := card_le_card (acc_subset (G := G) (S := S) (P := P) (c := c) (lo := lo)) + have h3 := h.card_P + omega + +open Classical in +/-- (2.1): todo vértice de `B` tiene un vecino en cada clase accesible. -/ +lemma h21 (h : Ctx G S P c r s lo hi) {y : V} (hy : y ∈ part S c (P \ acc G S P c lo)) + {X : ℕ} (hX : X ∈ acc G S P c lo) : (nIn G S c y X).Nonempty := by + by_contra hne + rw [not_nonempty_iff_eq_empty] at hne + have hy' := mem_filter.mp hy + have hmov : Mov G S c (c y) X := by + refine ⟨y, mem_cls.mpr ⟨hy'.1, rfl⟩, fun w hw hadj => ?_⟩ + have : w ∈ nIn G S c y X := mem_inter.mpr ⟨mem_nbr.mpr ⟨(mem_cls.mp hw).1, hadj⟩, hw⟩ + rw [hne] at this + exact notMem_empty _ this + exact (mem_sdiff.mp hy'.2).2 (h.mem_acc_of_mov hmov hX) + +open Classical in +lemma card_B (h : Ctx G S P c r s lo hi) : + (part S c (P \ acc G S P c lo)).card = (P \ acc G S P c lo).card * s + 1 := by + rw [card_part, ← add_sum_erase _ _ h.hi_mem_B] + have hsum : ∑ i ∈ (P \ acc G S P c lo).erase hi, (cls S c i).card = + ∑ _i ∈ (P \ acc G S P c lo).erase hi, s := by + refine sum_congr rfl fun i hi' => ?_ + obtain ⟨hih, hiB⟩ := mem_erase.mp hi' + obtain ⟨hiP, hiA⟩ := mem_sdiff.mp hiB + refine h.near.card i hiP ?_ hih + rintro rfl + exact hiA h.lo_mem_acc + rw [hsum, sum_const, smul_eq_mul, card_erase_of_mem h.hi_mem_B, h.near.card_hi] + have : 1 ≤ (P \ acc G S P c lo).card := card_pos.mpr ⟨hi, h.hi_mem_B⟩ + obtain ⟨k, hk⟩ : ∃ k, (P \ acc G S P c lo).card = k + 1 := ⟨_, (Nat.sub_add_cancel this).symm⟩ + rw [hk] + simp only [Nat.add_sub_cancel] + ring + +open Classical in +lemma card_A (h : Ctx G S P c r s lo hi) : + (part S c (acc G S P c lo)).card + 1 = (acc G S P c lo).card * s := by + rw [card_part, ← add_sum_erase _ _ h.lo_mem_acc] + have hsum : ∑ i ∈ (acc G S P c lo).erase lo, (cls S c i).card = + ∑ _i ∈ (acc G S P c lo).erase lo, s := by + refine sum_congr rfl fun i hi' => ?_ + obtain ⟨hil, hiA⟩ := mem_erase.mp hi' + refine h.near.card i (acc_subset hiA) hil ?_ + rintro rfl + exact h.hi_not hiA + rw [hsum, sum_const, smul_eq_mul, card_erase_of_mem h.lo_mem_acc] + have hlo := h.near.card_lo + have : 1 ≤ (acc G S P c lo).card := card_pos.mpr ⟨lo, h.lo_mem_acc⟩ + obtain ⟨k, hk⟩ : ∃ k, (acc G S P c lo).card = k + 1 := ⟨_, (Nat.sub_add_cancel this).symm⟩ + rw [hk] + simp only [Nat.add_sub_cancel] + rw [← hlo] + ring + +open Classical in +/-- `|𝒜| ≥ 2`. -/ +lemma two_le_card_acc (h : Ctx G S P c r s lo hi) : 2 ≤ (acc G S P c lo).card := by + by_contra hlt + push Not at hlt + have hA : acc G S P c lo = {lo} := by + refine eq_singleton_iff_unique_mem.mpr ⟨h.lo_mem_acc, fun x hx => ?_⟩ + by_contra hne + have : ({x, lo} : Finset ℕ) ⊆ acc G S P c lo := by + intro y hy + rcases mem_insert.mp hy with rfl | hy + · exact hx + · rw [mem_singleton.mp hy]; exact h.lo_mem_acc + have := card_le_card this + rw [card_pair hne] at this + omega + set B := part S c (P \ acc G S P c lo) + have hrB : (P \ acc G S P c lo).card = r := by + have h1 := h.card_r + have h2 : (acc G S P c lo).card = 1 := by rw [hA, card_singleton] + omega + -- doble conteo de aristas entre `B` y la clase `lo` + have hdc := sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow (s := B) (t := cls S c lo) + (r := fun y x => G.Adj y x) + have hleft : B.card ≤ ∑ y ∈ B, ((cls S c lo).bipartiteAbove (fun y x => G.Adj y x) y).card := by + rw [card_eq_sum_ones] + refine sum_le_sum fun y hy => ?_ + obtain ⟨w, hw⟩ := h.h21 hy h.lo_mem_acc + rw [nIn, mem_inter, mem_nbr] at hw + exact card_pos.mpr ⟨w, mem_filter.mpr ⟨hw.2, hw.1.2⟩⟩ + have hright : ∑ x ∈ cls S c lo, (B.bipartiteBelow (fun y x => G.Adj y x) x).card ≤ + ∑ _x ∈ cls S c lo, r := by + refine sum_le_sum fun x hx => ?_ + refine le_trans (card_le_card fun y hy => ?_) (h.deg x (mem_cls.mp hx).1) + obtain ⟨hyB, hadj⟩ := mem_filter.mp hy + exact mem_nbr.mpr ⟨(mem_filter.mp hyB).1, hadj.symm⟩ + rw [sum_const, smul_eq_mul] at hright + have hB : B.card = r * s + 1 := by + have := h.card_B + rw [hrB] at this + exact this + have hlo := h.near.card_lo + have hmul : (cls S c lo).card * r ≤ s * r := Nat.mul_le_mul_right r (by omega) + have hcomm : r * s = s * r := Nat.mul_comm r s + have e1 : B.card ≤ (cls S c lo).card * r := by + calc B.card ≤ _ := hleft + _ = _ := hdc + _ ≤ _ := hright + omega + +open Classical in +/-- `lo` no está en ningún `T_W`. -/ +lemma lo_notMem_T (W : ℕ) : lo ∉ T G S P c lo W := by + intro hmem + exact (mem_filter.mp hmem).2 ReflTransGen.refl + +open Classical in +lemma T_lo_nonempty (h : Ctx G S P c r s lo hi) : (T G S P c lo lo).Nonempty := by + have h2 := h.two_le_card_acc + have : 1 < ((acc G S P c lo).erase lo).card + 1 := by + rw [card_erase_add_one h.lo_mem_acc]; omega + obtain ⟨X, hX⟩ := card_pos.mp (by omega : 0 < ((acc G S P c lo).erase lo).card) + refine ⟨X, mem_filter.mpr ⟨hX, fun hpath => ?_⟩⟩ + have hXlo := (mem_erase.mp hX).1 + rcases hpath.cases_tail with h' | ⟨b, -, hb⟩ + · exact hXlo h'.symm + · exact hb.2.2 rfl + +open Classical in +/-- Elección de `U` y de la familia `𝒜' = T_U`. -/ +theorem exists_TU (h : Ctx G S P c r s lo hi) : + ∃ U ∈ acc G S P c lo, (T G S P c lo U).Nonempty ∧ + (∀ W ∈ T G S P c lo U, ∀ X ∈ (acc G S P c lo).erase W, + ReflTransGen (avoid G S c W) X lo) ∧ + (∀ X ∈ T G S P c lo U, ∀ Y ∈ acc G S P c lo, Y ∉ T G S P c lo U → Y ≠ U → + ¬ Mov G S c X Y) := by + set NT := (acc G S P c lo).filter fun W => (T G S P c lo W).Nonempty + have hNT : NT.Nonempty := ⟨lo, mem_filter.mpr ⟨h.lo_mem_acc, h.T_lo_nonempty⟩⟩ + obtain ⟨U, hU, hmin⟩ := exists_min_image NT (fun W => (T G S P c lo W).card) hNT + obtain ⟨hUacc, hUne⟩ := mem_filter.mp hU + refine ⟨U, hUacc, hUne, ?_, ?_⟩ + · -- toda clase de `T_U` es terminal + intro W hW X hX + obtain ⟨hWU', hWnot⟩ := mem_filter.mp hW + obtain ⟨hWU, hWacc⟩ := mem_erase.mp hWU' + have hsub : T G S P c lo W ⊆ (T G S P c lo U).erase W := by + intro Y hY + obtain ⟨hYW', hYnot⟩ := mem_filter.mp hY + obtain ⟨hYW, hYacc⟩ := mem_erase.mp hYW' + refine mem_erase.mpr ⟨hYW, ?_⟩ + have hYU : Y ≠ U := by + rintro rfl + have hUlo : Y ≠ lo := by rintro rfl; exact hYnot ReflTransGen.refl + obtain ⟨j, hj, hjU, hjpath⟩ := exists_step_avoid (mem_filter.mp hYacc).2 hUlo + have hjW : j ≠ W := by rintro rfl; exact hWnot hjpath + rcases split_avoid (x := W) hjpath hjW with hp | hp + · exact hYnot (ReflTransGen.head ⟨hj, hWU.symm, hjW⟩ + (rtgMono hp (fun a b hab => ⟨hab.1.1, hab.2.1, hab.2.2⟩))) + · exact hWnot hp + refine mem_filter.mpr ⟨mem_erase.mpr ⟨hYU, hYacc⟩, fun hp => ?_⟩ + rcases split_avoid (x := W) hp hYW with hp' | hp' + · exact hYnot (rtgMono hp' (fun a b hab => ⟨hab.1.1, hab.2.1, hab.2.2⟩)) + · exact hWnot hp' + have hTW : T G S P c lo W = ∅ := by + by_contra hne + have hWNT : W ∈ NT := mem_filter.mpr ⟨hWacc, nonempty_iff_ne_empty.mpr hne⟩ + exact absurd (hmin W hWNT) + (not_le.mpr (lt_of_le_of_lt (card_le_card hsub) (card_erase_lt_of_mem hW))) + by_contra hnot + have : X ∈ T G S P c lo W := mem_filter.mpr ⟨hX, hnot⟩ + rw [hTW] at this + exact notMem_empty _ this + · -- ninguna clase de `T_U` es movible a una clase de `(𝒜 \ 𝒜') \ {U}` + intro X hX Y hY hYT hYU hmov + obtain ⟨hXU', hXnot⟩ := mem_filter.mp hX + have hXU := (mem_erase.mp hXU').1 + have hYreach : ReflTransGen (avoid G S c U) Y lo := by + by_contra hn + exact hYT (mem_filter.mpr ⟨mem_erase.mpr ⟨hYU, hY⟩, hn⟩) + exact hXnot (ReflTransGen.head ⟨hmov, hXU, hYU⟩ hYreach) + +open Classical in +lemma T_subset (U : ℕ) : T G S P c lo U ⊆ (acc G S P c lo).erase U := filter_subset _ _ + +open Classical in +/-- Las hipótesis de conteo valen para `𝒜' = T_U`. -/ +theorem countHyp (h : Ctx G S P c r s lo hi) {U : ℕ} (hU : U ∈ acc G S P c lo) + (hne : (T G S P c lo U).Nonempty) + (hP2 : ∀ X ∈ T G S P c lo U, ∀ Y ∈ acc G S P c lo, Y ∉ T G S P c lo U → Y ≠ U → + ¬ Mov G S c X Y) : + CountHyp G S c (acc G S P c lo) (P \ acc G S P c lo) (T G S P c lo U) r s := by + refine ⟨disjoint_sdiff, h.cover, fun W hW => (mem_erase.mp (T_subset U hW)).2, hne, + h.card_r, h.deg, ?_, h.card_B, fun y hy X hX => h.h21 hy hX, ?_⟩ + · intro W hW + have hWacc := (mem_erase.mp (T_subset U hW)).2 + refine h.near.card W (acc_subset hWacc) ?_ ?_ + · rintro rfl; exact lo_notMem_T _ hW + · rintro rfl; exact h.hi_not hWacc + · intro x hx hxT + set Q := (acc G S P c lo \ T G S P c lo U).erase U + have hQ : Q ⊆ (nbr G (part S c (acc G S P c lo)) x).image c := by + intro Y hY + obtain ⟨hYU, hY'⟩ := mem_erase.mp hY + obtain ⟨hYacc, hYT⟩ := mem_sdiff.mp hY' + have hnm := hP2 (c x) hxT Y hYacc hYT hYU + have : ¬ Movable G S c x Y := fun hmov => hnm ⟨x, mem_cls.mpr ⟨hx, rfl⟩, hmov⟩ + simp only [Movable, not_forall, not_not] at this + obtain ⟨w, hw, hadj⟩ := this + rw [mem_cls] at hw + refine mem_image.mpr ⟨w, mem_nbr.mpr ⟨mem_filter.mpr ⟨hw.1, hw.2 ▸ hYacc⟩, hadj⟩, hw.2⟩ + have h1 := le_trans (card_le_card hQ) card_image_le + have hUmem : U ∈ acc G S P c lo \ T G S P c lo U := + mem_sdiff.mpr ⟨hU, fun hUT => (mem_erase.mp (T_subset U hUT)).1 rfl⟩ + have h2 : Q.card + 1 = _ := card_erase_add_one hUmem + have h3 : (acc G S P c lo \ T G S P c lo U).card + (T G S P c lo U).card = + (acc G S P c lo).card := by + rw [card_sdiff_add_card_eq_card] + exact fun W hW => (mem_erase.mp (T_subset U hW)).2 + omega + +end Ctx + +end HajnalSzemeredi diff --git a/LeanPool/projects/hajnal-szemeredi.yaml b/LeanPool/projects/hajnal-szemeredi.yaml new file mode 100644 index 0000000000..f018f1a277 --- /dev/null +++ b/LeanPool/projects/hajnal-szemeredi.yaml @@ -0,0 +1,52 @@ +slug: hajnal-szemeredi +title: The Hajnal–Szemerédi theorem on equitable vertex colourings +summary: >- + Every finite simple graph of maximum degree at most r admits a proper colouring + with r + 1 colours whose class sizes differ by at most one. When the vertex count + is s(r + 1), every class can have exactly s vertices. The proof follows the + Kierstead–Kostochka argument, preserving finite-subgraph and arbitrary-palette + recolouring, reachability, terminal-class and discharging infrastructure. + The polynomial-time algorithm from Section 3 is outside the imported scope. +branch: extremal graph theory +entry_module: LeanPool.HajnalSzemeredi +authors: +- Juan Pablo Traverso Gianini +source: + title: A short proof of the Hajnal–Szemerédi theorem on equitable colouring + authors: + - H. A. Kierstead + - A. V. Kostochka + doi: 10.1017/S0963548307008619 + url: https://github.com/jtraverso/hajnal-szemeredi/tree/ba34061e3cf12dfc8297610d5d7b3f0afac7ec54 + github_repo: jtraverso/hajnal-szemeredi + commit: ba34061e3cf12dfc8297610d5d7b3f0afac7ec54 + completion_url: https://github.com/jtraverso/hajnal-szemeredi/commit/7003b3b5fb94b54364899ac03f4d26be9fd1f8ed + completion_date: '2026-10-12' +license: Apache-2.0 +status: verified +provenance: AI +main_declarations: +- HajnalSzemeredi.hajnalSzemeredi +- HajnalSzemeredi.hajnalSzemeredi_exact +main_results: +- declaration: HajnalSzemeredi.hajnalSzemeredi + informal: >- + Every finite simple graph whose vertex degrees are at most r has a proper + colouring by Fin (r + 1) such that the size of any colour class is at most + the size of any other colour class plus one. +- declaration: HajnalSzemeredi.hajnalSzemeredi_exact + informal: >- + If a finite simple graph has s(r + 1) vertices and every vertex degree is at + most r, it has a proper colouring by Fin (r + 1) with every class of size s. +- declaration: HajnalSzemeredi.core + informal: >- + For any finite vertex subset S and finite natural-number palette P of size + r + 1, if S has s(r + 1) vertices and every vertex has at most r neighbours + within S, there is a proper colouring of S in P with all classes of size s. +tags: +- graph-theory +- equitable-colouring +- extremal-combinatorics +msc: +- 05C15 +- 05C35 From dfbcbd39c846fbc82f10fc57f2c34edebba42bd3 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 13 Oct 2026 10:52:12 +0000 Subject: [PATCH 2/2] Generalize the colour-class update identity --- LeanPool/HajnalSzemeredi/Cases.lean | 2 +- LeanPool/HajnalSzemeredi/Defs.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanPool/HajnalSzemeredi/Cases.lean b/LeanPool/HajnalSzemeredi/Cases.lean index 051ebfeb76..de5555a92c 100644 --- a/LeanPool/HajnalSzemeredi/Cases.lean +++ b/LeanPool/HajnalSzemeredi/Cases.lean @@ -250,7 +250,7 @@ theorem case1 {S : Finset V} {P : Finset ℕ} {c g : V → ℕ} {r s lo hi U : · subst hvz; simpa [hc1] using hXacc · rw [hc1, Function.update_of_ne hvz]; exact (mem_filter.mp hvA).2 have hclsW : cls SA φ (c z) = insert y₁ ((cls S c (c z)).erase z) := by - rw [hSA, hφ, cls_insert_update_self, hc1, cls_update_old hzA hXW.symm, cls_part hWacc] + rw [hSA, hφ, cls_insert_update_self, hc1, cls_update_old hXW.symm, cls_part hWacc] have hclsWcard : (cls SA φ (c z)).card = s := by rw [hclsW, card_insert_of_notMem, card_erase_of_mem (mem_cls.mpr ⟨hzS, rfl⟩), hWcard] · have : 0 < s := hWcard ▸ card_pos.mpr ⟨z, mem_cls.mpr ⟨hzS, rfl⟩⟩ diff --git a/LeanPool/HajnalSzemeredi/Defs.lean b/LeanPool/HajnalSzemeredi/Defs.lean index 2bfefa7a1f..4ecf8e3048 100644 --- a/LeanPool/HajnalSzemeredi/Defs.lean +++ b/LeanPool/HajnalSzemeredi/Defs.lean @@ -147,7 +147,7 @@ lemma cls_update_self (hv : v ∈ S) : · simp [hw] open Classical in -lemma cls_update_old (hv : v ∈ S) (hj : c v ≠ j) : +lemma cls_update_old (hj : c v ≠ j) : cls S (Function.update c v j) (c v) = (cls S c (c v)).erase v := by ext w by_cases hw : w = v @@ -171,7 +171,7 @@ lemma card_cls_update_self (hv : v ∈ S) (hj : c v ≠ j) : open Classical in lemma card_cls_update_old (hv : v ∈ S) (hj : c v ≠ j) : (cls S (Function.update c v j) (c v)).card + 1 = (cls S c (c v)).card := by - rw [cls_update_old hv hj, card_erase_add_one] + rw [cls_update_old hj, card_erase_add_one] simp [hv] open Classical in