/-
Copyright 2026 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 FormalConjecturesUtilGreen's Open Problem 38
[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).
open Filter Setopen scoped Pointwise
namespace Green38$A - A$ intersects ${-1, 0, 1}^n$ only at $0$.
def IntersectsOnlyAtZero {n : ℕ} (A : Finset (𝔽₇ n)) : Prop :=
∀ a ∈ A - A, (∀ i, a i ∈ ({-1, 0, 1} : Finset (ZMod 7))) → a = 0The set of cardinalities of all subsets A where A - A intersects {-1, 0, 1}^n only at 0.
def ValidCardinalities (n : ℕ) : Set ℕ :=
{ (A.card) | (A : Finset (𝔽₇ n)) (_ : IntersectsOnlyAtZero A) }{0, 2, 4} is a valid independent set in C_7, giving cardinality 3.
@[category test, AMS 5]
theorem green_38.test_n1_lower :
3 ∈ ValidCardinalities 1 := ⊢ 3 ∈ ValidCardinalities 1
refine ⟨{![0], ![2], ![4]}, ?_, ⊢ {![0], ![2], ![4]}.card = 3 All goals completed! 🐙⟩
intro a a:𝔽₇ 1ha:a ∈ {![0], ![2], ![4]} - {![0], ![2], ![4]}⊢ (∀ (i : Fin 1), a i ∈ {-1, 0, 1}) → a = 0
a:𝔽₇ 1ha:a ∈ {![0], ![2], ![4]} - {![0], ![2], ![4]}⊢ a 0 = -1 ∨ a 0 = 0 ∨ a 0 = 1 → a = 0
-- a is a difference of elements from {0, 2, 4}, check all cases
⊢ Function.uncurry (fun x1 x2 => x1 - x2) (![0], ![4]) 0 = -1 ∨
Function.uncurry (fun x1 x2 => x1 - x2) (![0], ![4]) 0 = 0 ∨
Function.uncurry (fun x1 x2 => x1 - x2) (![0], ![4]) 0 = 1 →
Function.uncurry (fun x1 x2 => x1 - x2) (![0], ![4]) = 0a:𝔽₇ 1a✝:List.Mem a
(List.foldr (fun x IH => if ∀ y ∈ IH, (fun x1 x2 => x1 ≠ x2) x y then x :: IH else IH) []
(List.map (Function.uncurry fun x1 x2 => x1 - x2)
((List.map (Prod.mk ![0]) []).append
(List.map (Prod.mk ![2]) (List.insert ![0] (List.insert ![2] [![4]])) ++
(List.map (Prod.mk ![4]) (List.insert ![0] (List.insert ![2] [![4]])) ++ [])))))⊢ a 0 = -1 ∨ a 0 = 0 ∨ a 0 = 1 → a = 0
⊢ Function.uncurry (fun x1 x2 => x1 - x2) (![0], ![4]) 0 = -1 ∨
Function.uncurry (fun x1 x2 => x1 - x2) (![0], ![4]) 0 = 0 ∨
Function.uncurry (fun x1 x2 => x1 - x2) (![0], ![4]) 0 = 1 →
Function.uncurry (fun x1 x2 => x1 - x2) (![0], ![4]) = 0 ⊢ 4 = 1 ∨ 4 = 0 ∨ -4 = 1 → 4 = 0
All goals completed! 🐙
a:𝔽₇ 1a✝:List.Mem a
(List.foldr (fun x IH => if ∀ y ∈ IH, (fun x1 x2 => x1 ≠ x2) x y then x :: IH else IH) []
(List.map (Function.uncurry fun x1 x2 => x1 - x2)
((List.map (Prod.mk ![0]) []).append
(List.map (Prod.mk ![2]) (List.insert ![0] (List.insert ![2] [![4]])) ++
(List.map (Prod.mk ![4]) (List.insert ![0] (List.insert ![2] [![4]])) ++ [])))))⊢ a 0 = -1 ∨ a 0 = 0 ∨ a 0 = 1 → a = 0 a:𝔽₇ 1⊢ List.Mem a
(List.foldr (fun x IH => if ∀ y ∈ IH, (fun x1 x2 => x1 ≠ x2) x y then x :: IH else IH) []
(List.map (Function.uncurry fun x1 x2 => x1 - x2)
((List.map (Prod.mk ![0]) []).append
(List.map (Prod.mk ![2]) (List.insert ![0] (List.insert ![2] [![4]])) ++
(List.map (Prod.mk ![4]) (List.insert ![0] (List.insert ![2] [![4]])) ++ []))))) →
a 0 = -1 ∨ a 0 = 0 ∨ a 0 = 1 → a = 0
use a:𝔽₇ 1⊢ a = Function.uncurry (fun x1 x2 => x1 - x2) (![2], ![4]) ∨
a ∈
List.foldr (fun x IH => if ∀ y ∈ IH, (fun x1 x2 => x1 ≠ x2) x y then x :: IH else IH) []
(List.map (Function.uncurry fun x1 x2 => x1 - x2)
((List.map (Prod.mk ![2]) []).append
(List.map (Prod.mk ![4]) (List.insert ![0] (List.insert ![2] [![4]])) ++ []))) →
a 0 = -1 ∨ a 0 = 0 ∨ a 0 = 1 → a = 0 All goals completed! 🐙 ∘ List.mem_cons.1
The largest subset $A \subset \mathbb{F}_7^n$ for which $A - A$ intersects ${-1, 0, 1}^n$ only at $0$.
noncomputable def LargestAdmissibleCardinality : ℕ → ℝ := fun n ↦
(sSup (ValidCardinalities n) : ℕ)The lower bound constant $C_1 \approx 3.2578$ from [Po20].
noncomputable def C₁ : ℝ := (367 : ℝ) ^ (5⁻¹ : ℝ)The upper bound constant $C_2 \approx 3.3177$ from [La79].
noncomputable def C₂ : ℝ := (7 * Real.cos (Real.pi / 7)) / (1 + Real.cos (Real.pi / 7))Can we improve the lower bound?
@[category research open, AMS 5 11]
theorem green_38.lower :
let ans := (answer(sorry) : ℕ → ℝ)
ans ≤ᶠ[atTop] LargestAdmissibleCardinality ∧
∃ c > C₁, (fun n ↦ c ^ n) =O[atTop] ans := ⊢ let ans := sorry;
ans ≤ᶠ[atTop] LargestAdmissibleCardinality ∧ ∃ c > C₁, (fun n => c ^ n) =O[atTop] ans
All goals completed! 🐙Can we improve the best upper bound?
@[category research open, AMS 5 11]
theorem green_38.upper :
let ans := (answer(sorry) : ℕ → ℝ)
LargestAdmissibleCardinality ≤ᶠ[atTop] ans ∧
∃ c < C₂, ans =O[atTop] (fun n ↦ c ^ n) := ⊢ let ans := sorry;
LargestAdmissibleCardinality ≤ᶠ[atTop] ans ∧ ∃ c < C₂, ans =O[atTop] fun n => c ^ n
All goals completed! 🐙
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].
@[category research solved, AMS 5 11]
theorem green_38.variants.best_lower :
∀ ε > 0, ∀ᶠ n in atTop, (C₁ - ε) ^ n ≤ LargestAdmissibleCardinality n := ⊢ ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, (C₁ - ε) ^ n ≤ LargestAdmissibleCardinality n
All goals completed! 🐙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].
@[category research solved, AMS 5 11]
theorem green_38.variants.best_upper :
∀ ε > 0, ∀ᶠ n in atTop, LargestAdmissibleCardinality n ≤ (C₂ + ε) ^ n := ⊢ ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, LargestAdmissibleCardinality n ≤ (C₂ + ε) ^ n
All goals completed! 🐙0 is a valid cardinality, since the empty set vacuously satisfies the condition.
@[category test, AMS 5 11]
theorem green_38.test_zero_mem_validCardinalities {n : ℕ} :
0 ∈ ValidCardinalities n := n:ℕ⊢ 0 ∈ ValidCardinalities n
n:ℕ⊢ ∃ (_ : IntersectsOnlyAtZero ∅), ∅.card = 0
All goals completed! 🐙The set of valid cardinalities we take the supremum over is bounded above.
@[category test, AMS 5 11]
theorem green_38.test_bound_above {n : ℕ} :
BddAbove (ValidCardinalities n) := n:ℕ⊢ BddAbove (ValidCardinalities n)
n:ℕ⊢ 7 ^ n ∈ upperBounds (ValidCardinalities n)
n:ℕA:Finset (𝔽₇ n)w✝:IntersectsOnlyAtZero A⊢ A.card ≤ 7 ^ n
calc A.card
_ ≤ Fintype.card (𝔽₇ n) := A.card_le_univ
_ = _ := n:ℕA:Finset (𝔽₇ n)w✝:IntersectsOnlyAtZero A⊢ Fintype.card (𝔽₇ n) = 7 ^ n All goals completed! 🐙
end Green38