Theorem 10.3 — Eventual scaled central anchor and tail reserve existence

Proved

Erdos390.eventual_scaled_central_anchor_reserve_exists

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Eventual Scaled Central Anchor and Tail Reserve Existence)

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:

an upper prime bound $B \in \mathbb{N}$ ,
a positive integer divisor $D \in \mathbb{N}$ ( $D \neq 0$ ),
a central factor subset $\mathrm{central} \subseteq (n, 2n]$ such that $\prod_{\mathrm{central}} a = \binom{2n}{n} \cdot D$ ,
scale-normalized envelope functions $c_{\mathrm{anchor}}, c_{\mathrm{tail}} : \mathbb{N} \to \mathbb{R}$ ,

such that:

All prime factors of $D$ are bounded: $\forall \ell \in \mathbb{P},\ \ell \mid D \implies \ell \le B$ .
The second order scale is non-negative: $\mathrm{scale}(n) = \frac{n}{\log n} \ge 0$ .
For all primes $\ell \le B$ :

(v_\ell(D) : \mathbb{R}) \le c_{\mathrm{anchor}}(\ell) \cdot \mathrm{scale}(n)

c_{\mathrm{tail}}(\ell) \cdot \mathrm{scale}(n) \le (v_\ell(\prod_{(2n, 2n+h]} a) : \mathbb{R})

c_{\mathrm{anchor}}(\ell) \le c_{\mathrm{tail}}(\ell).

This isolates the continuous density balance and stationary prefix cofactor routing of Shouqiao Wang's CentralAnchorReserveAlgebra.lean.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

/-- Theorem 10.3 (Scaled central anchor and tail reserve):
For every constant `c > C0`, for sufficiently large `n`, there exists an anchor divisor `D`,
a central subset of `(n, 2n]` whose product is `binom(2n, n) * D`, an upper prime bound `B`,
and reserve coefficient envelopes `cAnchor, cTail : ℕ → ℝ` such that the scale `secondOrderScale n ≥ 0`,
and for all primes `ℓ ≤ B`, the p-adic valuations of `D` and the upper tail product satisfy
`(v_ℓ(D) : ℝ) ≤ cAnchor ℓ * scale ≤ cTail ℓ * scale ≤ (v_ℓ(tail) : ℝ)`. -/
theorem eventual_scaled_central_anchor_reserve_exists :
    ∀ 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) ∧
          0 ≤ secondOrderScale n ∧
          (∀ ℓ : ℕ, ℓ.Prime → ℓ ≤ B →
            (D.factorization ℓ : ℝ) ≤ cAnchor ℓ * secondOrderScale n ∧
            cTail ℓ * secondOrderScale n ≤ (((factorInterval (2 * n) (2 * n + Nat.ceil (c * secondOrderScale n))).prod id).factorization ℓ : ℝ) ∧
            cAnchor ℓ ≤ cTail ℓ) := by sorry

end Erdos390

Source

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

View graph