Graham's zero-sum conjecture

DefinitionGraham's zero-sum statement (Erdős Problem 541)#✓fully proved

This is the statement that for every prime \(p\) and every sequence \(a_0, \dots, a_{p-1}\) of residues modulo \(p\), not necessarily distinct, if there is a natural number \(r\) such that every nonempty set \(S \subseteq \{0, \dots, p-1\}\) with \(\sum_{i \in S} a_i = 0\) in \(\mathbb{Z}/p\mathbb{Z}\) has exactly \(r\) elements, then at most two distinct residues occur among \(a_0, \dots, a_{p-1}\).

def fixedZeroSumLengthTwoResidues : Prop :=
  ∀ p : ℕ, p.Prime → ∀ a : Fin p → ZMod p,
    (∃ r : ℕ, ∀ S : Finset (Fin p), S.Nonempty → ∑ i ∈ S, a i = 0 → S.card = r) →
      (Set.range a).ncard ≤ 2

Used by 1

Used byZero sums of a single length use at most two residues (Erdős Problem 541)

TheoremZero sums of a single length use at most two residues (Erdős Problem 541)#●ready to prove

For every prime \(p\) and every sequence \(a_0, \dots, a_{p-1}\) of residues modulo \(p\), not necessarily distinct, if there is a natural number \(r\) such that every nonempty set \(S \subseteq \{0, \dots, p-1\}\) with \(\sum_{i \in S} a_i = 0\) in \(\mathbb{Z}/p\mathbb{Z}\) has exactly \(r\) elements, then at most two distinct residues occur among \(a_0, \dots, a_{p-1}\).

Resolved true: Erdős and Szemerédi proved it for all large primes \(p\), and Gao, Hamidoune and Wang for every modulus.

public theorem_wanted fixedZeroSumLengthTwoResidues_holds : fixedZeroSumLengthTwoResidues

Sources

• T. F. Bloom, Erdős Problems, Problem #541, https://www.erdosproblems.com/541 (status PROVED (LEAN)); resolution: W. Gao, Y. O. Hamidoune and G. Wang, Distinct length modular zero-sum subsequences: a proof of Graham's conjecture, J. Number Theory (2010), 1425-1431, erdosproblems.com/541: proved by Erdős and Szemerédi for large p and by Gao, Hamidoune and Wang for all moduli, https://www.erdosproblems.com/541.

Uses 1

Statement usesGraham's zero-sum statement (Erdős Problem 541)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.