The leading $p$ -adic layer of a unit-fraction representation of $1$ cancels

Proved

Erdos287.padic_leading_cancel

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

number-theoryp-adicunit-fractions

Let $k \ge 2$ and let $n_0, \dots, n_{k-1}$ be integers, each $> 1$ , with $\sum_{i<k} 1/n_i = 1$ . Fix a prime $p$ and an integer $a \ge 1$ with $v_p(n_i) \le a$ for all $i$ (for instance $a$ the maximal $p$ -adic valuation occurring, assumed positive). Write

M = \{\, i < k : v_p(n_i) = a \,\}

for the leading layer. Then

\Big| \sum_{i \in M} \frac{1}{n_i} \Big|_p < p^{\,a} .

Every individual term of the leading layer has $p$ -adic norm exactly $p^a$ , so the inequality is strict precisely because the leading terms cancel against one another.

The proof splits the sum at the layer: the complement has norm below $p^a$ because each of its terms does, while the layer itself has norm at most $p^a$ by the ultrametric inequality. Were the layer's norm equal to $p^a$ , the two parts would have different norms and the total would satisfy $|1|_p = p^a > 1$ , contradicting $|1|_p = 1$ .

This strictly strengthens Erdos287.padic_multiplicity, which only records that the leading layer has at least two members. For $p = 2$ the present statement says the layer has an even number of members; for odd $p$ it imposes a weighted congruence on the unit parts $n_i/p^a$ . Iterating it downwards through $a, a-1, \dots, 1$ is the layer-by-layer machinery needed for the residual core Erdos287.mixed_gap_core, where the two-even-run case stalls exactly because the leading layers of the two runs cancel and every lower layer must then be analysed in turn.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem padic_leading_cancel (k : ℕ) (hk : 2 ≤ k) (f : ℕ → ℕ)
    (hf1 : ∀ i, i < k → 1 < f i)
    (hsum : ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1)
    (p : ℕ) (hp : Nat.Prime p) (a : ℕ) (ha : 1 ≤ a)
    (hmax : ∀ i, i < k → padicValNat p (f i) ≤ a) :
    padicNorm p (∑ i ∈ (Finset.range k).filter (fun i => padicValNat p (f i) = a),
      (1 : ℚ) / f i) < (p : ℚ) ^ (a : ℤ) := by sorry
end Erdos287

Source

Auxiliary result proved for the prove2.me mission on Erdos problem #287 (https://www.erdosproblems.com/287). Strengthens Erdos287.padic_multiplicity from 'the maximal p-adic valuation is attained twice' to 'the leading layer cancels'. Classical background: P. Erdos, 'Egy Kurschak-fele elemi szamelmeleti tetel altalanositasa', Mat. Fiz. Lapok 39 (1932), 17-24. A new auxiliary lemma, not a quotation from the literature.

View graph

The leading ppp-adic layer of a unit-fraction representation of 111 cancels

The leading $p$ -adic layer of a unit-fraction representation of $1$ cancels