The separation dichotomy

For a finite group G acting on Ω and A B : Finset Ω, the averaging identity ∑_{g : G} #((g • A) ∩ B) = ∑_{a ∈ A} #(B ∩ orbit a) · #(stabilizer a) gives a dichotomy: if every orbit meeting both A and B has at least #A · #B points, then either some g separates A from B, or #((g • A) ∩ B) = 1 for every g and A, B lie in a single common orbit of size exactly #A · #B. For the regular action of G on itself the second case is an exact factorization G = B · A⁻¹, and in ZMod n it is a tiling B ⊕ (-A) = ℤ/n.

Main results

• TotD.sum_card_smul_inter: the averaging identity.
• TotD.separation_dichotomy: the dichotomy (no transitivity assumed).
• TotD.separation_of_forall_lt: common orbits of size greater than #A · #B force separation.
• TotD.forall_card_smul_inter_eq_one_iff_factorization: the regular case.
• TotD.forall_card_vadd_inter_eq_one_iff_tiling: the ZMod n case.
• TotD.tiling_witness_zmod12, TotD.separating_witness_zmod12: examples in ℤ/12, by decide.

References

• J. Araújo, P. J. Cameron, B. Steinberg, Between primitive and 2-transitive: synchronization and its friends, EMS Surv. Math. Sci. 4 (2017) 101–184, §5.2.
• P. J. Cameron, Synchronization, LTCC lecture notes, 2010, Lecture 3.

The counting engine: fibres and the averaging identity

theorem TotD.card_smul_fiber_eq_card_stabilizer {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] {a b : Ω} (hab : b ∈ MulAction.orbit G a) : {g : G | g • a = b}.card = Nat.card ↥(MulAction.stabilizer G a)

The transporter fibre {g | g • a = b} is a left coset of stabilizer G a when b lies in the orbit of a, so it has #(stabilizer G a) elements. (Non-transitive generalization of the fibre count in SectionRegular.lean.)

theorem TotD.card_smul_fiber_eq_zero {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] {a b : Ω} (hab : b ∉ MulAction.orbit G a) : {g : G | g • a = b}.card = 0

The transporter fibre is empty when b is not in the orbit of a.

theorem TotD.sum_card_smul_inter {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] (A B : Finset Ω) : ∑ g : G, (g • A ∩ B).card = ∑ a ∈ A, (↑B ∩ MulAction.orbit G a).ncard * Nat.card ↥(MulAction.stabilizer G a)

The averaging identity (the engine; cf. Barbieri–Bhattacharjee–Manna–Nagy, arXiv:2508.20731, Lemma 15, there for A = B). For a finite group G acting on Ω and A B : Finset Ω: ∑ g : G, #((g • A) ∩ B) = ∑ a ∈ A, #(↑B ∩ orbit G a) * #(stabilizer G a).

Grouping the a ∈ A by orbit and dividing by #G = #O * #(stab), this is the usual form (1/#G) ∑ g #(gA ∩ B) = ∑_O #(A ∩ O) * #(B ∩ O) / #O over the orbits O meeting both A and B — stated multiplied out to stay in ℕ.

The dichotomy, orbit-local weak form

theorem TotD.separation_dichotomy {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] {A B : Finset Ω} (hA : A.Nonempty) (hB : B.Nonempty) (horb : ∀ a ∈ A, ∀ b ∈ B, b ∈ MulAction.orbit G a → A.card * B.card ≤ Nat.card ↑(MulAction.orbit G a)) : (∃ (g : G), g • A ∩ B = ∅) ∨ (∀ (g : G), (g • A ∩ B).card = 1) ∧ ∃ (x : Ω), ↑A ⊆ MulAction.orbit G x ∧ ↑B ⊆ MulAction.orbit G x ∧ Nat.card ↑(MulAction.orbit G x) = A.card * B.card

The separation dichotomy, orbit-local weak form. Let a finite group G act on Ω, and let A B : Finset Ω be nonempty. Suppose every orbit meeting BOTH A and B has size at least #A * #B. Then either

• some g : G separates: (g • A) ∩ B = ∅; or
• the pair is extremal: #((g • A) ∩ B) = 1 for EVERY g, and A and B lie in one single common orbit of size exactly #A * #B.

