Theorem 10.3 — Central anchor and tail quotient decomposition

Open

Erdos390.eventual_central_tail_split

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Central Anchor and Tail Quotient 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 factor subset $\mathcal{H}' \subseteq (n, 2n]$ , and a residual tail factor subset $\mathcal{G}_{\mathrm{res}} \subseteq (2n, 2n + h]$ satisfying the exact product identities:

\prod_{a \in \mathcal{H}'} a = \binom{2n}{n} \cdot D

and

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

This isolates the constructive core of Theorem 10.3 (equations (10.27)-(10.28) of Shouqiao Wang's paper) from the finite set union algebra and rational quotient cancellation.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

/-- Theorem 10.3 (Central anchor and tail quotient decomposition):
For every constant `c > C0`, for sufficiently large `n`, there exists an auxiliary
divisor `D` of the upper tail, a central subset of `(n, 2n]` whose product is `binom(2n, n) * D`,
and a residual tail subset of `(2n, 2n + ⌈c n / log n⌉]` whose product times `D` is the
full tail product. -/
theorem eventual_central_tail_split :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        ∃ (D : ℕ) (central tail : Finset ℕ),
          central ⊆ factorInterval n (2 * n) ∧
          tail ⊆ factorInterval (2 * n) (2 * n + Nat.ceil (c * secondOrderScale n)) ∧
          central.prod id = Nat.choose (2 * n) n * D ∧
          tail.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, Theorem 10.3 (arXiv / GitHub 61325b1, paper.tex lines 10100-10145)

View graph