feat(ErdosProblems): 835

FormalConjectures/ErdosProblems/835.lean

@@ -0,0 +1,75 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+import FormalConjectures.Util.ProblemImports
+
+
+/-!
+# Erdős Problem 835
+
+*Reference:* [erdosproblems.com/835](https://www.erdosproblems.com/835)
+-/
+
+open Finset SimpleGraph
+open scoped Nat
+
+namespace Erdos835
+variable {n k : ℕ}
+
+/-- Johnson's upper bound on the maximum size `A(n, d, w)` of a `n`-dimensional binary code of
+distance `d` and weight `w` is as follows:
+* If `d > 2 * w`, then `A(n, d, w) = 1`.
+* If `d ≤ 2 * w`, then `A(n, d, w) ≤ ⌊n / w * A(n - 1, d, w - 1)⌋`. -/
+def johnsonBound : ℕ → ℕ → ℕ → ℕ
+  | 0, _d, _w => 1
+  | _n, _d, 0 => 1
+  | n + 1, d, w + 1 => if 2 * (w + 1) < d then 1 else (n + 1) * johnsonBound n d w / (w + 1)
+
+/-- Johnson's bound for the independence number of the Johnson graph. -/
+@[category research solved, AMS 5]
+lemma indepNum_johnson_le_johnsonBound : α(J(n, k)) ≤ johnsonBound n 4 k := sorry
+
+/-- Johnson's bound for the chromatic number of the Johnson graph. -/
+@[category research solved, AMS 5]
+lemma div_johnsonBound_le_chromaticNum_johnson :
+    ⌈(n.choose k / johnsonBound n 4 k : ℚ≥0)⌉₊ ≤ χ(J(n, k)) := by
+  obtain hnk | hkn := lt_or_ge n k
+  · simp [Nat.choose_eq_zero_of_lt, *]
+  have : Nonempty {s : Finset (Fin n) // #s = k} := by
+    simpa [Finset.Nonempty] using Finset.powersetCard_nonempty (s := .univ).2 <| by simpa
+  grw [← card_div_indepNum_le_chromaticNumber, indepNum_johnson_le_johnsonBound] <;> simp
+
+/-- It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than
+$k+1$, see [Johnson graphs](https://aeb.win.tue.nl/graphs/Johnson.html). -/
+@[category research solved, AMS 5]
+theorem chromaticNumber_johnson_2k_k_lower_bound (hk : 3 ≤ k) (hk' : k ≤ 8) :
+    k + 1 < J(2 * k, k).chromaticNumber := by
+  sorry
+
+/-- It is also known that for $3 \leq k \leq 203$ odd, the chromatic number of $J(2k, k)$ is
+greater than $k+1$, see [Johnson graphs](https://aeb.win.tue.nl/graphs/Johnson.html). -/
+@[category research solved, AMS 5]
+theorem chromaticNumber_johnson_2k_k_lower_bound_odd (hk : 3 ≤ k) (hk' : k ≤ 300) (hk_odd : Odd k) :
+    k + 1 < J(2 * k, k).chromaticNumber := by
+  grw [← div_johnsonBound_le_chromaticNum_johnson]
+  decide +revert +kernel
+
+/-- Is the chromatic number of `J(2 * k, k)` always at least `k + 2`? -/
+@[category research open, AMS 5]
+theorem johnson_chromaticNumber : answer(sorry) ↔
+    ∀ k ≥ 3, k + 2 ≤ J(2 * k, k).chromaticNumber :=
+  sorry
+
+end Erdos835

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/Clique.lean

@@ -0,0 +1,33 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+import Mathlib.Combinatorics.SimpleGraph.Clique
+
+namespace SimpleGraph
+variable {V : Type*} {G : SimpleGraph V}
+
+@[inherit_doc] scoped notation "α(" G ")" => indepNum G
+
+@[simp] lemma indepNum_of_isEmpty [IsEmpty V] : α(G) = 0 := by
+  simp [indepNum, isNIndepSet_iff, Subsingleton.elim _ ∅]
+
+@[simp] lemma indepNum_pos [Finite V] [Nonempty V] : 0 < α(G) := by
+  cases nonempty_fintype V
+  obtain ⟨v⟩ := ‹Nonempty V›
+  rw [← Nat.add_one_le_iff]
+  exact le_csSup ⟨Nat.card V, by simp [mem_upperBounds, isNIndepSet_iff, Finset.card_le_univ]⟩
+    ⟨{v}, by simp [isNIndepSet_iff]⟩
+
+end SimpleGraph

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/Coloring.lean

@@ -13,20 +13,31 @@ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 See the License for the specific language governing permissions and
 limitations under the License.
 -/
+import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Clique
+import Mathlib.Data.NNRat.Floor
+import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Combinatorics.SimpleGraph.Coloring
-import Mathlib.Order.CompletePartialOrder
 
 variable {V α ι : Type*} {G : SimpleGraph V} {n : ℕ}
 
 namespace SimpleGraph
 
+@[inherit_doc] scoped notation "χ(" G ")" => chromaticNumber G
+
 lemma le_chromaticNumber_iff_colorable : n ≤ G.chromaticNumber ↔ ∀ m, G.Colorable m → n ≤ m := by
   simp [chromaticNumber]
 
 lemma le_chromaticNumber_iff_coloring :
     n ≤ G.chromaticNumber ↔ ∀ m, G.Coloring (Fin m) → n ≤ m := by
   simp [le_chromaticNumber_iff_colorable, Colorable]
 
+lemma lt_chromaticNumber_iff_not_colorable : n < G.chromaticNumber ↔ ¬ G.Colorable n := by
+  rw [← chromaticNumber_le_iff_colorable, not_le]
+
+lemma le_chromaticNumber_iff_not_colorable (hn : n ≠ 0) :
+    n ≤ G.chromaticNumber ↔ ¬ G.Colorable (n - 1) := by
+  let n + 1 := n; simp [ENat.add_one_le_iff, lt_chromaticNumber_iff_not_colorable]
+
 lemma Coloring.injective_comp_of_pairwise_adj (C : G.Coloring α) (f : ι → V)
     (hf : Pairwise fun i j ↦ G.Adj (f i) (f j)) : (C ∘ f).Injective :=
   Function.injective_iff_pairwise_ne.2 fun _i _j hij ↦ C.valid <| hf hij
@@ -40,6 +51,19 @@ lemma le_chromaticNumber_of_pairwise_adj (hn : n ≤ Nat.card ι) (f : ι → V)
     (hf : Pairwise fun i j ↦ G.Adj (f i) (f j)) : n ≤ G.chromaticNumber :=
   le_chromaticNumber_iff_colorable.2 fun _m hm ↦ hn.trans <| hm.card_le_of_pairwise_adj f hf
 
+lemma card_div_indepNum_le_chromaticNumber : ⌈(Nat.card V / α(G) : ℚ≥0)⌉₊ ≤ G.chromaticNumber := by
+  cases finite_or_infinite V
+  swap; · simp
+  cases nonempty_fintype V
+  simp only [Nat.card_eq_fintype_card, le_chromaticNumber_iff_coloring, Nat.ceil_le]
+  refine fun m c ↦ div_le_of_le_mul₀ (by simp) (by simp) ?_
+  norm_cast
+  rw [← mul_one (Fintype.card V), ← Fintype.card_fin m]
+  refine Finset.card_mul_le_card_mul (c · = ·)
+    (by simp [Finset.bipartiteAbove, Finset.filter_nonempty_iff])
+    fun b _ ↦ IsIndepSet.card_le_indepNum ?_
+  simpa [IsIndepSet, Set.Pairwise] using fun x hx y hy _ ↦ c.not_adj_of_mem_colorClass hx hy
+
 instance (f : ι → V) : IsSymm ι fun i j ↦ G.Adj (f i) (f j) where symm _ _ := .symm
 
 variable (G) in

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/GraphConjectures/Definitions.lean

@@ -43,9 +43,6 @@ noncomputable def m (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ :=
   let matchings := { M : Subgraph G | M.IsMatching }
   sSup (Set.image (fun M => (M.edgeSet.toFinset.card : ℝ)) matchings)
 
-/-- The independence number of a graph `G`. -/
-noncomputable def a (G : SimpleGraph α) : ℝ := (G.indepNum : ℝ)
-
 /-- The maximum cardinality among all independent sets `s`
     that maximize the quantity `|s| - |N(s)|`, where `N(s)`
     is the neighborhood of the set `s`. -/
@@ -57,7 +54,6 @@ noncomputable def aprime (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ :=
   letI max_card := (critical_sets.image Finset.card).max
   (max_card.getD 0 : ℝ)
 
-
 /-- `largestInducedForestSize G` is the size of a largest induced forest of `G`. -/
 noncomputable def largestInducedForestSize (G : SimpleGraph α) : ℕ :=
   sSup { n | ∃ s : Finset α, (G.induce s).IsAcyclic ∧ s.card = n }

FormalConjectures/ForMathlib/Combinatorics/SimpleGraph/Johnson.lean

@@ -0,0 +1,55 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+import Mathlib.Combinatorics.SimpleGraph.Basic
+import FormalConjectures.ForMathlib.Data.Finset.Card
+
+open Finset
+
+namespace SimpleGraph
+variable {n k : ℕ}
+
+/--
+The Johnson graph $J(n, k)$ has as vertices the $k$-subsets of an $n$-set.
+Two vertices are adjacent if their intersection has size $k - 1$.
+-/
+@[simps -isSimp]
+def johnson (n k : ℕ) : SimpleGraph {s : Finset (Fin n) // #s = k} where
+  Adj s t := #(s.val ∩ t.val) + 1 = k
+  symm s t h := by simpa [inter_comm]
+  loopless := by simp +contextual [Irreflexive]
+
+scoped notation "J(" n ", " k ")" => johnson n k
+
+lemma johnson_adj_iff_ge {s t : {s : Finset (Fin n) // #s = k}} :
+    J(n, k).Adj s t ↔ s ≠ t ∧ k ≤ #(s.val ∩ t.val) + 1 := by
+  obtain ⟨s, hs⟩ := s
+  obtain ⟨t, ht⟩ := t
+  simp only [johnson_adj, le_antisymm_iff (α := ℕ), ne_eq, Subtype.mk.injEq, and_congr_left_iff]
+  rintro h
+  constructor
+  · rintro hst rfl
+    simp at hst
+    omega
+  · rintro hst
+    rw [Nat.add_one_le_iff, ← hs, card_lt_card_iff_of_subset inter_subset_left]
+    simp only [ne_eq, inter_eq_left]
+    contrapose! hst
+    exact eq_of_subset_of_card_le hst (by simp [*])
+
+lemma not_johnson_adj_iff_lt {s t : {s : Finset (Fin n) // #s = k}} :
+    ¬ J(n, k).Adj s t ↔ s = t ∨ #(s.val ∩ t.val) + 1 < k := by simp [johnson_adj_iff_ge]; tauto
+
+end SimpleGraph

FormalConjectures/ForMathlib/Data/Finset/Card.lean

@@ -0,0 +1,28 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+import Mathlib.Data.Finset.Card
+
+namespace Finset
+variable {α : Type*} {s t : Finset α}
+
+lemma card_le_card_iff_of_subset (hst : s ⊆ t) : #t ≤ #s ↔ s = t where
+  mp := eq_of_subset_of_card_le hst
+  mpr := by rintro rfl; rfl
+
+lemma card_lt_card_iff_of_subset (hst : s ⊆ t) : #s < #t ↔ s ≠ t := by
+  rw [← not_le, card_le_card_iff_of_subset hst]
+
+end Finset

FormalConjectures/ForMathlib/Data/Finset/Powerset.lean

@@ -0,0 +1,30 @@
+/-
+Copyright 2025 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+import Mathlib.Data.Finset.Powerset
+
+namespace Finset
+variable {α : Type*} [DecidableEq α] {s t : Finset α} {n : ℕ}
+
+attribute [gcongr] powersetCard_mono
+
+lemma powersetCard_inter : powersetCard n (s ∩ t) = powersetCard n s ∩ powersetCard n t := by
+  ext; simpa [subset_inter_iff] using and_and_right
+
+@[simp] lemma disjoint_powersetCard_powersetCard :
+    Disjoint (powersetCard n s) (powersetCard n t) ↔ #(s ∩ t) < n := by
+  simp [disjoint_iff_inter_eq_empty, ← powersetCard_inter]
+
+end Finset

FormalConjectures/Util/ForMathlib.lean

@@ -36,11 +36,16 @@ import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.D
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Domination
 import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.GraphConjectures.Invariants
 import FormalConjectures.ForMathlib.Computability.Encoding
+import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Balanced
+import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Clique
+import FormalConjectures.ForMathlib.Combinatorics.SimpleGraph.Johnson
 import FormalConjectures.ForMathlib.Computability.TuringMachine.BusyBeavers
 import FormalConjectures.ForMathlib.Computability.TuringMachine.Notation
 import FormalConjectures.ForMathlib.Computability.TuringMachine.PostTuringMachine
+import FormalConjectures.ForMathlib.Data.Finset.Card
 import FormalConjectures.ForMathlib.Data.Finset.Empty
 import FormalConjectures.ForMathlib.Data.Finset.OrdConnected
+import FormalConjectures.ForMathlib.Data.Finset.Powerset
 import FormalConjectures.ForMathlib.Data.Nat.Factorization.Basic
 import FormalConjectures.ForMathlib.Data.Nat.Full
 import FormalConjectures.ForMathlib.Data.Nat.MaxPrimeFac

FormalConjectures/WrittenOnTheWallII/GraphConjecture6.lean

@@ -13,16 +13,11 @@ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 See the License for the specific language governing permissions and
 limitations under the License.
 -/
-
-
 import FormalConjectures.Util.ProblemImports
 
-open Classical
-
-namespace WrittenOnTheWallII.GraphConjecture6
-
 open SimpleGraph
 
+namespace WrittenOnTheWallII.GraphConjecture6
 variable {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α]
 
 /--
@@ -33,7 +28,7 @@ For a connected graph `G` we have
 -/
 @[category research solved, AMS 5]
 theorem conjecture6 (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn : G.Connected) :
-    1 + n G - m G - a G ≤ Ls G := by
+    1 + n G - m G - α(G) ≤ Ls G := by
   sorry
 
 end WrittenOnTheWallII.GraphConjecture6

FormalConjectures/WrittenOnTheWallII/Test.lean

@@ -70,7 +70,7 @@ def Star5 : SimpleGraph (Fin 1 ⊕ Fin 5) := completeBipartiteGraph (Fin 1) (Fin
 /-! ### House Graph Tests -/
 
 @[category test, AMS 5]
-theorem house_indep : a HouseGraph = 2 := by
+theorem house_indep : α(HouseGraph) = 2 := by
   sorry
 
 @[category test, AMS 5]
@@ -141,7 +141,7 @@ theorem house_cvetkovic : cvetkovic HouseGraph = 3 := by
 /-! ### K4 Tests -/
 
 @[category test, AMS 5]
-theorem K4_indep : a K4 = 1 := by
+theorem K4_indep : α(K4) = 1 := by
   sorry
 
 @[category test, AMS 5]
@@ -212,7 +212,7 @@ theorem K4_cvetkovic : cvetkovic K4 = 1 := by
 /-! ### Petersen Graph Tests -/
 
 @[category test, AMS 5]
-theorem petersen_indep : a PetersenGraph = 4 := by
+theorem petersen_indep : α(PetersenGraph) = 4 := by
   sorry
 
 @[category test, AMS 5]
@@ -283,7 +283,7 @@ theorem petersen_cvetkovic : cvetkovic PetersenGraph = 4 := by
 /-! ### C6 Tests -/
 
 @[category test, AMS 5]
-theorem C6_indep : a C6 = 3 := by
+theorem C6_indep : α(C6) = 3 := by
   sorry
 
 @[category test, AMS 5]
@@ -354,7 +354,7 @@ theorem C6_cvetkovic : cvetkovic C6 = 3 := by
 /-! ### Star5 Tests -/
 
 @[category test, AMS 5]
-theorem Star5_indep : a Star5 = 5 := by
+theorem Star5_indep : α(Star5) = 5 := by
   sorry
 
 @[category test, AMS 5]