Eventual existence of range sublist factoring order-4 deficit

Open

Erdos390.eventual_tail_divisor_order4_range_sublist_exists

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

asymptoticscombinatoricsnumber-theory

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}$ , given any divisor $D \in \mathbb{N}$ with $D \ne 1$ that does not belong to the range list $L = \mathrm{List.range'} (2n + 1) h$ and cannot be factored as a product of two or three elements of $L$ , and central subset $\mathrm{central} \subseteq (n, 2n]$ such that $\prod \mathrm{central} = \binom{2n}{n} D$ and $D \mid \prod_{(2n, 2n + h]} k$ , there exists a sublist $l \prec L$ whose product equals $D$ .

Preamble

import Mathlib.Data.List.Range
import Definitions.Def_erdos390_problem
open Filter
open Erdos390

Formal statement

namespace Erdos390

theorem eventual_tail_divisor_order4_range_sublist_exists :
    ∀ 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 →
          D ≠ 1 →
          D ∉ List.range' (2 * n + 1) (Nat.ceil (c * secondOrderScale n)) →
          (¬ ∃ a b : ℕ, a ∈ List.range' (2 * n + 1) (Nat.ceil (c * secondOrderScale n)) ∧
                        b ∈ List.range' (2 * n + 1) (Nat.ceil (c * secondOrderScale n)) ∧
                        a < b ∧ a * b = D) →
          (¬ ∃ a b c' : ℕ, a ∈ List.range' (2 * n + 1) (Nat.ceil (c * secondOrderScale n)) ∧
                          b ∈ List.range' (2 * n + 1) (Nat.ceil (c * secondOrderScale n)) ∧
                          c' ∈ List.range' (2 * n + 1) (Nat.ceil (c * secondOrderScale n)) ∧
                          a < b ∧ b < c' ∧ a * b * c' = D) →
          ∃ l : List ℕ,
            l.Sublist (List.range' (2 * n + 1) (Nat.ceil (c * secondOrderScale n))) ∧
            l.prod = D := by sorry

end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdős Problem 390, Section 10, BankPaperGuardedUpperProductAssembly.lean

View graph