Elementary abelian 2-groups attain the optimal bound

If g : Fin n → (Fin k → ZMod 2) has unique multiset sums — the only multiset of size n whose weighted sum of the g i equals ∑ i, g i is the all-ones multiset — then n - 1 ≤ k (elementaryAbelianTwoGroups_optimal). This is the optimality half of the elementary-abelian case of the minimum-modulus problem.

def MinModulus.UniqueMultisetSums {n k : ℕ} (g : Fin n → Fin k → ZMod 2) : Prop

g has unique multiset sums: the only multiset of size n whose weighted sum of the g i equals ∑ i, g i is the all-ones multiset.

Equations

• MinModulus.UniqueMultisetSums g = ∀ (m : Fin n → ℕ), ∑ i : Fin n, m i = n → ∑ i : Fin n, ↑(m i) • g i = ∑ i : Fin n, g i → ∀ (i : Fin n), m i = 1

theorem MinModulus.elementaryAbelianTwoGroups_optimal {n k : ℕ} (g : Fin n → Fin k → ZMod 2) (huniq : UniqueMultisetSums g) : n - 1 ≤ k