Finite growth with disjoint exchange supports

Binary sums grow by adding one translate. A polynomial initial stage and a multiplicative stage produce more than half of the group; two disjoint such families then cover the whole group.

def EGZ.Expansion.binarySums {E : Type u_1} {G : Type u_3} [AddCommGroup G] [DecidableEq G] (shift : E → G) (F : Finset E) : Finset G

All sums obtained by choosing any subfamily of a finite family.

Equations

• EGZ.Expansion.binarySums shift F = Finset.image (fun (J : Finset E) => ∑ e ∈ J, shift e) F.powerset

@[simp]

theorem EGZ.Expansion.binarySums_empty {E : Type u_1} {G : Type u_3} [AddCommGroup G] [DecidableEq G] (shift : E → G) : binarySums shift ∅ = {0}

theorem EGZ.Expansion.zero_mem_binarySums {E : Type u_1} {G : Type u_3} [AddCommGroup G] [DecidableEq G] (shift : E → G) (F : Finset E) : 0 ∈ binarySums shift F

theorem EGZ.Expansion.binarySums_insert {E : Type u_1} {G : Type u_3} [DecidableEq E] [AddCommGroup G] [DecidableEq G] (shift : E → G) (F : Finset E) {e : E} (he : e ∉ F) : binarySums shift (insert e F) = translate (binarySums shift F) (shift e) ∪ binarySums shift F

theorem EGZ.Expansion.exists_bool_choice_of_mem_binarySums {E : Type u_1} {G : Type u_3} [AddCommGroup G] [DecidableEq G] (shift : E → G) (F : Finset E) {x : G} (hx : x ∈ binarySums shift F) : ∃ (choice : ↥F → Bool), (∑ e : ↥F, if choice e = true then shift ↑e else 0) = x

Subset sums can be expressed as Boolean choices indexed by the selected family, the form used by the exchange-completion argument.

def EGZ.Expansion.usedAtoms {E : Type u_1} {A : Type u_2} [DecidableEq A] (support : E → Finset A) (F : Finset E) : Finset A

Atoms reserved by a family of exchanges.

Equations

• EGZ.Expansion.usedAtoms support F = F.biUnion support

theorem EGZ.Expansion.card_usedAtoms_le {E : Type u_1} {A : Type u_2} [DecidableEq A] (support : E → Finset A) (F : Finset E) {B : ℕ} (hB : ∀ (e : E), (support e).card ≤ B) : (usedAtoms support F).card ≤ B * F.card

@[simp]

theorem EGZ.Expansion.usedAtoms_insert {E : Type u_1} {A : Type u_2} [DecidableEq E] [DecidableEq A] (support : E → Finset A) (F : Finset E) (e : E) : usedAtoms support (insert e F) = support e ∪ usedAtoms support F

theorem EGZ.Expansion.new_exchange_of_positive_boundary {E : Type u_1} {A : Type u_2} {G : Type u_3} [DecidableEq A] [AddCommGroup G] [DecidableEq G] (support : E → Finset A) (shift : E → G) (hzero : ∀ (e : E), support e = ∅ → shift e = 0) (F : Finset E) (Y : Finset G) {e : E} (he : Disjoint (support e) (usedAtoms support F)) (hpos : 0 < boundary Y (shift e)) : e ∉ F

def EGZ.Expansion.Admissible {E : Type u_1} {A : Type u_2} [DecidableEq A] (support : E → Finset A) (U : Finset A) (F : Finset E) : Prop

A family uses disjoint supports and avoids all previously reserved atoms.

Equations

• EGZ.Expansion.Admissible support U F = (((↑F).Pairwise fun (e f : E) => Disjoint (support e) (support f)) ∧ Disjoint (EGZ.Expansion.usedAtoms support F) U)

theorem EGZ.Expansion.admissible_empty {E : Type u_1} {A : Type u_2} [DecidableEq A] (support : E → Finset A) (U : Finset A) : Admissible support U ∅

