Theorem 10.3 — central anchor in (n,2n] with its exact residual (source-faithful)

Proved

Erdos390.eventual_central_anchor_and_residual_exists

by foos · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricserdos-problemsnumber-theory

Fix a real constant $c$ with $c > C_0 = \frac{4029639598}{25970038185}$ and write $h = \left\lceil c\,\frac{n}{\log n} \right\rceil$ for the tail length. For all sufficiently large $n$ , there exist a natural number $D$ , a finite set $\mathrm{central} \subseteq (n, 2n]$ , and a finite set $\mathrm{residual} \subseteq (n, 2n+h]$ , disjoint from $\mathrm{central}$ , such that

\prod_{a \in \mathrm{central}} a = \binom{2n}{n} \cdot D, \qquad \Bigl(\prod_{a \in \mathrm{residual}} a\Bigr) \cdot D = \prod_{k \in (2n,\, 2n+h]} k.

This is the source-faithful core of the paper's Theorem 10.3 upper-bound construction. The central binomial coefficient $\binom{2n}{n}$ is absorbed by a set of factors confined to the central interval $(n, 2n]$ , up to an auxiliary divisor $D$ (the anchor cofactor), and the residual set then realizes the tail product $\prod_{(2n, 2n+h]}$ divided by that same $D$ , using factors drawn from the full interval $(n, 2n+h]$ and disjoint from the anchor set. The disjoint union $\mathrm{central} \cup \mathrm{residual}$ is then a subset of $(n, 2n+h]$ with product $\binom{2n}{n} \cdot \prod_{(2n, 2n+h]} = (2n+h)!/(n!)^2$ , the complement quotient of Theorem 10.3.

Unlike a statement that quantifies universally over an arbitrary anchor pair $(D, \mathrm{central})$ , the residual here is bound to the same $D$ and $\mathrm{central}$ produced by the anchor construction, which is the form in which the paper's guarded assembly is proved.

Formalization Note No divisibility hypothesis is placed on $D$ : the identity $\prod_{\mathrm{residual}} \cdot D = \prod_{(2n, 2n+h]}$ itself implies $D \mid \prod_{(2n, 2n+h]}$ . The residual set may use factors of $(n, 2n]$ outside $\mathrm{central}$ , exactly as in the source assembly; in particular it is not confined to the tail interval $(2n, 2n+h]$ .

Preamble

import Definitions.Def_erdos390_problem

open Filter

Formal statement

namespace Erdos390

/-- **Theorem 10.3 (central anchor and residual, source-faithful binding).**
For every constant `c > C0`, for sufficiently large `n`, there is a divisor `D`,
a central anchor subset `central ⊆ (n, 2n]` whose product is `binom(2n, n) * D`,
and a residual subset of `(n, 2n + ⌈c n / log n⌉]`, disjoint from `central`,
whose product times `D` equals the full upper tail product on `(2n, 2n + ⌈c n / log n⌉]`. -/
theorem eventual_central_anchor_and_residual_exists :
    ∀ c : ℝ, C0 < c →
      ∀ᶠ n : ℕ in atTop,
        ∃ (D : ℕ) (central residual : Finset ℕ),
          central ⊆ factorInterval n (2 * n) ∧
          central.prod id = Nat.choose (2 * n) n * D ∧
          residual ⊆ factorInterval n (2 * n + Nat.ceil (c * secondOrderScale n)) ∧
          Disjoint central residual ∧
          residual.prod id * D =
            (factorInterval (2 * n) (2 * n + Nat.ceil (c * secondOrderScale n))).prod id := by sorry

end Erdos390

Source

Shouqiao Wang, A Proposed Solution to Erdős Problem 390, Section 10, Theorem 10.3 (thm:upper-bound-construction), eq. (final-residual-set) and (final-complement-subset): https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/paper.tex; Lean development: 390/lean/Erdos390/WholePaper/BankPaperGuardedUpperProductAssembly.lean (guardedComplementFactorSet_prod, isAdmissibleEndpoint_of_exactificationResidual), pinned snapshot https://github.com/ShouqiaoW/erdos/tree/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390

View graph