Eventual existence of an admissible endpoint above $C_0$

Proved

Erdos390.eventual_admissible_upper_bound

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

asymptoticscombinatoricserdos-problemsnumber-theoryupper-bound

Let $I(n, M) = \{a \in \mathbb{N} : n < a \le M\}$ , and let

C_0 = \frac{4029639598}{25970038185}.

An integer $M$ is defined to be an admissible endpoint for $n$ if there exists a finite subset of factors $A \subseteq I(n, M)$ whose product equals $n!$ :

\prod_{a \in A} a = n!.

For every real constant $c > C_0$ , all sufficiently large natural numbers $n$ admit an admissible endpoint bounded by $2n + \lceil c \frac{n}{\log n} \rceil$ :

\forall c > C_0, \quad \forall^\infty n, \quad \operatorname{IsAdmissibleEndpoint}\left(n, 2n + \left\lceil c \frac{n}{\log n} \right\rceil\right).

This theorem isolates the core constructive existence theorem from Theorem 10.3 (Upper-bound construction) of Shouqiao Wang's proposed solution to Erdős Problem 390.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

/-- For every constant `c > C0`, for sufficiently large `n`, there exists an admissible
endpoint in `(n, 2n + ⌈c n / log n⌉]`. -/
theorem eventual_admissible_upper_bound :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        IsAdmissibleEndpoint n (2 * n + Nat.ceil (c * secondOrderScale n)) := by sorry

end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdős Problem 390, p. 103, Section 10, Theorem 10.3 (Upper-bound construction), https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex#L10062-L10179

View graph

Eventual existence of an admissible endpoint above C0C_0C0​

Eventual existence of an admissible endpoint above $C_0$