theorem EGZ.Expansion.Admissible.insert {E : Type u_1} {A : Type u_2} [DecidableEq E] [DecidableEq A] {support : E → Finset A} {U : Finset A} {F : Finset E} (hF : Admissible support U F) {e : E} (he : Disjoint (support e) (U ∪ usedAtoms support F)) : Admissible support U (Insert.insert e F)

theorem EGZ.Expansion.iterate_binary_growth {E : Type u_1} {A : Type u_2} {G : Type u_3} [DecidableEq E] [DecidableEq A] [AddCommGroup G] [DecidableEq G] (support : E → Finset A) (shift : E → G) (U : Finset A) (F₀ : Finset E) (hF₀ : Admissible support U F₀) (N : ℕ) (target : ℕ → ℝ) (stop : Finset E → Prop) (hstart : target 0 ≤ ↑(binarySums shift F₀).card) (step : ∀ i < N, ∀ (F : Finset E), F₀ ⊆ F → Admissible support U F → F.card ≤ F₀.card + i → ¬stop F → target i ≤ ↑(binarySums shift F).card → ↑(binarySums shift F).card < target (i + 1) → ∃ e ∉ F, Disjoint (support e) (U ∪ usedAtoms support F) ∧ target (i + 1) ≤ ↑(binarySums shift (insert e F)).card) : ∃ (F : Finset E), F₀ ⊆ F ∧ Admissible support U F ∧ F.card ≤ F₀.card + N ∧ (stop F ∨ target N ≤ ↑(binarySums shift F).card)

A finite greedy iteration, retaining the current family whenever its size already meets the next target. The optional stopping predicate is returned explicitly.

def EGZ.Expansion.growthDenominator (d : ℕ) : ℕ

A convenient integer reciprocal step for polynomial growth.

Equations

• EGZ.Expansion.growthDenominator d = 6 * d * d * 2 ^ d

theorem EGZ.Expansion.growthDenominator_pos {d : ℕ} (hd : 0 < d) : 0 < growthDenominator d

theorem EGZ.Expansion.polynomial_growth_step {d : ℕ} (hd : 0 < d) {x : ℝ} (hx : 1 ≤ x) : (x + (↑(growthDenominator d))⁻¹) ^ d ≤ x ^ d + x ^ (d - 1) / (6 * ↑d)

Increasing the root of the set size by a fixed reciprocal costs no more than the boundary provided by the basis estimate.

theorem EGZ.Expansion.exists_polynomial_growth {E : Type u_1} {A : Type u_2} [DecidableEq A] {p d B budget : ℕ} [Fact (Nat.Prime p)] (support : E → Finset A) (shift : E → FpCoord p d) (hd : 0 < d) (hB : ∀ (e : E), (support e).card ≤ B) (hzero : ∀ (e : E), support e = ∅ → shift e = 0) (hbasis : ∀ (U : Finset A), U.card ≤ budget → ∃ (b : Module.Basis (Fin d) (ZMod p) (FpCoord p d)), ∀ (i : Fin d), ∃ (e : E), Disjoint (support e) U ∧ shift e = b i) (U : Finset A) (N : ℕ) (hbudget : U.card + B * N ≤ budget) (hsmall : 2 * (1 + ↑N / ↑(growthDenominator d)) ≤ ↑p) : ∃ (F : Finset E), Admissible support U F ∧ F.card ≤ N ∧ (1 + ↑N / ↑(growthDenominator d)) ^ d ≤ ↑(binarySums shift F).card

