Finite combinatorics used in the Wallace construction

This file formalizes the finite torsion-free-group bookkeeping used in Sections 4 and 5 of the current paper:

• the reindexing part of the triangular enumeration;
• extraction of finite bounded-independent sets;
• uniform integer dependence for bounded finite vectors;
• bounded deletion of at most |A| points.

The paper writes integer bounds as |c| ≤ M. We use Int.natAbs c ≤ M, which is definitionally the corresponding natural-number inequality.

def Wallace.FiniteCombinatorics.SupportedBelow {I : Type u} [LinearOrder I] (s : ℕ → I →₀ ℤ) (i : I) : Prop

The support condition in the triangular enumeration: every coordinate occurring in a term of the sequence lies strictly below its assigned index.

Equations

• Wallace.FiniteCombinatorics.SupportedBelow s i = ∀ (n : ℕ), ∀ j ∈ (s n).support, j < i

def Wallace.FiniteCombinatorics.BoundedIndependent {G : Type u} [AddCommGroup G] (M : ℕ) (X : Finset G) : Prop

A finite set is M-independent if every integer relation whose coefficients have absolute value at most M is trivial. This is the paper's definition, specialized to a finite set.

Equations

• Wallace.FiniteCombinatorics.BoundedIndependent M X = ∀ (c : G → ℤ), (∀ x ∈ X, (c x).natAbs ≤ M) → ∑ x ∈ X, c x • x = 0 → ∀ x ∈ X, c x = 0

def Wallace.FiniteCombinatorics.Forbidden {G : Type u} [AddCommGroup G] (M : ℕ) (B : Finset G) (x : G) : Prop

A point is forbidden over B if it satisfies one of the finitely many bounded equations used in the bounded-independence extraction argument.

Equations

• Wallace.FiniteCombinatorics.Forbidden M B x = ∃ (q : ℤ) (c : ↥B → ℤ), q ≠ 0 ∧ q.natAbs ≤ M ∧ (∀ (b : ↥B), (c b).natAbs ≤ M) ∧ q • x + ∑ b : ↥B, c b • ↑b = 0

def Wallace.FiniteCombinatorics.boundedIntFinset (M : ℕ) : Finset ℤ

The finite interval of integer coefficients of absolute value at most M.

Equations

• Wallace.FiniteCombinatorics.boundedIntFinset M = Finset.Icc (-↑M) ↑M

@[simp]

theorem Wallace.FiniteCombinatorics.mem_boundedIntFinset_iff {M : ℕ} {z : ℤ} : z ∈ boundedIntFinset M ↔ z.natAbs ≤ M

noncomputable def Wallace.FiniteCombinatorics.coefficientPatterns {G : Type u} (M : ℕ) (B : Finset G) : Finset (↥B → ℤ)

All bounded coefficient functions on a finite set.

Equations

• Wallace.FiniteCombinatorics.coefficientPatterns M B = Fintype.piFinset fun (x : ↥B) => Wallace.FiniteCombinatorics.boundedIntFinset M

@[simp]

theorem Wallace.FiniteCombinatorics.mem_coefficientPatterns_iff {G : Type u} {M : ℕ} {B : Finset G} {c : ↥B → ℤ} : c ∈ coefficientPatterns M B ↔ ∀ (b : ↥B), (c b).natAbs ≤ M

noncomputable def Wallace.FiniteCombinatorics.equationSolution {G : Type u} [AddCommGroup G] (B : Finset G) (q : ℤ) (c : ↥B → ℤ) : G

Choose a solution to the finite integer equation when one exists, and zero otherwise.

Equations

• Wallace.FiniteCombinatorics.equationSolution B q c = if h : ∃ (x : G), q • x + ∑ b : ↥B, c b • ↑b = 0 then Classical.choose h else 0

noncomputable def Wallace.FiniteCombinatorics.forbiddenFinset {G : Type u} [AddCommGroup G] (M : ℕ) (B : Finset G) : Finset G

A concrete finite set containing every forbidden point.

Equations

• One or more equations did not get rendered due to their size.

theorem Wallace.FiniteCombinatorics.forbidden_mem_forbiddenFinset {G : Type u} [AddCommGroup G] [IsAddTorsionFree G] {M : ℕ} {B : Finset G} {x : G} (hx : Forbidden M B x) : x ∈ forbiddenFinset M B

theorem Wallace.FiniteCombinatorics.boundedIndependent_insert_of_not_forbidden {G : Type u} [AddCommGroup G] [DecidableEq G] {M : ℕ} {Y : Finset G} {x : G} (hY : BoundedIndependent M Y) (hxY : x ∉ Y) (hx : ¬Forbidden M Y x) : BoundedIndependent M (insert x Y)

theorem Wallace.FiniteCombinatorics.exists_integer_dependence (s : ℕ) (b : Fin (s + 1) → Fin s → ℤ) : ∃ (coeff : Fin (s + 1) → ℤ), (∃ (i : Fin (s + 1)), coeff i ≠ 0) ∧ ∀ (j : Fin s), ∑ i : Fin (s + 1), coeff i * b i j = 0

s+1 integer vectors in ℤ^s have a nontrivial integer dependence.

We first obtain a rational dependence by the dimension theorem and then clear all denominators using mathlib's localization API.

@[reducible, inline]

abbrev Wallace.FiniteCombinatorics.BoundedInt (Q : ℕ) : Finset ℤ

Integer coefficients in [-Q,Q], as a finite type.

Equations

• Wallace.FiniteCombinatorics.BoundedInt Q = Wallace.FiniteCombinatorics.boundedIntFinset Q

structure Wallace.FiniteCombinatorics.BoundedVectorFamily (r Q : ℕ) : Type

All bounded vector families of every dimension at most r.

