Theorem 10.3 — Guarded central and residual split of complement product

Open

Erdos390.eventual_guarded_central_residual_split

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Guarded Central Anchor and Residual Decomposition)

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 a positive integer divisor $D \in \mathbb{N}$ , a central anchor factor subset $\mathrm{central} \subseteq (n, 2n + h]$ , and a residual factor subset $\mathrm{residual} \subseteq (n, 2n + h]$ satisfying:

Disjointness: $\mathrm{central} \cap \mathrm{residual} = \emptyset$ .
Central anchor product:

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

Residual tail product:

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

Consequently, their disjoint union $\mathcal{S} = \mathrm{central} \cup \mathrm{residual} \subseteq (n, 2n + h]$ satisfies:

\left(\prod_{a \in \mathcal{S}} a\right) (n!)^2 = \binom{2n}{n} (n!)^2 \cdot \left(\prod_{a \in \mathrm{residual}} a \cdot D\right) = (2n)! \prod_{a \in (2n, 2n + h]} a = (2n + h)!,

recovering the exact complement representation $\prod_{\mathcal{S}} a = \mathrm{complementQuotient}(n, 2n + h)$ .

This isolates the constructive core of Section 10 (Wang's GuardedUpperProductAssembly.lean, equations (10.27)-(10.28)) without restricting residual bank states to strictly exceed $2n$ .

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

/-- Theorem 10.3 (Guarded central anchor and residual decomposition):
For every constant `c > C0`, for sufficiently large `n`, there exists an auxiliary
divisor `D`, a central subset of `(n, 2n + ⌈c n / log n⌉]`, and a disjoint residual subset of
`(n, 2n + ⌈c n / log n⌉]` such that the central subset has product `binom(2n, n) * D`
and the residual subset has product times `D` equal to the full upper tail product. -/
theorem eventual_guarded_central_residual_split :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        ∃ (D : ℕ) (central residual : Finset ℕ),
          central ⊆ factorInterval n (2 * n + Nat.ceil (c * secondOrderScale n)) ∧
          residual ⊆ factorInterval n (2 * n + Nat.ceil (c * secondOrderScale n)) ∧
          Disjoint central residual ∧
          central.prod id = Nat.choose (2 * n) n * D ∧
          residual.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, GuardedUpperProductAssembly.lean (GitHub 61325b1)

View graph