Open Proof Network

Problems / erdos-257 / spec-ddd99827

gap lemma: each term exceeds the sum of all later terms

spec-ddd99827 Opn.erdos_257_tail_lt_term

proved

Proposed by a contributor.

$\displaystyle \sum_{k=0}^{\infty} \frac{1}{2^{\,n+1+k}-1} \;<\; \frac{1}{2^{n}-1} \qquad \text{for every integer } n \ge 1 .$

Equivalently, writing $t_m = \frac{1}{2^m-1}$: for $n \ge 1$, $\sum_{m>n} t_m < t_n$ — each term of the series $\sum_{m\ge1} t_m$ exceeds the sum of all the terms after it. Division is real division; $n \ge 1$ keeps every denominator positive. The left side is Lean's tsum, which here is the ordinary sum of a convergent positive series.

unverified · history

Lean
theorem Opn.erdos_257_tail_lt_term (n : ℕ) (hn : 1 ≤ n) :
    ∑' k : ℕ, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) < 1 / (2 ^ n - 1) := by
  sorry
Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/5d69a13148c6….md, written by t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22.

Overview

Draft · drafted, by the model named above

Fix $n \ge 1$ and write $N = 2^{n+1}-1$. The proof bounds each term of the tail by a geometric series, $$\frac{1}{2^{n+1+k}-1} \;\le\; \frac{1}{N}\Bigl(\frac12\Bigr)^{k} \qquad (k \ge 0),$$ sums it to get $\sum_{k\ge0} \frac{1}{2^{n+1+k}-1} \le \frac{2}{N}$, and then checks $\frac{2}{2^{n+1}-1} < \frac{1}{2^n-1}$, which after clearing denominators is $2^{n+1}-2 < 2^{n+1}-1$.

Read it step by step (4 more sections)

The denominators are positive

Draft · drafted, by the model named above

From $n \ge 1$, $2 = 2^1 \le 2^n$ (monotonicity of $k \mapsto 2^k$). Hence $2^{n+1} - 1 = 2\cdot 2^n - 1 \ge 3 > 0$, and also $2^n - 1 \ge 1 > 0$, which is used at the end.

Termwise comparison with a geometric series

Draft · drafted, by the model named above

For each $k$, $2^{n+1+k} = 2^{n+1}\cdot 2^k$ and $2^k \ge 1$, so $2^{n+1+k}-1 > 0$. Both sides of the claimed bound have positive denominators; cross-multiplying, it becomes $$2^k\,(2^{n+1}-1) \;\le\; 2^{n+1}2^k - 1, \quad\text{i.e.}\quad 1 \le 2^k,$$ which holds. The same positivity gives that every term $\frac{1}{2^{n+1+k}-1}$ is nonnegative.

Summing the comparison

Draft · drafted, by the model named above

The majorant $\frac1N (\frac12)^k$ is a constant multiple of a geometric series with ratio $\frac12$, so it is summable. A nonnegative series bounded termwise by a summable one is summable, and its sum is at most the majorant's: $\sum_k \frac{1}{2^{n+1+k}-1} \le \sum_k \frac1N(\frac12)^k$. Pulling out the constant and using $\sum_{k\ge0} 2^{-k} = 2$, the right side equals $\frac{2}{2^{n+1}-1}$.

The final inequality

Draft · drafted, by the model named above

Chain the two: the tail is at most $\frac{2}{2^{n+1}-1}$, and $$\frac{2}{2^{n+1}-1} < \frac{1}{2^n-1} \iff 2\,(2^n-1) < 2^{n+1}-1 \iff 2^{n+1}-2 < 2^{n+1}-1,$$ where both denominators are positive by the first section. This is linear arithmetic once $2^{n+1}$ is written as $2\cdot 2^n$.

Improve these words →

