Tail three-family combinatorial assembly

Proved

Erdos390.tail_three_family_assembly

by doctosil · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

asymptoticscombinatoricsnumber-theory

Let $n, h, D \in \mathbb{N}$ and let $\mathrm{central}, \mathrm{fixed}, \mathrm{bank}, \mathrm{candidates}$ be finite subsets of $\mathbb{N}$ . Suppose $\mathrm{central} \subseteq (n, 2n]$ and $\mathrm{fixed}, \mathrm{bank}, \mathrm{candidates} \subseteq (2n, 2n + h]$ are pairwise disjoint subsets satisfying:

\left(\prod_{a \in \mathrm{fixed}} a\right) \cdot \left(\prod_{b \in \mathrm{bank}} b\right) \cdot \left(\prod_{c \in \mathrm{candidates}} c\right) \cdot D = \prod_{k \in (2n, 2n + h]} k.

Then:

Each tail subset is contained in $(n, 2n + h]$ ;
Each tail subset is disjoint from $\mathrm{central}$ ;
The mutual pairwise disjointness and product identity are preserved.

Preamble

import Mathlib
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem tail_three_family_assembly
    {n h D : ℕ} {central fixed bank candidates : Finset ℕ}
    (hcentral : central ⊆ factorInterval n (2 * n))
    (hfixed : fixed ⊆ factorInterval (2 * n) (2 * n + h))
    (hbank : bank ⊆ factorInterval (2 * n) (2 * n + h))
    (hcand : candidates ⊆ factorInterval (2 * n) (2 * n + h))
    (hdisj_fb : Disjoint fixed bank)
    (hdisj_fc : Disjoint fixed candidates)
    (hdisj_bc : Disjoint bank candidates)
    (hprod : fixed.prod id * bank.prod id * candidates.prod id * D =
      (factorInterval (2 * n) (2 * n + h)).prod id) :
    fixed ⊆ factorInterval n (2 * n + h) ∧
    bank ⊆ factorInterval n (2 * n + h) ∧
    candidates ⊆ factorInterval n (2 * n + h) ∧
    Disjoint central fixed ∧
    Disjoint central bank ∧
    Disjoint central candidates ∧
    Disjoint fixed bank ∧
    Disjoint fixed candidates ∧
    Disjoint bank candidates ∧
    fixed.prod id * bank.prod id * candidates.prod id * D =
      (factorInterval (2 * n) (2 * n + h)).prod id := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Erdős Problem 390 tail three-family assembly

View graph