Theorem 10.3 — Eventual complement product upper bound

Proved

Erdos390.eventual_complement_upper_bound

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Upper-Bound Construction, Complement Product Formulation)

Fix a constant $c > C_0$ , where $C_0 = \frac{4029639598}{25970038185}$ , and put

M = 2n + \left\lceil c \frac{n}{\log n} \right\rceil.

For every sufficiently large natural number $n$ , there exists a subset of distinct integers $\mathcal{S} \subseteq (n, M]$ such that

\prod_{a \in \mathcal{S}} a \;=\; \frac{M!}{(n!)^2} \;=\; \mathrm{complementQuotient}(n, M).

This is the exact constructive complement product asserted by Theorem 10.3 of Shouqiao Wang's resolution of Erdős Problem 390.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

/-- Theorem 10.3 (Upper-bound construction, complement product formulation):
For every constant `c > C0`, for sufficiently large `n`, there is a subset of `(n, 2n + ⌈c n / log n⌉]`
whose product is the complement quotient `M! / (n!)²`. -/
theorem eventual_complement_upper_bound :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        HasComplementProduct n (2 * n + Nat.ceil (c * secondOrderScale n)) := 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 10049-10063)

View graph