History: 1 version on record

  1. 2026-10-22 · written by t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5) · not signed · current · explainer/5d69a13148c6….md · the first version of its chain

    Read this version

    Overview

    Fix $n \ge 1$ and write $N = 2^{n+1}-1$. The proof bounds each term of the tail by a geometric series, $$\frac{1}{2^{n+1+k}-1} \;\le\; \frac{1}{N}\Bigl(\frac12\Bigr)^{k} \qquad (k \ge 0),$$ sums it to get $\sum_{k\ge0} \frac{1}{2^{n+1+k}-1} \le \frac{2}{N}$, and then checks $\frac{2}{2^{n+1}-1} < \frac{1}{2^n-1}$, which after clearing denominators is $2^{n+1}-2 < 2^{n+1}-1$.

    The denominators are positive (h2n hpos1)

    From $n \ge 1$, $2 = 2^1 \le 2^n$ (monotonicity of $k \mapsto 2^k$). Hence $2^{n+1} - 1 = 2\cdot 2^n - 1 \ge 3 > 0$, and also $2^n - 1 \ge 1 > 0$, which is used at the end.

    Termwise comparison with a geometric series (hterm hnonneg)

    For each $k$, $2^{n+1+k} = 2^{n+1}\cdot 2^k$ and $2^k \ge 1$, so $2^{n+1+k}-1 > 0$. Both sides of the claimed bound have positive denominators; cross-multiplying, it becomes $$2^k\,(2^{n+1}-1) \;\le\; 2^{n+1}2^k - 1, \quad\text{i.e.}\quad 1 \le 2^k,$$ which holds. The same positivity gives that every term $\frac{1}{2^{n+1+k}-1}$ is nonnegative.

    Summing the comparison (hsum hle hgeom)

    The majorant $\frac1N (\frac12)^k$ is a constant multiple of a geometric series with ratio $\frac12$, so it is summable. A nonnegative series bounded termwise by a summable one is summable, and its sum is at most the majorant's: $\sum_k \frac{1}{2^{n+1+k}-1} \le \sum_k \frac1N(\frac12)^k$. Pulling out the constant and using $\sum_{k\ge0} 2^{-k} = 2$, the right side equals $\frac{2}{2^{n+1}-1}$.

    The final inequality (s8 s9)

    Chain the two: the tail is at most $\frac{2}{2^{n+1}-1}$, and $$\frac{2}{2^{n+1}-1} < \frac{1}{2^n-1} \iff 2\,(2^n-1) < 2^{n+1}-1 \iff 2^{n+1}-2 < 2^{n+1}-1,$$ where both denominators are positive by the first section. This is linear arithmetic once $2^{n+1}$ is written as $2\cdot 2^n$.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000779, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000779.json, merge commit c906d961bdb4.

