Green's Open Problem 26

References:

• [Gr24] Green, Ben. "100 open problems." (2024).
• [JLP92] Jaeger, François, et al. "Group connectivity of graphs—a nonhomogeneous analogue of nowhere-zero flow properties." Journal of Combinatorial Theory, Series B 56.2 (1992): 165-182.
• [ALM91] Alon, Noga, Nathan Linial, and Roy Meshulam. "Additive bases of vector spaces over prime fields." Journal of Combinatorial Theory, Series A 57.2 (1991): 203-210.
• [Yu25] Yu, Yang. "Note on the Additive Basis Conjecture." arXiv preprint arXiv:2510.01300 (2025).

@[reducible, inline]

abbrev Green26.𝔽 (p n : ℕ) [Fact (Nat.Prime p)] : Type

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

Equations

• Green26.𝔽 p n = (Fin n → ZMod p)

@[reducible, inline]

abbrev Green26.𝔽₃ (n : ℕ) : Type

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

Equations

• Green26.𝔽₃ n = Green26.𝔽 3 n

def Green26.StandardCube {p : ℕ} [Fact (Nat.Prime p)] (n : ℕ) : Set (𝔽 p n)

The standard cube in $\mathbb{F}_p^n$ is the set of points with coordinates in $\{0, 1\}$.

Equations

• Green26.StandardCube n = {x : Green26.𝔽 p n | ∀ (i : Fin n), x i = 0 ∨ x i = 1}

def Green26.IsCube {p n : ℕ} [Fact (Nat.Prime p)] (A : Set (𝔽 p n)) : Prop

A cube is the image of $\lbrace 0, 1\rbrace^n$ under a linear automorphism.

Equations

• Green26.IsCube A = ∃ (φ : Green26.𝔽 p n ≃ₗ[ZMod p] Green26.𝔽 p n), A = ⇑φ '' Green26.StandardCube n

theorem Green26.green_26 (n : ℕ) (A : Fin 100 → Set (𝔽₃ n)) : (∀ (i : Fin 100), IsCube (A i)) → ∑ i : Fin 100, A i = Set.univ

Let $A_1, \dots, A_{100}$ be "cubes" in $\mathbb{F}^n_3$. Is it true that $A_1 + \dots + A_{100} = \mathbb{F}^n_3$?

theorem Green26.green_26.variants.yu25 (n : ℕ) (A : Fin 4 → Set (𝔽₃ n)) : (∀ (i : Fin 4), IsCube (A i)) → ∑ i : Fin 4, A i = Set.univ

[Yu25] has solved the original problem (with 100 replaced by 4)

theorem Green26.green_26.variants.alm91 (p : ℕ) [Fact (Nat.Prime p)] : ∃ (k : ℕ → ℕ), ((fun (n : ℕ) => ↑(k n)) =O[Filter.atTop] fun (n : ℕ) => Real.log ↑n) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Fin (k n) → Set (𝔽 p n)), (∀ (i : Fin (k n)), IsCube (A i)) → ∑ i : Fin (k n), A i = Set.univ

[ALM91] showed that if 100 is replaced by $\leq c(p) \log n$ then the result is true for $\mathbb{F}^n_p$.

theorem Green26.green_26.variants.open : sorry ↔ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ (C : ℕ), ∀ (n : ℕ) (A : Fin C → Set (𝔽 p n)), (∀ (i : Fin C), IsCube (A i)) → ∑ i : Fin C, A i = Set.univ

The analogous problem in $\mathbb{F}^n_p$ remains open. [Gr24]