Theorem 10.3 — Guarded four-family joint upper product assembly

Open

Erdos390.eventual_guarded_four_family_assembly

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Guarded Four-Family Joint Upper Product Assembly)

Fix a constant $c > C_0$ , where $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}$ , there exist an auxiliary positive integer divisor $D \in \mathbb{N}$ and four mutually disjoint finite sets of integers

\mathrm{central}, \mathrm{fixed}, \mathrm{bank}, \mathrm{candidates} \subseteq (n, 2n + h]

such that:

Central anchor containment and product: $\mathrm{central} \subseteq (n, 2n]$ and

\prod_{a \in \mathrm{central}} a = \binom{2n}{n} \cdot D.

Residual partition: $\mathrm{fixed}, \mathrm{bank}, \mathrm{candidates} \subseteq (n, 2n + h]$ are mutually disjoint and each is disjoint from $\mathrm{central}$ .
Joint tail product exactification:

\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 = \prod_{a \in (2n, 2n + h]} a.

This formalizes the complete four-family decomposition from Section 10 of Shouqiao Wang's paper (BankPaperGuardedUpperProductAssembly.lean). The divisor $D$ couples the central anchor balance with the exactification of the upper tail product through the union of fixed prime factors, signed bank states, and rounded candidate sets.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

/-- Theorem 10.3 (Four-family joint upper product assembly):
For every constant `c > C0`, for sufficiently large `n`, there exists an auxiliary divisor `D`
and four mutually disjoint subsets `central`, `fixed`, `bank`, `candidates` of `(n, 2n + ⌈c n / log n⌉]`
such that:
1. `central ⊆ (n, 2n]` with `central.prod id = Nat.choose (2 * n) n * D`
2. `fixed`, `bank`, `candidates ⊆ (n, 2n + ⌈c n / log n⌉]`
3. `fixed`, `bank`, `candidates` are mutually disjoint and disjoint from `central`
4. `fixed.prod id * bank.prod id * candidates.prod id * D = tailProduct`. -/
theorem eventual_guarded_four_family_assembly :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        ∃ (D : ℕ) (central fixed bank candidates : Finset ℕ),
          central ⊆ factorInterval n (2 * n) ∧
          fixed ⊆ factorInterval n (2 * n + Nat.ceil (c * secondOrderScale n)) ∧
          bank ⊆ factorInterval n (2 * n + Nat.ceil (c * secondOrderScale n)) ∧
          candidates ⊆ factorInterval n (2 * n + Nat.ceil (c * secondOrderScale n)) ∧
          Disjoint central fixed ∧
          Disjoint central bank ∧
          Disjoint central candidates ∧
          Disjoint fixed bank ∧
          Disjoint (fixed ∪ bank) candidates ∧
          central.prod id = Nat.choose (2 * n) n * D ∧
          fixed.prod id * bank.prod id * candidates.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 commit 61325b1)

View graph