A block of consecutive integers of bounded $2$ -adic valuation is short

Proved

Erdos287.block_two_adic_length

by xbgxjack · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryp-adic

If every element of the block $m, m+1, \dots, m+t-1$ of consecutive positive integers has $2$ -adic valuation at most $c$ , then

t \le 2^{\,c+1} - 1 .

Any $2^{c+1}$ consecutive integers contain a multiple of $2^{c+1}$ , whose valuation exceeds $c$ .

Applied to Erdős problem #287 this makes the structure of a hypothetical counterexample quantitative: a run of even denominators whose halved block has maximal $2$ -adic valuation $c$ contains no multiple of $2^{c+1}$ , hence has at most $2^{c+1}-1$ terms and spans fewer than $2^{c+2}$ integers.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem block_two_adic_length (c m t : ℕ) (hm : 0 < m)
    (h : ∀ j, j < t → padicValNat 2 (m + j) ≤ c) :
    t ≤ 2 ^ (c + 1) - 1 := by sorry
end Erdos287

Source

Auxiliary results proved for the prove2.me mission on Erdos problem #287 (https://www.erdosproblems.com/287), for the attack on the residual core Erdos287.mixed_gap_core with exactly two runs of even denominators. Classical background: P. Erdos, 'Egy Kurschak-fele elemi szamelmeleti tetel altalanositasa', Mat. Fiz. Lapok 39 (1932), 17-24. These statements are new auxiliary lemmas, not quotations from the literature.

View graph

A block of consecutive integers of bounded 222-adic valuation is short

A block of consecutive integers of bounded $2$ -adic valuation is short