The transitive case (Ω a single orbit of size #A * #B) is known — it is the definition of a separating group in Araújo–Cameron–Steinberg 2017 §5.2, and the λ = 1 case of Cameron's Theorem 8. The orbit-local form proved here assumes nothing outside the common orbits: failure of separation forces A ∪ B into one common orbit and pins its size. BBMN (Bull. Austral. Math. Soc. 14 (1976) 7–10, Thm 2) is the strict-inequality corollary separation_of_forall_lt below.

Proof: averaging. If no g separates, ∑ g #((g • A) ∩ B) ≥ #G; the engine plus #(orbit) ≥ #A * #B on common orbits bounds the same sum by #G from above; equality analysis of the sandwich gives everything.

theorem TotD.separation_of_forall_lt {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] {A B : Finset Ω} (hA : A.Nonempty) (hB : B.Nonempty) (horb : ∀ a ∈ A, ∀ b ∈ B, b ∈ MulAction.orbit G a → A.card * B.card < Nat.card ↑(MulAction.orbit G a)) : ∃ (g : G), g • A ∩ B = ∅

Orbit-local BBMN (Bull. Austral. Math. Soc. 14 (1976) 7–10, Theorem 2, sharpened to an orbit-local hypothesis): if every orbit meeting both A and B has size STRICTLY greater than #A * #B, then some g separates. The strict hypothesis kills the extremal branch of separation_dichotomy.

Extremal = exact factorization (the regular action)

theorem TotD.card_smul_inter_regular {G : Type u_3} [Group G] [DecidableEq G] (g : G) (A B : Finset G) : (g • A ∩ B).card = {p ∈ A ×ˢ B | p.2 * p.1⁻¹ = g}.card

For the left-regular action of G on itself, (g • A) ∩ B is in bijection with the pairs (a, b) ∈ A × B such that b * a⁻¹ = g (send b to (g⁻¹ * b, b)).

theorem TotD.card_vadd_inter_regular {G : Type u_3} [AddGroup G] [DecidableEq G] (g : G) (A B : Finset G) : ((g +ᵥ A) ∩ B).card = {p ∈ A ×ˢ B | p.2 + -p.1 = g}.card

For the regular action of an additive group G on itself, (g +ᵥ A) ∩ B is in bijection with the pairs (a, b) ∈ A × B such that b + -a = g.

theorem TotD.forall_card_smul_inter_eq_one_iff_factorization {G : Type u_3} [Group G] [DecidableEq G] (A B : Finset G) : (∀ (g : G), (g • A ∩ B).card = 1) ↔ ∀ (g : G), ∃! p : G × G, p ∈ A ×ˢ B ∧ p.2 * p.1⁻¹ = g

Extremal = exact factorization (regular action; cf. Araújo–Cameron–Steinberg 2017 §6.4 for the loop-transversal view, and Barbieri et al. arXiv:2508.20731 for the diagonal A = B case): for G acting on itself by left multiplication and A B : Finset G, every translate of A meets B exactly once iff every g : G has a UNIQUE expression g = b * a⁻¹ with (a, b) ∈ A × B — an exact factorization G = B · A⁻¹. These are precisely the extremal non-separating pairs of separation_dichotomy on the regular action (all orbits have size #G = #A * #B).

theorem TotD.forall_card_vadd_inter_eq_one_iff_factorization {G : Type u_3} [AddGroup G] [DecidableEq G] (A B : Finset G) : (∀ (g : G), ((g +ᵥ A) ∩ B).card = 1) ↔ ∀ (g : G), ∃! p : G × G, p ∈ A ×ˢ B ∧ p.2 + -p.1 = g

Extremal = exact factorization, additive version: every translate of A meets B exactly once iff every g : G has a unique expression g = b + -a with (a, b) ∈ A × B.

The ℤ/n bridge: extremal pairs are rhythmic canons

theorem TotD.forall_card_vadd_inter_eq_one_iff_tiling {n : ℕ} (A B : Finset (ZMod n)) : (∀ (g : ZMod n), ((g +ᵥ A) ∩ B).card = 1) ↔ ∀ (x : ZMod n), ∃! p : ZMod n × ZMod n, p ∈ A ×ˢ B ∧ p.2 - p.1 = x

Extremal pairs over ℤ/n are exactly the rhythmic canons. For A B : Finset (ZMod n), every translate of A meets B in exactly one point iff the difference map A × B → ZMod n, (a, b) ↦ b - a, is a bijection — i.e. B ⊕ (-A) = ℤ/n is a tiling of ℤ/n by translates. This is the rhythmic-canon condition of Coven–Meyerowitz ("Tiling the integers with translates of one finite set") and Vuza (for the aperiodic ones): the extremal non-separating pairs of the separation dichotomy over ℤ/n ARE rhythmic canons.

Sanity witnesses on ℤ/12 (decide)

theorem TotD.tiling_witness_zmod12 (g : ZMod 12) : ((g +ᵥ {0, 3, 6, 9}) ∩ {0, 1, 2}).card = 1

The diminished-seventh rhythm {0,3,6,9} against the chromatic cell {0,1,2} in ℤ/12: #A * #B = 12 = #(ℤ/12), and every translate meets in exactly one point — the extremal branch of the dichotomy; by forall_card_vadd_inter_eq_one_iff_tiling, a rhythmic canon.

theorem TotD.separating_witness_zmod12 : ∃ (g : ZMod 12), (g +ᵥ {0, 1, 2, 3}) ∩ {0, 1, 2} = ∅

The chromatic cell {0,1,2,3} against {0,1,2} in ℤ/12: again #A * #B = 12 = #(ℤ/12), but this pair is NOT a tiling — and indeed it separates (the other branch of the dichotomy).