Theorem 10.3 — Existence of bounded central anchor with upper tail reserve

Proved

Erdos390.eventual_bounded_central_anchor_exists

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Existence of Bounded Central Anchor with Tail Reserve)

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

For all sufficiently large $n \in \mathbb{N}$ , there exist a prime bound $B \in \mathbb{N}$ , a positive integer divisor $D > 0$ , and a central factor subset $\mathrm{central} \subseteq (n, 2n]$ such that:

The central product exactly factors the central binomial coefficient and $D$ :

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

The prime support of $D$ is bounded by $B$ :

\forall \ell \in \mathbb{P},\quad \ell \mid D \implies \ell \le B.

At every prime $\ell \le B$ , the $\ell$ -adic valuation of $D$ is bounded by the valuation of the upper tail product:

v_\ell(D) \le v_\ell\left( \prod_{a \in (2n, 2n + h]} a \right).

This isolates the analytical construction of the three-family routed central anchor set (Shouqiao Wang's CentralAnchorExistence.lean), combining prefix allocation, promotion costs, and upper tail valuations.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

theorem eventual_bounded_central_anchor_exists :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        ∃ (B D : ℕ) (central : Finset ℕ),
          D ≠ 0 ∧
          central ⊆ factorInterval n (2 * n) ∧
          central.prod id = Nat.choose (2 * n) n * D ∧
          (∀ ℓ : ℕ, ℓ.Prime → ℓ ∣ D → ℓ ≤ B) ∧
          (∀ ℓ : ℕ, ℓ.Prime → ℓ ≤ B →
            D.factorization ℓ ≤ ((factorInterval (2 * n) (2 * n + Nat.ceil (c * secondOrderScale n))).prod id).factorization ℓ) := by sorry

end Erdos390

Source

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

View graph