Theorem 10.3 — Central anchor existence and tail divisibility

Proved

Erdos390.eventual_central_anchor_certificate

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Central Anchor Existence and Tail Divisibility)

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}$ , there exist a positive integer divisor $D \in \mathbb{N}$ and a central factor subset $\mathrm{central} \subseteq (n, 2n]$ such that:

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

and $D$ divides the literal product of the upper tail:

D \mid \prod_{a \in (2n, 2n + h]} a.

This isolates the existence of the three-family routed central anchor set (Shouqiao Wang's CentralAnchorExistence.lean), ensuring that the promotion powers of two and large central cofactors divide the upper tail product.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

/-- Theorem 10.3 (Central anchor certificate):
For every constant `c > C0`, for sufficiently large `n`, there exists an auxiliary
divisor `D` and a central subset of `(n, 2n]` whose product is `binom(2n, n) * D`,
such that `D` divides the full upper tail product on `(2n, 2n + ⌈c n / log n⌉]`. -/
theorem eventual_central_anchor_certificate :
    ∀ 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 := by sorry

end Erdos390

Source

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

View graph