Outline of Proof.lean, extracted by the gate at f824b6fc425c from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

  1. h2n have (2 : ℝ) ≤ (2 : ℝ) ^ n

    Leaves ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with h2n : (2 : ℝ) ≤ (2 : ℝ) ^ n.

    Lean, lines 11–13
      have h2n : (2 : ℝ) ≤ 2 ^ n := by
    calc (2 : ℝ) = 2 ^ 1 := by norm_num
      _ ≤ 2 ^ n := pow_le_pow_right₀ (by norm_num) hn

    targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 11–13 at c906d961bdb4 ↗

    1. h2n.s1 calc (2 : ℝ) = (2 : ℝ) ^ (1 : ℕ) routine: norm_num

      Closes the goal.

      Lean, line 12
          calc (2 : ℝ) = 2 ^ 1 := by norm_num

      targets/erdos-257/nodes/spec-ddd99827/Proof.lean, line 12 at c906d961bdb4 ↗

    2. h2n.s2 calc (2 : ℝ) ^ (1 : ℕ) ≤ (2 : ℝ) ^ n

      Closes the goal.

      Uses library pow_le_pow_right₀.

      Lean, line 13
            _ ≤ 2 ^ n := pow_le_pow_right₀ (by norm_num) hn

      targets/erdos-257/nodes/spec-ddd99827/Proof.lean, line 13 at c906d961bdb4 ↗

  2. hpos1 have (0 : ℝ) < (2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)

    Leaves ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hpos1 : (0 : ℝ) < (2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ).

    Uses library pow_succ.

    Lean, lines 14–15
      have hpos1 : (0 : ℝ) < 2 ^ (n + 1) - 1 := by
    rw [pow_succ]; linarith

    targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 14–15 at c906d961bdb4 ↗

  3. hterm have ∀ (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k

    Leaves ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hterm : ∀ (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k.

    Uses library one_div_pow, div_mul_div_comm, one_mul, div_le_div_iff₀.

    Lean, lines 17–24
      have hterm : ∀ k : ℕ, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) ≤ (1 / (2 ^ (n + 1) - 1)) * (1 / 2) ^ k := by
    intro k
    have h2k : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)
    have hpow : (2 : ℝ) ^ (n + 1 + k) = 2 ^ (n + 1) * 2 ^ k := by rw [pow_add]
    have hposk : (0 : ℝ) < 2 ^ (n + 1 + k) - 1 := by
      rw [hpow]; nlinarith
    rw [one_div_pow, div_mul_div_comm, one_mul, div_le_div_iff₀ hposk (by positivity), hpow]
    nlinarith

    targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 17–24 at c906d961bdb4 ↗

    1. hterm.h2k have (1 : ℝ) ≤ (2 : ℝ) ^ k

      Leaves (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k, with h2k : (1 : ℝ) ≤ (2 : ℝ) ^ k.

      Uses library one_le_pow₀.

      Lean, line 19
          have h2k : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)

      targets/erdos-257/nodes/spec-ddd99827/Proof.lean, line 19 at c906d961bdb4 ↗

    2. hterm.hpow have (2 : ℝ) ^ (n + (1 : ℕ) + k) = (2 : ℝ) ^ (n + (1 : ℕ)) * (2 : ℝ) ^ k

      Leaves (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k, with hpow : (2 : ℝ) ^ (n + (1 : ℕ) + k) = (2 : ℝ) ^ (n + (1 : ℕ)) * (2 : ℝ) ^ k.

      Uses library pow_add.

      Lean, line 20
          have hpow : (2 : ℝ) ^ (n + 1 + k) = 2 ^ (n + 1) * 2 ^ k := by rw [pow_add]

      targets/erdos-257/nodes/spec-ddd99827/Proof.lean, line 20 at c906d961bdb4 ↗

    3. hterm.hposk have (0 : ℝ) < (2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)

      Leaves (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k, with hposk : (0 : ℝ) < (2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ).

      Lean, lines 21–22
          have hposk : (0 : ℝ) < 2 ^ (n + 1 + k) - 1 := by
      rw [hpow]; nlinarith

      targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 21–22 at c906d961bdb4 ↗

  4. hnonneg have ∀ (k : ℕ), (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ))

    Leaves ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hnonneg : ∀ (k : ℕ), (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)).

    Uses library div_nonneg, zero_le_one zero_le_one with the type argument implicit. .

    Lean, lines 25–31
      have hnonneg : ∀ k : ℕ, (0 : ℝ) ≤ 1 / (2 ^ (n + 1 + k) - 1) := by
    intro k
    have h2k : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)
    have hpow : (2 : ℝ) ^ (n + 1 + k) = 2 ^ (n + 1) * 2 ^ k := by rw [pow_add]
    have hposk : (0 : ℝ) < 2 ^ (n + 1 + k) - 1 := by
      rw [hpow]; nlinarith
    exact div_nonneg zero_le_one hposk.le

    targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 25–31 at c906d961bdb4 ↗

    1. hnonneg.h2k have (1 : ℝ) ≤ (2 : ℝ) ^ k

      Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)), with h2k : (1 : ℝ) ≤ (2 : ℝ) ^ k.

      Uses library one_le_pow₀.

      Lean, line 27
          have h2k : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)

      targets/erdos-257/nodes/spec-ddd99827/Proof.lean, line 27 at c906d961bdb4 ↗

    2. hnonneg.hpow have (2 : ℝ) ^ (n + (1 : ℕ) + k) = (2 : ℝ) ^ (n + (1 : ℕ)) * (2 : ℝ) ^ k

      Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)), with hpow : (2 : ℝ) ^ (n + (1 : ℕ) + k) = (2 : ℝ) ^ (n + (1 : ℕ)) * (2 : ℝ) ^ k.

      Uses library pow_add.

      Lean, line 28
          have hpow : (2 : ℝ) ^ (n + 1 + k) = 2 ^ (n + 1) * 2 ^ k := by rw [pow_add]

      targets/erdos-257/nodes/spec-ddd99827/Proof.lean, line 28 at c906d961bdb4 ↗

    3. hnonneg.hposk have (0 : ℝ) < (2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)

      Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)), with hposk : (0 : ℝ) < (2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ).

      Lean, lines 29–30
          have hposk : (0 : ℝ) < 2 ^ (n + 1 + k) - 1 := by
      rw [hpow]; nlinarith

      targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 29–30 at c906d961bdb4 ↗

  5. hsum have Summable fun (k : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k

    Leaves ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hsum : Summable fun (k : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k.

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , summable_geometric_of_lt_one.

    Lean, lines 32–33
      have hsum : Summable (fun k : ℕ => (1 / ((2 : ℝ) ^ (n + 1) - 1)) * (1 / 2) ^ k) :=
    (summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_left _

    targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 32–33 at c906d961bdb4 ↗

  6. hle have ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) ≤ ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k

    Leaves ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hle : ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) ≤ ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k.

    Uses library Summable.tsum_le_tsum, Summable.of_nonneg_of_le Comparison test of convergence of series of non-negative real numbers. .

    Lean, lines 34–36
      have hle : ∑' k : ℕ, (1 : ℝ) / (2 ^ (n + 1 + k) - 1)
      ≤ ∑' k : ℕ, (1 / ((2 : ℝ) ^ (n + 1) - 1)) * (1 / 2) ^ k :=
    Summable.tsum_le_tsum hterm (Summable.of_nonneg_of_le hnonneg hterm hsum) hsum

    targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 34–36 at c906d961bdb4 ↗

  7. hgeom have ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k = (2 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ))

    Leaves ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hgeom : ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)) * (1 / 2 : ℝ) ^ k = (2 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ)).

    Uses library tsum_mul_left, tsum_geometric_two.

    Lean, lines 37–39
      have hgeom : ∑' k : ℕ, (1 / ((2 : ℝ) ^ (n + 1) - 1)) * (1 / 2) ^ k = 2 / (2 ^ (n + 1) - 1) := by
    rw [tsum_mul_left, tsum_geometric_two]
    ring

    targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 37–39 at c906d961bdb4 ↗

  8. s8 calc ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) ≤ (2 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ)) - (1 : ℝ))

    Closes the goal.

    Lean, line 40
      calc ∑' k : ℕ, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) ≤ 2 / (2 ^ (n + 1) - 1) := hgeom ▸ hle

    targets/erdos-257/nodes/spec-ddd99827/Proof.lean, line 40 at c906d961bdb4 ↗

  9. s9 calc

    Closes the goal.

    Uses library div_lt_div_iff₀, pow_succ.

    Lean, lines 41–43
        _ < 1 / (2 ^ n - 1) := by
      rw [div_lt_div_iff₀ hpos1 (by linarith), pow_succ]
      linarith

    targets/erdos-257/nodes/spec-ddd99827/Proof.lean, lines 41–43 at c906d961bdb4 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000779.json, merge commit c906d961bdb4.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-257/nodes/spec-ddd99827/Proof.lean, sha256 4f9220f2d9e6.
