Sums of cubes in ternary vector spaces

DefinitionThe standard cube in \(\mathbb{F}_3^n\)#βœ“fully proved

For \(n \in \mathbb{N}\), the standard cube is the set \(\{0, 1\}^n \subseteq \mathbb{F}_3^n\) of vectors each of whose coordinates is \(0\) or \(1\).

def cubeOrigin (n : β„•) : Set (Fin n β†’ ZMod 3) :=
  { x | βˆ€ i : Fin n, x i = 0 ∨ x i = 1 }
Used by 1
Used byCubes in \(\mathbb{F}_3^n\)

DefinitionCubes in \(\mathbb{F}_3^n\)#βœ“fully proved

A set \(A \subseteq \mathbb{F}_3^n\) is a cube if there is an \(\mathbb{F}_3\)-linear automorphism \(e\) of \(\mathbb{F}_3^n\) with \(A = e(\{0, 1\}^n)\), the image of the standard cube \(\{0, 1\}^n\) under \(e\).

def IsCube (n : β„•) (A : Set (Fin n β†’ ZMod 3)) : Prop :=
  βˆƒ e : (Fin n β†’ ZMod 3) ≃ₗ[ZMod 3] (Fin n β†’ ZMod 3),
    A = Set.image (e : (Fin n β†’ ZMod 3) β†’ (Fin n β†’ ZMod 3)) (cubeOrigin n)
Uses 1 Β· Used by 1
Statement usesThe standard cube in \(\mathbb{F}_3^n\)
Used byGreen's problem on sums of \(100\) cubes in \(\mathbb{F}_3^n\)

DefinitionA sumset of \(100\) sets equal to \(\mathbb{F}_3^n\)#βœ“fully proved

For sets \(A_1, \dots, A_{100} \subseteq \mathbb{F}_3^n\), the property that every \(v \in \mathbb{F}_3^n\) can be written as \(v = a_1 + \dots + a_{100}\) with \(a_i \in A_i\) for each \(i\), that is, \(A_1 + \dots + A_{100} = \mathbb{F}_3^n\).

def SumsetEqUniv (n : β„•) (A : Fin 100 β†’ Set (Fin n β†’ ZMod 3)) : Prop :=
  βˆ€ v : Fin n β†’ ZMod 3,
    βˆƒ a : Fin 100 β†’ Fin n β†’ ZMod 3,
      (βˆ€ i, a i ∈ A i) ∧ v = Finset.sum (Finset.univ : Finset (Fin 100)) a
Used by 1
Used byGreen's problem on sums of \(100\) cubes in \(\mathbb{F}_3^n\)

DefinitionGreen's problem on sums of \(100\) cubes in \(\mathbb{F}_3^n\)#βœ“fully proved

The statement that for every \(n \ge 1\) and every family \(A_1, \dots, A_{100}\) of cubes in \(\mathbb{F}_3^n\) (not necessarily distinct), that is, images of \(\{0, 1\}^n\) under linear automorphisms of \(\mathbb{F}_3^n\), the sumset \(A_1 + \dots + A_{100}\) is all of \(\mathbb{F}_3^n\).

def conjecture : Prop :=
  βˆ€ (n : β„•), 1 ≀ n β†’
    βˆ€ (A : Fin 100 β†’ Set (Fin n β†’ ZMod 3)),
      (βˆ€ i, IsCube n (A i)) β†’ SumsetEqUniv n A
Uses 2 Β· Used by 1
Statement usesCubes in \(\mathbb{F}_3^n\) Β· A sumset of \(100\) sets equal to \(\mathbb{F}_3^n\)
Used byAny \(100\) cubes sum to all of \(\mathbb{F}_3^n\)

TheoremAny \(100\) cubes sum to all of \(\mathbb{F}_3^n\)#●ready to prove

For every \(n \ge 1\) and every family \(A_1, \dots, A_{100}\) of cubes in \(\mathbb{F}_3^n\) (not necessarily distinct), that is, images of \(\{0, 1\}^n\) under linear automorphisms of \(\mathbb{F}_3^n\), the sumset \(A_1 + \dots + A_{100}\) is all of \(\mathbb{F}_3^n\).

Yang Yu proves that over \(\mathbb{F}_3\) the union of any four linear bases is an additive basis, so any four cubes already sum to \(\mathbb{F}_3^n\), and the remaining summands can be taken to be \(0\). Ben Green's author-maintained 100 Open Problems (December 2025) marks this problem, current Problem 26, solved on that basis; the analogue over \(\mathbb{F}_p\) remains open.

public theorem_wanted conjecture_holds : conjecture
Sources
  • Yang Yu, The Permanent Rank of a Matrix (Part Three) Note on the Additive Basis Conjecture, arXiv:2510.01300v2, https://arxiv.org/abs/2510.01300v2.
Uses 1
Statement usesGreen's problem on sums of \(100\) cubes in \(\mathbb{F}_3^n\)
4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.