Theorem 10.3 — Eventual floating partition residual existence

Open

Erdos390.eventual_floating_partition_residual_exists

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Eventual Floating Partition Residual Existence)

Fix a constant $c > C_0 = \frac{4029639598}{25970038185}$ , and put $h = \left\lceil c \frac{n}{\log n} \right\rceil$ .

For all sufficiently large $n \in \mathbb{N}$ , given any divisor $D \in \mathbb{N}$ and central subset $\mathrm{central} \subseteq (n, 2n]$ such that $\prod_{\mathrm{central}} a = \binom{2n}{n} \cdot D$ and $D \mid \prod_{(2n, 2n+h]} a$ , there exist finite subsets $\mathrm{fixed}, \mathrm{floating}, \mathrm{bank}, \mathrm{candidates} \subseteq (n, 2n + h]$ such that:

$\mathrm{fixed}$ and $\mathrm{floating}$ are mutually disjoint and disjoint from $\mathrm{central}$ ,
$\mathrm{floating}$ is partitioned into two disjoint subsets: $\mathrm{bank} \cup \mathrm{candidates} = \mathrm{floating}$ with $\mathrm{bank} \cap \mathrm{candidates} = \emptyset$ ,
Product exactification:

\left(\prod_{a \in \mathrm{fixed}} a\right) \cdot \left(\prod_{a \in \mathrm{floating}} a\right) \cdot D = \prod_{a \in (2n, 2n + h]} a.

This isolates the continuous exactification partition of the smooth tail in Shouqiao Wang's BankPaperGuardedUpperProductAssembly.lean.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

/-- Theorem 10.3 (Eventual floating partition residual existence):
For every constant `c > C0`, for sufficiently large `n`, given any central anchor divisor `D`
and subset `central ⊆ (n, 2n]` whose product is `binom(2n, n) * D` with `D ∣ tailProduct`,
there exist disjoint sets `fixed, floating ⊆ (n, 2n + ⌈c n / log n⌉]` each disjoint from `central`,
and a disjoint partition `floating = bank ∪ candidates`, such that `fixed.prod * floating.prod * D = tailProduct`. -/
theorem eventual_floating_partition_residual_exists :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        ∀ (D : ℕ) (central : Finset ℕ),
          central ⊆ factorInterval n (2 * n) →
          central.prod id = Nat.choose (2 * n) n * D →
          D ∣ (factorInterval (2 * n) (2 * n + Nat.ceil (c * secondOrderScale n))).prod id →
          ∃ (fixed floating bank candidates : Finset ℕ),
            fixed ⊆ factorInterval n (2 * n + Nat.ceil (c * secondOrderScale n)) ∧
            floating ⊆ factorInterval n (2 * n + Nat.ceil (c * secondOrderScale n)) ∧
            Disjoint central fixed ∧
            Disjoint central floating ∧
            Disjoint fixed floating ∧
            bank ∪ candidates = floating ∧
            Disjoint bank candidates ∧
            fixed.prod id * floating.prod id * D =
              (factorInterval (2 * n) (2 * n + Nat.ceil (c * secondOrderScale n))).prod id := by sorry

end Erdos390

Source

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

View graph