Three-family disjoint union assembly with product exactification

Proved

Erdos390.three_family_residual_union_assembly

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

algebracombinatoricserdos-problems

Three-Family Disjoint Union Assembly with Product Exactification

Let $n, M, D, P \in \mathbb{N}$ and let $\mathrm{central}, \mathrm{fixed}, \mathrm{bank}, \mathrm{candidates} \subseteq (n, M]$ be finite sets of integers.

Suppose that $\mathrm{fixed}, \mathrm{bank}, \mathrm{candidates}$ are mutually disjoint and each is disjoint from $\mathrm{central}$ :

\mathrm{Disjoint}\ \mathrm{central}\ \mathrm{fixed}, \quad \mathrm{Disjoint}\ \mathrm{central}\ \mathrm{bank}, \quad \mathrm{Disjoint}\ \mathrm{central}\ \mathrm{candidates},

\mathrm{Disjoint}\ \mathrm{fixed}\ \mathrm{bank}, \quad \mathrm{Disjoint}\ (\mathrm{fixed} \cup \mathrm{bank})\ \mathrm{candidates}.

Suppose furthermore that their joint product times $D$ equals $P$ :

\left( \prod_{a \in \mathrm{fixed}} a \right) \cdot \left( \prod_{a \in \mathrm{bank}} a \right) \cdot \left( \prod_{a \in \mathrm{candidates}} a \right) \cdot D = P.

Then the unified set $\mathrm{residual} = (\mathrm{fixed} \cup \mathrm{bank}) \cup \mathrm{candidates} \subseteq (n, M]$ is disjoint from $\mathrm{central}$ and satisfies:

\left( \prod_{a \in \mathrm{residual}} a \right) \cdot D = P.

This establishes the fundamental combinatorial union assembly theorem (Shouqiao Wang's GuardedExactificationProduct.lean and BankPaperGuardedUpperProductAssembly.lean), enabling the integration of fixed factors, signed bank states, and rounded candidate sets into a unified residual complement.

Preamble

import Mathlib
import Definitions.Def_erdos390_problem

Formal statement

namespace Erdos390

theorem three_family_residual_union_assembly
    {n M D P : ℕ} {central fixed bank candidates : Finset ℕ}
    (hfixed_sub : fixed ⊆ factorInterval n M)
    (hbank_sub : bank ⊆ factorInterval n M)
    (hcand_sub : candidates ⊆ factorInterval n M)
    (hdisj_cf : Disjoint central fixed)
    (hdisj_cb : Disjoint central bank)
    (hdisj_cc : Disjoint central candidates)
    (hdisj_fb : Disjoint fixed bank)
    (hdisj_fbc : Disjoint (fixed ∪ bank) candidates)
    (hprod : fixed.prod id * bank.prod id * candidates.prod id * D = P) :
    ∃ residual : Finset ℕ,
      residual ⊆ factorInterval n M ∧
      Disjoint central residual ∧
      residual.prod id * D = P := by sorry

end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdős Problem 390, Section 9, GuardedExactificationProduct.lean (GitHub 61325b1)

View graph