Theorem 10.3 — Asymptotic nonnegativity of the second order scale

Proved

Erdos390.eventual_secondOrderScale_nonneg

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

asymptoticscombinatoricserdos-problemsnumber-theory

Theorem 10.3 (Asymptotic Nonnegativity of the Second Order Scale)

For all sufficiently large $n \in \mathbb{N}$ , the second order asymptotic scale $\mathrm{scale}(n) = \frac{n}{\log n}$ is non-negative:

0 \le \frac{n}{\log n}.

Indeed, for all $n \ge 2$ , $n > 1$ ensures $\log n > 0$ , while $n \ge 0$ , so the ratio is strictly non-negative.

This ensures all scale-normalized density envelope inequalities hold with preserved orientation in Erdős Problem 390.

Preamble

import Definitions.Def_erdos390_problem
open Filter

Formal statement

namespace Erdos390

open Filter

/-- The second-order scale `secondOrderScale n = n / log n` is eventually non-negative for large `n`. -/
theorem eventual_secondOrderScale_nonneg :
    ∀ᶠ n : ℕ in atTop, 0 ≤ secondOrderScale n := by sorry

end Erdos390

Source

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

View graph