shannon_capacity_c5
Provedanalysiscombinatoricslogicnumber-theory
Shannon capacity of C₅: The independence number of the 5-th tensor power of C₅ gives the capacity √5. Proved by Lovász (1979) using the theta function, introducing semidefinite programming to combinatorics. Exact capacity of C₇ is still unknown.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem shannon_capacity_c5 :
∃ (cap : ℝ),
cap = Real.sqrt 5 ∧
∀ eps : ℝ, 0 < eps →
∃ N : ℕ, ∀ (n : ℕ) (_ : N ≤ n) (ind : Fin n → Fin 5),
(∀ i j : Fin n, i ≠ j →
(ind i).val = (ind j).val ∨ (ind i).val + 1 ≡ (ind j).val [MOD 5]) →
(n : ℝ) ≤ (cap + eps) ^ n := by
sorrySource