Theorem 10.3 — Three-family disjoint product assembly from floating partition

Proved

Erdos390.three_family_partition_assembly

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Three-Family Disjoint Product Assembly from Floating Partition)

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

$\mathrm{fixed} \subseteq (n, M]$ and $\mathrm{floating} \subseteq (n, M]$ ,
$\mathrm{central} \cap \mathrm{fixed} = \emptyset$ and $\mathrm{central} \cap \mathrm{floating} = \emptyset$ ,
$\mathrm{fixed} \cap \mathrm{floating} = \emptyset$ ,
$\mathrm{floating}$ is partitioned into two disjoint sets: $\mathrm{bank} \cup \mathrm{candidates} = \mathrm{floating}$ with $\mathrm{bank} \cap \mathrm{candidates} = \emptyset$ ,
Product condition: $\left(\prod_{a \in \mathrm{fixed}} a\right) \cdot \left(\prod_{a \in \mathrm{floating}} a\right) \cdot D = P$ .

Then the three families $\mathrm{fixed}, \mathrm{bank}, \mathrm{candidates} \subseteq (n, M]$ are mutually disjoint, each disjoint from $\mathrm{central}$ , and satisfy:

\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.

This isolates the combinatorial splitting of the dynamic exactification block into the bank adjustment and candidate rounding sets in Shouqiao Wang's BankPaperGuardedUpperProductAssembly.lean.

Preamble

import Mathlib
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

/-- Theorem 10.3 (Three-family assembly from floating partition):
Given a fixed subset and a floating subset of `(n, M]` disjoint from each other and from `central`,
and a disjoint partition `floating = bank ∪ candidates`, if `fixed.prod * floating.prod * D = P`,
then `fixed`, `bank`, and `candidates` satisfy all mutual disjointness, subset, and product conditions. -/
theorem three_family_partition_assembly
    {n M D P : ℕ} {central fixed floating bank candidates : Finset ℕ}
    (hfixed_sub : fixed ⊆ factorInterval n M)
    (hfloat_sub : floating ⊆ factorInterval n M)
    (hdisj_cf : Disjoint central fixed)
    (hdisj_cfloat : Disjoint central floating)
    (hdisj_ffloat : Disjoint fixed floating)
    (hpart : bank ∪ candidates = floating)
    (hdisj_bc : Disjoint bank candidates)
    (hprod : fixed.prod id * floating.prod id * D = P) :
    fixed ⊆ factorInterval n M ∧
    bank ⊆ factorInterval n M ∧
    candidates ⊆ factorInterval n M ∧
    Disjoint central fixed ∧
    Disjoint central bank ∧
    Disjoint central candidates ∧
    Disjoint fixed bank ∧
    Disjoint (fixed ∪ bank) candidates ∧
    fixed.prod id * bank.prod id * candidates.prod id * D = P := by sorry

end Erdos390

Source

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

View graph