Disjoint collision blocks for commutative-monoid labels (Erdős 624)

Proved

Erdos624.collision_blocks

by Ethan Cheung · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problems

Let $U$ be a finite set, $M$ a finite commutative monoid and $v:U\to M$ arbitrary.

Theorem. Let $t,d\ge0$ with

|M|<\binom{|U|-2t(d-1)}{t}.

Then there are pairwise disjoint sets $B_1,\dots,B_d\subseteq U$ with $|B_j|\le 2t$ , and distinct subsets $P_j,Q_j\subseteq B_j$ with $\prod_{x\in P_j}v(x)=\prod_{x\in Q_j}v(x)$ for every $j$ .

This is the finite collision-block lemma (7)–(8) used to show that commutative-aggregate maps through a monoid of polynomial size cannot be one half of a covering pair in Erdős Problem 624.

Formalization Note. Blocks indexed by $\mathrm{Fin}\,d$ ; $U$ and $M$ arbitrary finite types.

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem collision_blocks {U : Type*} [Fintype U] [DecidableEq U] {M : Type*} [CommMonoid M] [Fintype M]
    (t d : ℕ) (v : U → M)
    (h7 : Fintype.card M < (Fintype.card U - 2 * t * (d - 1)).choose t) :
    ∃ Bk P Q : Fin d → Finset U, (∀ i j, i ≠ j → Disjoint (Bk i) (Bk j)) ∧
      ∀ i, #(Bk i) ≤ 2 * t ∧ P i ⊆ Bk i ∧ Q i ⊆ Bk i ∧ P i ≠ Q i ∧
        ∏ x ∈ P i, v x = ∏ x ∈ Q i, v x := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); (7)–(8) of the analysis derived from GPT 6.1 Sol's analysis (sixth report, Oct 2026), relayed by Ethan Cheung; Lean-verified by Grok Bot for Ethan Cheung (Oct 24 2026)

View graph