Eventual existence of separated anchor and tail envelopes

Proved

Erdos390.eventual_separated_anchor_tail_envelopes_exist

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

asymptoticscombinatoricsnumber-theory

For any parameter $c > C_0$ , there exists an asymptotic filter threshold such that for all sufficiently large $n$ , there exist:

A prime cutoff bound $B \in \mathbb{N}$ ,
A nonzero central anchor deficit $D \in \mathbb{N}_{> 0}$ ,
A central subset $\mathrm{central} \subseteq (n, 2n]$ such that $\prod \mathrm{central} = \binom{2n}{n} \cdot D$ ,
Prime envelope coefficient functions $c_{\mathrm{anchor}}, c_{\mathrm{tail}} : \mathbb{N} \to \mathbb{R}$ ,

such that:

Every prime dividing $D$ is bounded by $B$ : $\forall \ell \mid D, \ell \le B$ .
For all primes $\ell \le B$ , the anchor valuation is bounded by $c_{\mathrm{anchor}}(\ell) \cdot \frac{n}{\log n}$ .
For all primes $\ell \le B$ , the tail factor product valuation is bounded below by $c_{\mathrm{tail}}(\ell) \cdot \frac{n}{\log n}$ .
For all primes $\ell \le B$ , the envelope dominance condition $c_{\mathrm{anchor}}(\ell) \le c_{\mathrm{tail}}(\ell)$ holds.

Preamble

import Definitions.Def_erdos390_problem
open Filter
open Erdos390

Formal statement

namespace Erdos390

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

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Erdős Problem 390 reduction for separated anchor and tail envelopes

View graph