theorem EGZ.Expansion.exists_multiplicative_growth {E : Type u_1} {A : Type u_2} [DecidableEq A] {p d B budget : ℕ} [NeZero p] [Fact (Nat.Prime p)] (support : E → Finset A) (shift : E → FpCoord p d) (hB : ∀ (e : E), (support e).card ≤ B) (hzero : ∀ (e : E), support e = ∅ → shift e = 0) {a : ℝ} (ha : 0 < a) (hgrowth : ∀ (U : Finset A), U.card ≤ budget → ∀ (Y : Finset (FpCoord p d)), 2 * Y.card ≤ p ^ d → ∃ (e : E), Disjoint (support e) U ∧ a * ↑Y.card ≤ ↑p * ↑(boundary Y (shift e))) (U : Finset A) (F₀ : Finset E) (hF₀ : Admissible support U F₀) {seed : ℝ} (hseed : 0 < seed) (hsize : seed ≤ ↑(binarySums shift F₀).card) (N : ℕ) (hbudget : U.card + B * (F₀.card + N) ≤ budget) (hlarge : ↑p ^ d < 2 * (seed * (1 + ↑N * a / ↑p))) : ∃ (F : Finset E), F₀ ⊆ F ∧ Admissible support U F ∧ F.card ≤ F₀.card + N ∧ p ^ d < 2 * (binarySums shift F).card

theorem EGZ.Expansion.Admissible.union {E : Type u_1} {A : Type u_2} [DecidableEq E] [DecidableEq A] {support : E → Finset A} {U : Finset A} {F J : Finset E} (hF : Admissible support U F) (hJ : Admissible support (U ∪ usedAtoms support F) J) : Admissible support U (F ∪ J)

theorem EGZ.Expansion.add_mem_binarySums_union {E : Type u_1} {A : Type u_2} {G : Type u_3} [DecidableEq E] [DecidableEq A] [AddCommGroup G] [DecidableEq G] (support : E → Finset A) (shift : E → G) (hzero : ∀ (e : E), support e = ∅ → shift e = 0) {F J : Finset E} (hdis : Disjoint (usedAtoms support F) (usedAtoms support J)) {x y : G} (hx : x ∈ binarySums shift F) (hy : y ∈ binarySums shift J) : x + y ∈ binarySums shift (F ∪ J)

theorem EGZ.Expansion.binarySums_cover_of_two_large {E : Type u_1} {A : Type u_2} {G : Type u_3} [DecidableEq E] [DecidableEq A] [AddCommGroup G] [DecidableEq G] [Fintype G] (support : E → Finset A) (shift : E → G) (hzero : ∀ (e : E), support e = ∅ → shift e = 0) {F J : Finset E} (hdis : Disjoint (usedAtoms support F) (usedAtoms support J)) (hF : Fintype.card G < 2 * (binarySums shift F).card) (hJ : Fintype.card G < 2 * (binarySums shift J).card) : binarySums shift (F ∪ J) = Finset.univ

theorem EGZ.Expansion.exists_half_binarySums {E : Type u_1} {A : Type u_2} [DecidableEq A] {p d B budget : ℕ} [NeZero p] [Fact (Nat.Prime p)] (support : E → Finset A) (shift : E → FpCoord p d) (hd : 0 < d) (hB : ∀ (e : E), (support e).card ≤ B) (hzero : ∀ (e : E), support e = ∅ → shift e = 0) (hbasis : ∀ (U : Finset A), U.card ≤ budget → ∃ (b : Module.Basis (Fin d) (ZMod p) (FpCoord p d)), ∀ (i : Fin d), ∃ (e : E), Disjoint (support e) U ∧ shift e = b i) {a : ℝ} (ha : 0 < a) (hgrowth : ∀ (U : Finset A), U.card ≤ budget → ∀ (Y : Finset (FpCoord p d)), 2 * Y.card ≤ p ^ d → ∃ (e : E), Disjoint (support e) U ∧ a * ↑Y.card ≤ ↑p * ↑(boundary Y (shift e))) (U : Finset A) (n m : ℕ) (hbudget : U.card + B * (n + m) ≤ budget) (hsmall : 2 * (1 + ↑n / ↑(growthDenominator d)) ≤ ↑p) (hlarge : ↑p ^ d < 2 * ((1 + ↑n / ↑(growthDenominator d)) ^ d * (1 + ↑m * a / ↑p))) : ∃ (F : Finset E), Admissible support U F ∧ F.card ≤ n + m ∧ p ^ d < 2 * (binarySums shift F).card

