One finite character-fusion stage

This module turns the bounded-deletion conclusion into the exact short-relation compatibility required by the uniform Kronecker lemma. It is the finite algebraic heart of one fusion stage.

theorem Wallace.disjoint_of_mixedRelationFree {G : Type u} [AddCommGroup G] {A Y : Finset G} {Q : ℕ} (hQ : 1 ≤ Q) (hfree : FiniteCombinatorics.MixedRelationFree Q A Y) : Disjoint A Y

A short-relation-free old/new pair is disjoint as soon as the height bound contains 1.

theorem Wallace.stageTarget_respectsRelationsUpTo {G : Type u} [AddCommGroup G] [DecidableEq G] {A Y : Finset G} {Q : ℕ} (hQ : 1 ≤ Q) (hfree : FiniteCombinatorics.MixedRelationFree Q A Y) (old : G →+ UnitAddCircle) : RespectsRelationsUpTo Q (Wallace.unionTuple✝ A Y) (Wallace.stageTarget✝ A Y old)

Bounded deletion makes the finite fusion target compatible with every relation up to Q.

theorem Wallace.exists_character_fusion_stage {G : Type u} [AddCommGroup G] [DecidableEq G] {A Y : Finset G} {Q : ℕ} (hQ : 1 ≤ Q) (hfree : FiniteCombinatorics.MixedRelationFree Q A Y) (old : G →+ UnitAddCircle) {eps : ℝ} (hbound : IsUniformKroneckerBound (A ∪ Y).card eps Q) : ∃ (next : G →+ UnitAddCircle), (∀ x ∈ A, ‖next x - old x‖ < eps) ∧ ∀ y ∈ Y, ‖next y‖ < eps

One application of uniform Kronecker performs a finite fusion stage.