Basic

@[reducible, inline]

abbrev EGZ.FpVec (p d : ℕ) : Type

The vector space 𝔽_p^d, represented as d-tuples over ZMod p.

The definitions are total for every natural number p. Results using the field structure will carry a primality hypothesis.

Equations

• EGZ.FpVec p d = (Fin d → ZMod p)

def EGZ.HasZeroSumSubsequence {ι : Type u_1} (p : ℕ) {d : ℕ} (a : ι → FpVec p d) : Prop

A sequence contains p terms, at distinct positions, whose sum is zero.

Equations

• EGZ.HasZeroSumSubsequence p a = ∃ (I : Finset ι), I.card = p ∧ ∑ i ∈ I, a i = 0

def EGZ.EGZProperty (p d n : ℕ) : Prop

Every sequence of exactly n vectors in 𝔽_p^d has a zero-sum subsequence of length p.

Equations

• EGZ.EGZProperty p d n = ∀ (a : Fin n → EGZ.FpVec p d), EGZ.HasZeroSumSubsequence p a

def EGZ.IsPHollow (p : ℕ) {d s : ℕ} (v : Fin s → FpVec p d) : Prop

A family v₁, ..., vₛ is p-hollow when the only nonnegative integer combinations of total weight p that sum to zero put all their weight on a single vector. For prime p, this condition forces v to be injective.

Equations

• EGZ.IsPHollow p v = ∀ (α : Fin s → ℕ), ∑ i : Fin s, α i = p → (∑ i : Fin s, α i • v i = 0 ↔ ∃ (i : Fin s), α i = p)

def EGZ.AdmitsPHollowLength (p d s : ℕ) : Prop

There is a p-hollow family of s vectors in 𝔽_p^d.

Equations

• EGZ.AdmitsPHollowLength p d s = ∃ (v : Fin s → EGZ.FpVec p d), EGZ.IsPHollow p v

theorem EGZ.FpVec.card (p d : ℕ) [NeZero p] : Fintype.card (FpVec p d) = p ^ d

The cardinality of 𝔽_p^d (when p is nonzero, as it is for primes).

theorem EGZ.FpVec.characteristic_nsmul (p : ℕ) {d : ℕ} (x : FpVec p d) : p • x = 0

Every vector in 𝔽_p^d is killed by p. This also holds for the degenerate value p = 0, for which ZMod 0 is represented by the integers.

theorem EGZ.IsPHollow.injective {p d s : ℕ} {v : Fin s → FpVec p d} (hv : IsPHollow p v) (hp : 2 ≤ p) : Function.Injective v

A p-hollow parametrization has no repetitions once p ≥ 2.

theorem EGZ.IsPHollow.card_le {p d s : ℕ} {v : Fin s → FpVec p d} (hv : IsPHollow p v) (hp : Nat.Prime p) : s ≤ p ^ d

A prime-field p-hollow family has at most all the vectors in the space.

theorem EGZ.IsPHollow.sum_eq_zero_iff_constant {p d s : ℕ} {v : Fin s → FpVec p d} (hv : IsPHollow p v) {κ : Type u_1} [Fintype κ] (hcard : Fintype.card κ = p) (f : κ → Fin s) : ∑ x : κ, v (f x) = 0 ↔ ∃ (i : Fin s), ∀ (x : κ), f x = i

Operational form of hollowness: a p-term sum of members of a hollow family vanishes exactly when all p selected members have the same index.

The indexing type is arbitrary; the cardinality hypothesis is what records that the sum has exactly p terms.

theorem EGZ.IsPHollow.sum_fin_eq_zero_iff_constant {p d s : ℕ} {v : Fin s → FpVec p d} (hv : IsPHollow p v) (f : Fin p → Fin s) : ∑ x : Fin p, v (f x) = 0 ↔ ∃ (i : Fin s), ∀ (x : Fin p), f x = i

The common special case of sum_eq_zero_iff_constant indexed by Fin p.

theorem EGZ.AdmitsPHollowLength.le_pow {p d s : ℕ} (hp : Nat.Prime p) (h : AdmitsPHollowLength p d s) : s ≤ p ^ d

The existence predicate for hollow families inherits the ambient cardinality bound.

theorem EGZ.admitsPHollowLength_zero {p d : ℕ} (hp : 0 < p) : AdmitsPHollowLength p d 0

The empty family is hollow for every positive modulus.

theorem EGZ.EGZProperty.mono {p d m n : ℕ} (hmn : m ≤ n) (hm : EGZProperty p d m) : EGZProperty p d n

Exact-length EGZ properties persist when more terms are appended.

theorem EGZ.EGZProperty.pigeonhole_bound (p d : ℕ) : EGZProperty p d ((p - 1) * p ^ d + 1)

A crude pigeonhole upper bound. It is not intended to be sharp; its role is to establish that the least EGZ length is well-defined.

theorem EGZ.exists_egzProperty (p d : ℕ) : ∃ (n : ℕ), EGZProperty p d n

Some exact length has the EGZ property, uniformly for all natural p.

theorem EGZ.not_egzProperty_of_admitsPHollowLength {p d s : ℕ} (hp : 0 < p) (hadm : AdmitsPHollowLength p d s) : ¬EGZProperty p d (s * (p - 1))

Repeating each member of a positive-modulus hollow family only p - 1 times gives a sequence with no p-term zero sum.