Anchor and tail envelope conjunction assembly

Proved

Erdos390.anchor_tail_envelope_conjunction

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

asymptoticscombinatoricsnumber-theory

Let $B, D, n \in \mathbb{N}$ and $c \in \mathbb{R}$ . Let $c_{\mathrm{anchor}}, c_{\mathrm{tail}} : \mathbb{N} \to \mathbb{R}$ be prime valuation coefficient functions. Suppose that for every prime $\ell \le B$ :

The prime factor valuation of $D$ is bounded by the anchor envelope:

v_\ell(D) \le c_{\mathrm{anchor}}(\ell) \cdot s(n),

where $s(n) = \frac{n}{\log n}$ . 2. The tail interval factor product $P_{\mathrm{tail}} = \prod_{k \in (2n, 2n + \lceil c s(n) \rceil]} k$ dominates the tail envelope:

c_{\mathrm{tail}}(\ell) \cdot s(n) \le v_\ell(P_{\mathrm{tail}}).

The coefficient envelope dominance holds:

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

Then for every prime $\ell \le B$ , the three bounds hold simultaneously as a conjunction:

(v_\ell(D) \le c_{\mathrm{anchor}}(\ell) \cdot s(n)) \wedge (c_{\mathrm{tail}}(\ell) \cdot s(n) \le v_\ell(P_{\mathrm{tail}})) \wedge (c_{\mathrm{anchor}}(\ell) \le c_{\mathrm{tail}}(\ell)).

Preamble

import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem anchor_tail_envelope_conjunction
    {B D : ℕ} {c : ℝ} {n : ℕ} {cAnchor cTail : ℕ → ℝ}
    (hanchor : ∀ ℓ : ℕ, ℓ.Prime → ℓ ≤ B → (D.factorization ℓ : ℝ) ≤ cAnchor ℓ * secondOrderScale n)
    (htail : ∀ ℓ : ℕ, ℓ.Prime → ℓ ≤ B → cTail ℓ * secondOrderScale n ≤ (((factorInterval (2 * n) (2 * n + Nat.ceil (c * secondOrderScale n))).prod id).factorization ℓ : ℝ))
    (horder : ∀ ℓ : ℕ, ℓ.Prime → ℓ ≤ B → cAnchor ℓ ≤ cTail ℓ) :
    ∀ ℓ : ℕ, ℓ.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

P. Erdős, Some problems in number theory, 1975; Erdős Problem 390 decomposition for envelope conjunction

View graph