• size : Fin (r + 1)

  The dimension of the bounded integer vectors.

• vec : Fin (↑self.size + 1) → Fin ↑self.size → ↥(BoundedInt Q)

  A family of one more bounded integer vectors than its dimension.

@[instance_reducible]

instance Wallace.FiniteCombinatorics.instFintypeBoundedVectorFamily {r✝ Q✝ : ℕ} : Fintype (BoundedVectorFamily r✝ Q✝)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Wallace.FiniteCombinatorics.chosenIntegerDependence {r Q : ℕ} (B : BoundedVectorFamily r Q) : Fin (↑B.size + 1) → ℤ

Choose a nontrivial integer dependence among the bounded vectors.

Equations

• Wallace.FiniteCombinatorics.chosenIntegerDependence B = Classical.choose ⋯

noncomputable def Wallace.FiniteCombinatorics.familyDependenceBound {r Q : ℕ} (B : BoundedVectorFamily r Q) : ℕ

Bound the absolute values of the chosen integer dependence coefficients.

Equations

• Wallace.FiniteCombinatorics.familyDependenceBound B = Finset.univ.sup fun (i : Fin (↑B.size + 1)) => (Wallace.FiniteCombinatorics.chosenIntegerDependence B i).natAbs

noncomputable def Wallace.FiniteCombinatorics.integerDependenceBound (r Q : ℕ) : ℕ

A uniform bound for an integer dependence among any s+1 vectors in ℤ^s, for s ≤ r, whose entries have absolute value at most Q. Finiteness of the parameter space gives the uniformity; no unproved determinant estimate is used.

Equations

• Wallace.FiniteCombinatorics.integerDependenceBound r Q = Finset.univ.sup fun (B : Wallace.FiniteCombinatorics.BoundedVectorFamily r Q) => Wallace.FiniteCombinatorics.familyDependenceBound B

theorem Wallace.FiniteCombinatorics.exists_uniform_integer_dependence {r Q s : ℕ} (hs : s ≤ r) (b : Fin (s + 1) → Fin s → ℤ) (hb : ∀ (i : Fin (s + 1)) (j : Fin s), (b i j).natAbs ≤ Q) : ∃ (coeff : Fin (s + 1) → ℤ), (∃ (i : Fin (s + 1)), coeff i ≠ 0) ∧ (∀ (j : Fin s), ∑ i : Fin (s + 1), coeff i * b i j = 0) ∧ ∀ (i : Fin (s + 1)), (coeff i).natAbs ≤ integerDependenceBound r Q

def Wallace.FiniteCombinatorics.HasMixedRelation {G : Type u} [AddCommGroup G] (Q : ℕ) (A Y : Finset G) : Prop

A bounded relation using both the finite families A and Y.

Equations

• One or more equations did not get rendered due to their size.

def Wallace.FiniteCombinatorics.MixedRelationFree {G : Type u} [AddCommGroup G] (Q : ℕ) (A Y : Finset G) : Prop

No nontrivial relation of coefficient height at most Q uses both A and Y.

Equations

• Wallace.FiniteCombinatorics.MixedRelationFree Q A Y = ¬Wallace.FiniteCombinatorics.HasMixedRelation Q A Y

theorem Wallace.FiniteCombinatorics.mixedRelationFree_empty {G : Type u} [AddCommGroup G] (Q : ℕ) (A : Finset G) : MixedRelationFree Q A ∅

theorem Wallace.FiniteCombinatorics.exists_maximal_mixedRelationFree {G : Type u} [AddCommGroup G] [DecidableEq G] (Q : ℕ) (A X : Finset G) : ∃ Y ⊆ X, MixedRelationFree Q A Y ∧ ∀ x ∈ X, x ∉ Y → HasMixedRelation Q A (insert x Y)

A maximal relation-free subset of X. Maximality is by cardinality and therefore implies that adjoining any omitted point creates a mixed relation.

theorem Wallace.FiniteCombinatorics.mixedRelation_insert_witness {G : Type u} [AddCommGroup G] [DecidableEq G] {Q : ℕ} {A Y : Finset G} {x : G} (hY : MixedRelationFree Q A Y) (hxY : x ∉ Y) (hrel : HasMixedRelation Q A (insert x Y)) : ∃ (b : G → ℤ) (c : G → ℤ), (∀ a ∈ A, (b a).natAbs ≤ Q) ∧ (∀ z ∈ insert x Y, (c z).natAbs ≤ Q) ∧ (∃ a ∈ A, b a ≠ 0) ∧ c x ≠ 0 ∧ ∑ a ∈ A, b a • a + ∑ z ∈ insert x Y, c z • z = 0

noncomputable def Wallace.FiniteCombinatorics.deletionIndependenceBound (r Q : ℕ) : ℕ

The independence threshold from the current paper. Here integerDependenceBound r Q is the finite maximum denoted by B(r,Q), so this is exactly M(r,Q) = (r+1) B(r,Q) Q.

Equations

• Wallace.FiniteCombinatorics.deletionIndependenceBound r Q = (r + 1) * (Wallace.FiniteCombinatorics.integerDependenceBound r Q * Q)

theorem Wallace.FiniteCombinatorics.bounded_deletion {G : Type u} [AddCommGroup G] [DecidableEq G] (r Q : ℕ) (A X : Finset G) (hAr : A.card ≤ r) (hX : BoundedIndependent (deletionIndependenceBound r Q) X) : ∃ Y ⊆ X, (X \ Y).card ≤ A.card ∧ MixedRelationFree Q A Y

Bounded deletion (Lemma lem:bounded-deletion in the paper).

From an adequately bounded-independent finite set X, delete at most |A| points so that no bounded relation uses both A and the retained set. The threshold and the conclusion—including the sharp deletion count |X \ Y| ≤ |A|—are the ones in the paper.