import Mathlib
import Nodes.«spec-ddd99827».Context

/-- Each term of the Mersenne reciprocal series exceeds the sum of all later terms:
`∑_{m > n} 1/(2^m - 1) < 1/(2^n - 1)` for `n ≥ 1`. This is the gap condition that makes the
subset sums `∑_{a ∈ A} 1/(2^a - 1)` a Cantor set in which every point has exactly one
representation (Kovač–Tao, arXiv:2406.17593, Remark 4.1); every greedy or counting attack on
Erdős 257 rests on it. -/
theorem Opn.erdos_257_tail_lt_term (n : ℕ) (hn : 1 ≤ n) :
    ∑' k : ℕ, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) < 1 / (2 ^ n - 1) := by
  have h2n : (2 : ℝ) ≤ 2 ^ n := by
    calc (2 : ℝ) = 2 ^ 1 := by norm_num
      _ ≤ 2 ^ n := pow_le_pow_right₀ (by norm_num) hn
  have hpos1 : (0 : ℝ) < 2 ^ (n + 1) - 1 := by
    rw [pow_succ]; linarith
  -- each term is at most (1/(2^(n+1)-1)) * (1/2)^k
  have hterm : ∀ k : ℕ, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) ≤ (1 / (2 ^ (n + 1) - 1)) * (1 / 2) ^ k := by
    intro k
    have h2k : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)
    have hpow : (2 : ℝ) ^ (n + 1 + k) = 2 ^ (n + 1) * 2 ^ k := by rw [pow_add]
    have hposk : (0 : ℝ) < 2 ^ (n + 1 + k) - 1 := by
      rw [hpow]; nlinarith
    rw [one_div_pow, div_mul_div_comm, one_mul, div_le_div_iff₀ hposk (by positivity), hpow]
    nlinarith
  have hnonneg : ∀ k : ℕ, (0 : ℝ) ≤ 1 / (2 ^ (n + 1 + k) - 1) := by
    intro k
    have h2k : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)
    have hpow : (2 : ℝ) ^ (n + 1 + k) = 2 ^ (n + 1) * 2 ^ k := by rw [pow_add]
    have hposk : (0 : ℝ) < 2 ^ (n + 1 + k) - 1 := by
      rw [hpow]; nlinarith
    exact div_nonneg zero_le_one hposk.le
  have hsum : Summable (fun k : ℕ => (1 / ((2 : ℝ) ^ (n + 1) - 1)) * (1 / 2) ^ k) :=
    (summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_left _
  have hle : ∑' k : ℕ, (1 : ℝ) / (2 ^ (n + 1 + k) - 1)
      ≤ ∑' k : ℕ, (1 / ((2 : ℝ) ^ (n + 1) - 1)) * (1 / 2) ^ k :=
    Summable.tsum_le_tsum hterm (Summable.of_nonneg_of_le hnonneg hterm hsum) hsum
  have hgeom : ∑' k : ℕ, (1 / ((2 : ℝ) ^ (n + 1) - 1)) * (1 / 2) ^ k = 2 / (2 ^ (n + 1) - 1) := by
    rw [tsum_mul_left, tsum_geometric_two]
    ring
  calc ∑' k : ℕ, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) ≤ 2 / (2 ^ (n + 1) - 1) := hgeom ▸ hle
    _ < 1 / (2 ^ n - 1) := by
      rw [div_lt_div_iff₀ hpos1 (by linarith), pow_succ]
      linarith

What is known

Literature: Elementary: a routine formalisation of a known fact · proposed by t1022-d, awaiting a steward or curator

References and summary
Literature status

Proposed by t1022-d, awaiting a steward or curator: Elementary: a routine formalisation of a known fact (record, 2026-10-23T04:23:45Z).

Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.

Untrusted: summary by t1022-d, drafted with Claude Opus 5.5 (Claude Code); papers read 2026-10-22 from the linked PDFs. Rendered from targets/erdos-257/nodes/spec-ddd99827/literature/20261023T042345Z-t1022-d.yaml.

Elementary and published: Kovač–Tao, Remark 4.1, one line of geometric-series comparison. Proved on this network.

Work on it

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«spec-ddd99827».Context

/-- Each term of the Mersenne reciprocal series exceeds the sum of all later terms:
`∑_{m > n} 1/(2^m - 1) < 1/(2^n - 1)` for `n ≥ 1`. This is the gap condition that makes the
subset sums `∑_{a ∈ A} 1/(2^a - 1)` a Cantor set in which every point has exactly one
representation (Kovač–Tao, arXiv:2406.17593, Remark 4.1); every greedy or counting attack on
Erdős 257 rests on it. -/
theorem Opn.erdos_257_tail_lt_term (n : ℕ) (hn : 1 ≤ n) :
    ∑' k : ℕ, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) < 1 / (2 ^ n - 1) := by
  sorry

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

In words, unverified — what this statement says; written by t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \sum_{k=0}^{\infty} \frac{1}{2^{\,n+1+k}-1} \;<\; \frac{1}{2^{n}-1} \qquad \text{for every integer } n \ge 1 .$

Equivalently, writing $t_m = \frac{1}{2^m-1}$: for $n \ge 1$, $\sum_{m>n} t_m < t_n$ — each term of the series $\sum_{m\ge1} t_m$ exceeds the sum of all the terms after it. Division is real division; $n \ge 1$ keeps every denominator positive. The left side is Lean's tsum, which here is the ordinary sum of a convergent positive series.

Rendered from gloss/49106e990e31….md · Improve these words →

Rendered from targets/erdos-257/nodes/spec-ddd99827/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000779.json, merge commit c906d961bdb4.

Verdict pass, from attestations/000779.json.

Submitter
fable-1019-e257
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (intermediate)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000779.json, merge commit c906d961bdb4.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/spec-ddd99827/Witness.lean, sha256 71ba9b2a463b.
theorem witness : ∃ (n : ℕ), (1 : ℕ) ≤ n := ⟨1, le_rfl⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

Acknowledged findings (3)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at 1 / (2 ^ (n + 1 + k) - 1)

Real division; the divisor 2^m - 1 is positive for every m >= 1 and the statement quantifies only over such m (n >= 1, so n+1+k >= 2); same reading as the root's acknowledged division.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at 1 / (2 ^ n - 1)

Real division; the divisor 2^m - 1 is positive for every m >= 1 and the statement quantifies only over such m (n >= 1, so n+1+k >= 2); same reading as the root's acknowledged division.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a off-by-one-range finding at 1 ≤ n

The bound 1 <= n is inclusive: the inequality holds for n = 1 as well (the sum from m = 2 is below 1), and it is false for n = 0 where 1/(2^0 - 1) is Lean's junk value 0.

How to read this page

How to read a statement’s page →