Prove2Me

Dense-pool circuit packing (small-m): m4≤2120a28n3m^4\le 2^{120}a^{28}n^3 (Erdős 624 Round 9)

Proved
Erdos624.dense_pool_pack_small_m

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

combinatoricserdos-problems

Let UU be finite with ∣U∣=n≥1|U|=n\ge 1, colour capacity r=2r=2, and let MM be a set of mm colours each equipped with a pool Vu⊆UV_u\subseteq U satisfying a∣Vu∣≥na|V_u|\ge n (a≥1a\ge 1) and a labelling vu:Vu→F2k−1v_u:V_u\to\mathbb F_2^{k-1} such that every circuit of size at most eight in the pool is assigned colour uu. If

m≤230a7,m\le 2^{30}a^{7},

then

m4≤2120a28n3.m^4\le 2^{120}a^{28}n^3.

This is the small-mm branch of Sol's dense-pool packing (Round 9). Constants loosened to 21202^{120}. It does not settle Erdős Problem 624 / PAIR / Step 17; the large-mm weight/Λ case is not included.

Preamble
import Mathlib
open Finset BigOperators
Formal statement
namespace Erdos624

/-- Dense-pool circuit packing, small-m branch (Sol Round 9).
If `#M ≤ 2^{30} a^7` with dense pools and short-circuit compatibility,
then `m^4 ≤ 2^{120} a^{28} n^3`. Does not settle PAIR / #624. -/
theorem dense_pool_pack_small_m
    {U C : Type*} [Fintype U] [DecidableEq U] [DecidableEq C]
    {k : ℕ} (L : Finset U → Finset C) (hLcap : ∀ A, #(L A) ≤ 2)
    (M : Finset C) (pool : C → Finset U)
    (lab : C → U → (Fin (k - 1) → ZMod 2)) (a : ℕ)
    (ha : 1 ≤ a)
    (hPool : ∀ u ∈ M, a * #(pool u) ≥ Fintype.card U)
    (hCompat : ∀ u ∈ M,
      ∀ A : Finset U, A ⊆ pool u →
        (A.Nonempty ∧ (∑ x ∈ A, lab u x) = 0 ∧
          ∀ ⦃S : Finset U⦄, S ⊆ A → S.Nonempty → S ≠ A →
            ∑ x ∈ S, lab u x ≠ 0) →
        #A ≤ 8 → u ∈ L A)
    (hn : 1 ≤ Fintype.card U)
    (hm : #M ≤ 2 ^ 30 * a ^ 7) :
    (#M) ^ 4 ≤ 2 ^ 120 * a ^ 28 * (Fintype.card U) ^ 3 := by sorry

end Erdos624
Source
Erdős Problem 624 (https://www.erdosproblems.com/624); dense-pool circuit packing small-m branch derived from GPT 6.1 Sol's analysis, relayed by Ethan Cheung; Lean by Grok Bot for Ethan Cheung (Oct 24 2026). Honest: only the small-m branch (#M ≤ 2^{30} a^7); large-m weight/Λ case not included. Does NOT settle PAIR / #624.

View graph