Green's Open Problem 38

References:

• 100 open problems
• [La79] Lovász, László. "On the Shannon capacity of a graph." IEEE Transactions on Information theory 25.1 (1979): 1-7.
• [Po20] Polak, Sven. "New methods in coding theory: Error-correcting codes and the Shannon capacity." arXiv preprint arXiv:2005.02945 (2020).

@[reducible, inline]

abbrev Green38.𝔽₇ (n : ℕ) : Type

The vector space $\mathbb{F}_7^n$.

Equations

• Green38.𝔽₇ n = (Fin n → ZMod 7)

def Green38.IntersectsOnlyAtZero {n : ℕ} (A : Finset (𝔽₇ n)) : Prop

$A - A$ intersects $\{-1, 0, 1\}^n$ only at $0$.

Equations

• Green38.IntersectsOnlyAtZero A = ∀ a ∈ A - A, (∀ (i : Fin n), a i ∈ {-1, 0, 1}) → a = 0

def Green38.ValidCardinalities (n : ℕ) : Set ℕ

The set of cardinalities of all subsets A where A - A intersects {-1, 0, 1}^n only at 0.

Equations

• Green38.ValidCardinalities n = {x : ℕ | ∃ (A : Finset (Green38.𝔽₇ n)) (_ : Green38.IntersectsOnlyAtZero A), A.card = x}

theorem Green38.green_38.test_n1_lower : 3 ∈ ValidCardinalities 1

{0, 2, 4} is a valid independent set in C_7, giving cardinality 3.

noncomputable def Green38.LargestAdmissibleCardinality : ℕ → ℝ

The largest subset $A \subset \mathbb{F}_7^n$ for which $A - A$ intersects $\{-1, 0, 1\}^n$ only at $0$.

Equations

• Green38.LargestAdmissibleCardinality n = ↑(sSup (Green38.ValidCardinalities n))

noncomputable def Green38.C₁ : ℝ

The lower bound constant $C_1 \approx 3.2578$ from [Po20].

Equations

• Green38.C₁ = 367 ^ 5⁻¹

noncomputable def Green38.C₂ : ℝ

The upper bound constant $C_2 \approx 3.3177$ from [La79].

Equations

• Green38.C₂ = 7 * Real.cos (Real.pi / 7) / (1 + Real.cos (Real.pi / 7))

theorem Green38.green_38.lower : have ans := sorry; ans ≤ᶠ[Filter.atTop] LargestAdmissibleCardinality ∧ ∃ c > C₁, (fun (n : ℕ) => c ^ n) =O[Filter.atTop] ans

Can we improve the lower bound?

theorem Green38.green_38.upper : have ans := sorry; LargestAdmissibleCardinality ≤ᶠ[Filter.atTop] ans ∧ ∃ c < C₂, ans =O[Filter.atTop] fun (n : ℕ) => c ^ n

Can we improve the best upper bound?

theorem Green38.green_38.variants.best_lower (ε : ℝ) : ε > 0 → ∀ᶠ (n : ℕ) in Filter.atTop, (C₁ - ε) ^ n ≤ LargestAdmissibleCardinality n

The current best lower bound is $(C_1 - o(1))^n \leqslant |A|$ where $C_1 = 367^{1/5} \approx 3.2578$ [Po20, Section 9.1].

theorem Green38.green_38.variants.best_upper (ε : ℝ) : ε > 0 → ∀ᶠ (n : ℕ) in Filter.atTop, LargestAdmissibleCardinality n ≤ (C₂ + ε) ^ n

The current best upper bound is $|A| \leqslant (C_2 + o(1))^n$ where $C_2 = \frac{7 \cos(\pi/7)}{1 + \cos(\pi/7)} \approx 3.3177$ [La79, Corollary 5].

theorem Green38.green_38.test_zero_mem_validCardinalities {n : ℕ} : 0 ∈ ValidCardinalities n

0 is a valid cardinality, since the empty set vacuously satisfies the condition.

theorem Green38.green_38.test_bound_above {n : ℕ} : BddAbove (ValidCardinalities n)

The set of valid cardinalities we take the supremum over is bounded above.