Two even runs of different $2$ -adic weight cannot complete to $1$

Proved

Erdos287.even_blocks_distinct_norm

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

number-theoryp-adicunit-fractions

Consider two blocks of consecutive even integers,

2m_1,\ 2(m_1+1),\ \dots,\ 2(m_1+t_1-1) \qquad\text{and}\qquad 2m_2,\ 2(m_2+1),\ \dots,\ 2(m_2+t_2-1),

both nonempty, and write $B_1, B_2$ for their reciprocal sums. If $|B_1|_2 \ne |B_2|_2$ , then $B_1 + B_2 + O \ne 1$ for every sum $O$ of reciprocals of odd numbers.

Each block has $|B_i|_2 = 2^{\,c_i+1} > 1$ , where $c_i$ is the largest $2$ -adic valuation occurring in the halved block — a block of consecutive integers has a unique element of maximal $2$ -adic valuation (Kürschák), so no cancellation takes place inside a block. When the two norms differ the ultrametric equality $|B_1 + B_2|_2 = \max(|B_1|_2, |B_2|_2) > 1$ holds, and adding $O$ , whose norm is at most $1$ , leaves the norm unchanged; but $|1|_2 = 1$ .

This is the first step of the two-even-run case of Erdos287.mixed_gap_core. A gap- $\le 2$ representation splits into maximal step- $2$ runs of alternating parity, and Erdos287.two_unit_gaps shows at least two of those runs are even. When there are exactly two, this lemma forces them to have equal $2$ -adic weight, i.e. the two halved runs must have the same maximal $2$ -adic valuation $c$ — which by Erdos287.block_two_adic_length bounds each run's length by $2^{c+1}-1$ and places their midpoints at distinct odd multiples of $2^{c}$ , hence at distance at least $2^{c+1}$ .

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem even_blocks_distinct_norm (m₁ t₁ m₂ t₂ : ℕ) (hm₁ : 0 < m₁) (ht₁ : 0 < t₁)
    (hm₂ : 0 < m₂) (ht₂ : 0 < t₂)
    (hdiff : padicNorm 2 (∑ j ∈ Finset.range t₁, (1 : ℚ) / ((2 * (m₁ + j) : ℕ) : ℚ))
           ≠ padicNorm 2 (∑ j ∈ Finset.range t₂, (1 : ℚ) / ((2 * (m₂ + j) : ℕ) : ℚ)))
    (s : Finset ℕ) (g : ℕ → ℕ) (hodd : ∀ x ∈ s, ¬ 2 ∣ g x) (hg : ∀ x ∈ s, g x ≠ 0) :
    (∑ j ∈ Finset.range t₁, (1 : ℚ) / ((2 * (m₁ + j) : ℕ) : ℚ))
      + (∑ j ∈ Finset.range t₂, (1 : ℚ) / ((2 * (m₂ + j) : ℕ) : ℚ))
      + (∑ x ∈ s, (1 : ℚ) / (g x : ℚ)) ≠ 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

Two even runs of different 222-adic weight cannot complete to 111

Two even runs of different $2$ -adic weight cannot complete to $1$