Theorem 10.3 — Floating partition assembly into three-family product

Proved

Erdos390.floating_partition_assembly

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Floating Partition Assembly)

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 natural numbers. Suppose:

$\mathrm{fixed}, \mathrm{bank}, \mathrm{candidates} \subseteq (n, M]$ ,
$\mathrm{central}$ is disjoint from $\mathrm{fixed}, \mathrm{bank}, \mathrm{candidates}$ ,
$\mathrm{fixed}$ is disjoint from $\mathrm{bank}$ and $\mathrm{candidates}$ ,
$\mathrm{bank}$ and $\mathrm{candidates}$ are disjoint,
Product condition: $\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 there exists a floating subset $\mathrm{floating} = \mathrm{bank} \cup \mathrm{candidates} \subseteq (n, M]$ such that $\mathrm{floating}$ is disjoint from $\mathrm{central}$ and $\mathrm{fixed}$ , and:

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

This isolates the assembly of the dynamic floating block from its bank adjustment and candidate rounding constituents in Shouqiao Wang's BankPaperGuardedUpperProductAssembly.lean.

Preamble

import Mathlib
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

/-- Theorem 10.3 (Floating partition assembly):
Given subsets `fixed`, `bank`, and `candidates` of `(n, M]` satisfying central and pairwise disjointness,
the union `floating = bank ∪ candidates` satisfies `floating ⊆ (n, M]`, disjointness from `central` and `fixed`,
and exact product equivalence `fixed.prod * floating.prod * D = P`. -/
theorem floating_partition_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_fc : Disjoint fixed candidates)
    (hdisj_bc : Disjoint bank candidates)
    (hprod : fixed.prod id * bank.prod id * candidates.prod id * D = P) :
    ∃ floating : Finset ℕ,
      fixed ⊆ factorInterval n M ∧
      floating ⊆ factorInterval n M ∧
      Disjoint central fixed ∧
      Disjoint central floating ∧
      Disjoint fixed floating ∧
      bank ∪ candidates = floating ∧
      Disjoint bank candidates ∧
      fixed.prod id * floating.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