theorem EGZ.Expansion.exists_binarySums_cover_finite {E : Type u_1} {A : Type u_2} [DecidableEq A] {p d B budget : ℕ} [NeZero p] [Fact (Nat.Prime p)] (support : E → Finset A) (shift : E → FpCoord p d) (hd : 0 < d) (hB : ∀ (e : E), (support e).card ≤ B) (hzero : ∀ (e : E), support e = ∅ → shift e = 0) (hbasis : ∀ (U : Finset A), U.card ≤ budget → ∃ (b : Module.Basis (Fin d) (ZMod p) (FpCoord p d)), ∀ (i : Fin d), ∃ (e : E), Disjoint (support e) U ∧ shift e = b i) {a : ℝ} (ha : 0 < a) (hgrowth : ∀ (U : Finset A), U.card ≤ budget → ∀ (Y : Finset (FpCoord p d)), 2 * Y.card ≤ p ^ d → ∃ (e : E), Disjoint (support e) U ∧ a * ↑Y.card ≤ ↑p * ↑(boundary Y (shift e))) (n m : ℕ) (hbudget : B * (2 * (n + m)) ≤ budget) (hsmall : 2 * (1 + ↑n / ↑(growthDenominator d)) ≤ ↑p) (hlarge : ↑p ^ d < 2 * ((1 + ↑n / ↑(growthDenominator d)) ^ d * (1 + ↑m * a / ↑p))) : ∃ (F : Finset E), Admissible support ∅ F ∧ F.card ≤ 2 * (n + m) ∧ (usedAtoms support F).card ≤ budget ∧ binarySums shift F = Finset.univ

Explicit finite criterion for complete binary-sum coverage using pairwise disjoint exchange supports.

theorem EGZ.Expansion.exists_binary_growth_parameters (d B : ℕ) (hd : 0 < d) (c : ℝ) (hc : 0 < c) : ∃ (a : ℝ) (p₀ : ℕ), 0 < a ∧ ∀ (p : ℕ), p₀ ≤ p → ∃ (n : ℕ), ↑B * (2 * (↑n + ↑n)) ≤ c * ↑p ∧ 2 * (1 + ↑n / ↑(growthDenominator d)) ≤ ↑p ∧ ↑p ^ d < 2 * ((1 + ↑n / ↑(growthDenominator d)) ^ d * (1 + ↑n * a / ↑p))

Uniform numerical parameters for a linear atom budget. The two stages may have equal length; a deliberately generous fixed growth rate suffices.

theorem EGZ.Expansion.exists_binarySums_cover_uniform (d B : ℕ) (hd : 0 < d) (c : ℝ) (hc : 0 < c) : ∃ (a : ℝ) (p₀ : ℕ), 0 < a ∧ ∀ (p : ℕ) (x : NeZero p) (x_1 : Fact (Nat.Prime p)), p₀ ≤ p → ∀ (E : Type u) (A : Type v) (x_2 : DecidableEq E) (x_3 : DecidableEq A) (support : E → Finset A) (shift : E → FpCoord p d), (∀ (e : E), (support e).card ≤ B) → (∀ (e : E), support e = ∅ → shift e = 0) → (∀ (U : Finset A), ↑U.card ≤ c * ↑p → ∃ (b : Module.Basis (Fin d) (ZMod p) (FpCoord p d)), ∀ (i : Fin d), ∃ (e : E), Disjoint (support e) U ∧ shift e = b i) → (∀ (U : Finset A), ↑U.card ≤ c * ↑p → ∀ (Y : Finset (FpCoord p d)), 2 * Y.card ≤ p ^ d → ∃ (e : E), Disjoint (support e) U ∧ a * ↑Y.card ≤ ↑p * ↑(boundary Y (shift e))) → ∃ (F : Finset E), ((↑F).Pairwise fun (e f : E) => Disjoint (support e) (support f)) ∧ ↑(usedAtoms support F).card ≤ c * ↑p ∧ binarySums shift F = Finset.univ

For a sufficiently large fixed growth rate, a linear atom budget supports a family of disjoint exchanges whose binary sums cover the group. The growth rate and prime threshold are chosen before all exchange data.