Theorem 10.3 — Valuation comparison via scale reserve bounds

Proved

Erdos390.valuation_le_of_scale_reserve

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Valuation Comparison via Scale Reserve Bounds)

Let $v_D, v_P \in \mathbb{N}$ and $c_{\mathrm{anchor}}, c_{\mathrm{tail}}, \mathrm{scale} \in \mathbb{R}$ . Suppose:

$\mathrm{scale} \ge 0$ ,
$v_D \le c_{\mathrm{anchor}} \cdot \mathrm{scale}$ ,
$c_{\mathrm{tail}} \cdot \mathrm{scale} \le v_P$ ,
$c_{\mathrm{anchor}} \le c_{\mathrm{tail}}$ .

Then $v_D \le v_P$ .

This directly transfers asymptotic density reserve inequalities into literal $p$ -adic valuation dominances for all bounded prime factors in Erdős Problem 390.

Preamble

import Mathlib

Formal statement

namespace Erdos390

/-- Given non-negative scale `scale ≥ 0`, upper bound `vD ≤ cAnchor * scale`, lower bound
`cTail * scale ≤ vP`, and coefficient order `cAnchor ≤ cTail`, we have `vD ≤ vP`. -/
theorem valuation_le_of_scale_reserve
    {vD vP : ℕ} {cAnchor cTail scale : ℝ}
    (hscale : 0 ≤ scale)
    (hD : (vD : ℝ) ≤ cAnchor * scale)
    (hP : cTail * scale ≤ (vP : ℝ))
    (hcoeff : cAnchor ≤ cTail) :
    vD ≤ vP := by sorry

end Erdos390

Source

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

View graph