Dense-pool intersection lemma: $b\,q!\,\#\mathrm{good}\ge g^q$ (Erdős 624 auxiliary)

Open

Erdos624.dense_pool_intersection

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

combinatoricserdos-problems

Let $U$ be a finite set with $|U|=n\ge 1$ , and let $G$ be a finite colour set of size $g$ . Suppose each colour $u\in G$ has a pool $V_u\subseteq U$ satisfying $a|V_u|\ge n$ for some $a\ge 1$ . For $q\ge 1$ and $g\ge 2a(q-1)$ , writing $b=2^{q+1}a^q$ , the number $h$ of $q$ -subsets $S\subseteq G$ with $b\bigl|\bigcap_{u\in S}V_u\bigr|\ge n$ satisfies $b\cdot q!\cdot h\ge g^q$ .

Context: Erdős Problem 624 asks whether $H(n)-\log_2 n\to\infty$ . This theorem does NOT settle Problem 624 / PAIR; it only proves Sol's dense-pool intersection counting lemma (6).

Formalization Note. Pure Mathlib: bOf a q = 2^(q+1)*a^q, poolInter/goodTuples as Finset filters; no dependence on a separate Erdős 624 definitions module.

Preamble

import Mathlib
open Finset

Formal statement

namespace Erdos624

/-- `b = 2^{q+1} a^q`. -/
def bOf (a q : ℕ) : ℕ := 2 ^ (q + 1) * a ^ q

/-- Intersection of pools over `S` (empty → `univ`). -/
def poolInter {U C : Type*} [Fintype U] [DecidableEq U]
    (V : C → Finset U) (S : Finset C) : Finset U :=
  if h : S.Nonempty then S.inf' h V else univ

/-- Good q-tuples: those with `b · |∩ pools| ≥ n`. -/
def goodTuples {U C : Type*} [Fintype U] [DecidableEq U] [DecidableEq C]
    (G : Finset C) (V : C → Finset U) (a q : ℕ) : Finset (Finset C) :=
  let n := Fintype.card U
  let b := bOf a q
  {S ∈ G.powersetCard q | b * #(poolInter V S) ≥ n}

/-- Dense-pool intersection lemma (Sol (6)), multiplication-cleared.
Pools of density ≥1/a; for `g ≥ 2a(q−1)` and `n≥1`,
`b · q! · #good ≥ g^q` with `b = 2^{q+1} a^q`.
Does **not** settle PAIR / #624. -/
theorem dense_pool_intersection
    {U C : Type*} [Fintype U] [DecidableEq U] [DecidableEq C]
    (G : Finset C) (V : C → Finset U) (a q : ℕ)
    (ha : 1 ≤ a) (hq : 1 ≤ q) (hn : 1 ≤ Fintype.card U)
    (hPool : ∀ u ∈ G, a * #(V u) ≥ Fintype.card U)
    (hg : 2 * a * (q - 1) ≤ #G) :
    bOf a q * q.factorial * #(goodTuples G V a q) ≥ (#G) ^ q := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); dense-pool intersection (Sol (6)) derived from GPT 6.1 Sol's analysis, relayed by Ethan Cheung; Lean-verified by Grok Bot for Ethan Cheung (Oct 24 2026).

View graph

Dense-pool intersection lemma: b q! #good≥gqb\,q!\,\#\mathrm{good}\ge g^qbq!#good≥gq (Erdős 624 auxiliary)

Dense-pool intersection lemma: $b\,q!\,\#\mathrm{good}\ge g^q$ (Erdős 624 auxiliary)