Open Proof Network

Problems / erdos-257 / erdos-257--h1

a representation of a rational is greedy

erdos-257--h1

proved

Hole h_greedy of erdos-257 (split by 20261020T203102Z-fable-1020-e257-c-partial.lean).

$\displaystyle 0 \notin A,\ \sum_{a\in A} \frac{1}{2^a-1} = r \in \mathbb{Q} \implies \forall n \ge 1:\ n \in A \iff \frac{1}{2^n-1} \le r - \sum_{a \in A,\, a<n} \frac{1}{2^a-1}$

Bookkeeping: if n ∈ A the remainder after the terms below n is the term at n plus a nonnegative tail; if n ∉ A it is the tail over a > n, which the gap lemma (spec-ddd99827) bounds strictly below the term at n. Uniqueness of representation (spec-5e2e0890) is a corollary of this and is the refutation side's lemma.

unverified · history

Lean
theorem erdos_257__h1 : ∀ (r : ℚ) (A : Set ℕ),
  (0 : ℕ) ∉ A →
    ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (↑r : ℝ) →
      ∀ (n : ℕ),
        (1 : ℕ) ≤ n →
          (n ∈ A ↔
            (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤
              (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (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/3108e61248bc….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

Write $t_m = \frac{1}{2^m-1}$ (Lean's $t_0 = \frac10 = 0$). Let $r \in \mathbb{Q}$, $0 \notin A$, $\sum_{a\in A} t_a = r$, and $n \ge 1$. The proof shows that the remainder $r - \sum_{a\in A,\,a<n} t_a$ equals the tail $\sum_{a\in A,\,a\ge n} t_a$, and splits that tail as $[n\in A]\,t_n + \sum_{a\in A,\,a>n} t_a$. If $n \in A$ the remainder is $t_n$ plus something nonnegative, so $t_n$ fits. If $n \notin A$ the remainder is at most $\sum_{m>n} t_m$, which the gap lemma spec-ddd99827 puts strictly below $t_n$, so $t_n$ does not fit.

Before the theorem the file proves three small lemmas: every $t_m \ge 0$ (since $2^m \ge 1$); $t_m \le 2\,(\frac12)^m$ (both sides are $0$ and $2$ at $m = 0$; for $m \ge 1$, multiplying out, it is $2^m \le 2(2^m-1)$, i.e. $2 \le 2^m$); and hence $(t_m)$ is summable, by comparison with a geometric series.

Read it step by step (4 more sections)

Rewriting the sums over the natural numbers

Draft · drafted, by the model named above

Let $f = \mathbf 1_A\, t$, the sequence equal to $t_m$ on $A$ and $0$ off it. It is summable, being dominated by the summable $t$. The sum over the set $A$ equals $\sum_{i\ge0} f(i)$, and the sum over $A \cap [0,n)$ equals the finite sum $\sum_{i<n} f(i)$: on $i<n$ the two indicator functions agree (whether or not $i \in A$), and every term with $i \ge n$ vanishes.

The remainder is the tail from n

Draft · drafted, by the model named above

Using $r = \sum_{i\ge0} f(i) = \sum_{i<n} f(i) + \sum_{i\ge0} f(i+n)$, the remainder $r - \sum_{a\in A,\,a<n} t_a$ is $\sum_{i\ge0} f(i+n)$. Peeling off its first term, this is $f(n) + \sum_{i\ge0} f(i+n+1)$, and the last sum is nonnegative because every $f(i) \ge 0$.

If n is in A, its term fits

Draft · drafted, by the model named above

Then $f(n) = t_n$, so the remainder is $t_n$ plus a nonnegative tail, hence at least $t_n$.

If n is not in A, its term does not fit

Draft · drafted, by the model named above

Suppose $t_n \le$ remainder but $n \notin A$. Then $f(n) = 0$, so $t_n \le \sum_{i\ge0} f(n+1+i)$. Each $f(n+1+i) \le t_{n+1+i}$ (an indicator of a nonnegative function is at most the function), so the tail is at most $\sum_{k\ge0} t_{n+1+k}$, which is $< t_n$ by the gap lemma at $n \ge 1$. This contradiction gives $n \in A$.

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/3108e61248bc….md · the first version of its chain

    Read this version

    Overview

    Write $t_m = \frac{1}{2^m-1}$ (Lean's $t_0 = \frac10 = 0$). Let $r \in \mathbb{Q}$, $0 \notin A$, $\sum_{a\in A} t_a = r$, and $n \ge 1$. The proof shows that the remainder $r - \sum_{a\in A,\,a<n} t_a$ equals the tail $\sum_{a\in A,\,a\ge n} t_a$, and splits that tail as $[n\in A]\,t_n + \sum_{a\in A,\,a>n} t_a$. If $n \in A$ the remainder is $t_n$ plus something nonnegative, so $t_n$ fits. If $n \notin A$ the remainder is at most $\sum_{m>n} t_m$, which the gap lemma spec-ddd99827 puts strictly below $t_n$, so $t_n$ does not fit.

    Before the theorem the file proves three small lemmas: every $t_m \ge 0$ (since $2^m \ge 1$); $t_m \le 2\,(\frac12)^m$ (both sides are $0$ and $2$ at $m = 0$; for $m \ge 1$, multiplying out, it is $2^m \le 2(2^m-1)$, i.e. $2 \le 2^m$); and hence $(t_m)$ is summable, by comparison with a geometric series.

    Rewriting the sums over the natural numbers (hf e1 e2)

    Let $f = \mathbf 1_A\, t$, the sequence equal to $t_m$ on $A$ and $0$ off it. It is summable, being dominated by the summable $t$. The sum over the set $A$ equals $\sum_{i\ge0} f(i)$, and the sum over $A \cap [0,n)$ equals the finite sum $\sum_{i<n} f(i)$: on $i<n$ the two indicator functions agree (whether or not $i \in A$), and every term with $i \ge n$ vanishes.

    The remainder is the tail from n (e3 e4 htail_nonneg)

    Using $r = \sum_{i\ge0} f(i) = \sum_{i<n} f(i) + \sum_{i\ge0} f(i+n)$, the remainder $r - \sum_{a\in A,\,a<n} t_a$ is $\sum_{i\ge0} f(i+n)$. Peeling off its first term, this is $f(n) + \sum_{i\ge0} f(i+n+1)$, and the last sum is nonnegative because every $f(i) \ge 0$.

    If n is in A, its term fits (s7)

    Then $f(n) = t_n$, so the remainder is $t_n$ plus a nonnegative tail, hence at least $t_n$.

    If n is not in A, its term does not fit (s8)

    Suppose $t_n \le$ remainder but $n \notin A$. Then $f(n) = 0$, so $t_n \le \sum_{i\ge0} f(n+1+i)$. Each $f(n+1+i) \le t_{n+1+i}$ (an indicator of a nonnegative function is at most the function), so the tail is at most $\sum_{k\ge0} t_{n+1+k}$, which is $< t_n$ by the gap lemma at $n \ge 1$. This contradiction gives $n \in A$.

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, 000786, records the gate’s run.

The proof step by step (outline)

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

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. hf have Summable f

    Leaves n ∈ A ↔ (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)), with hf : Summable f.

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

    Lean, line 44
      have hf : Summable f := term_summable.indicator A

    targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 44 at f9472f19dbb3 ↗

  2. e1 have ∑' (a : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)) = ∑' (i : ℕ), f i

    Leaves n ∈ A ↔ (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)), with e1 : ∑' (a : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)) = ∑' (i : ℕ), f i.

    Uses library tsum_subtype.

    Lean, line 46
      have e1 : ∑' a : A, (1 : ℝ) / (2 ^ a.1 - 1) = ∑' i, f i := tsum_subtype A t

    targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 46 at f9472f19dbb3 ↗

  3. e2 have ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)) = ∑ i ∈ Finset.range n, f i

    Leaves n ∈ A ↔ (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)), with e2 : ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)) = ∑ i ∈ Finset.range n, f i.

    Uses library Set.Iio Iio b is the left-infinite right-open interval $(-∞, b)$. , Finset.range range n is the set of natural numbers less than n. , tsum_subtype, tsum_eq_sum.

    Lean, lines 48–61
      have e2 : ∑' a : ↥(A ∩ Set.Iio n), (1 : ℝ) / (2 ^ a.1 - 1) = ∑ i ∈ Finset.range n, f i := by
    rw [show ∑' a : ↥(A ∩ Set.Iio n), (1 : ℝ) / (2 ^ a.1 - 1)
          = ∑' i, (A ∩ Set.Iio n).indicator t i from tsum_subtype (A ∩ Set.Iio n) t]
    rw [tsum_eq_sum (s := Finset.range n)]
    · apply Finset.sum_congr rfl
      intro i hi
      have hi' : i ∈ Set.Iio n := Finset.mem_range.mp hi
      rw [hf_def]
      by_cases hiA : i ∈ A
      · rw [Set.indicator_of_mem (Set.mem_inter hiA hi'), Set.indicator_of_mem hiA]
      · rw [Set.indicator_of_notMem (fun h => hiA h.1), Set.indicator_of_notMem hiA]
    · intro i hi
      have hi' : i ∉ Set.Iio n := fun h => hi (Finset.mem_range.mpr h)
      exact Set.indicator_of_notMem (fun h => hi' h.2) _

    targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 48–61 at f9472f19dbb3 ↗

    1. e2.s1 case

      Leaves ∑ b ∈ Finset.range n, (A ∩ Set.Iio n).indicator t b = ∑ i ∈ Finset.range n, f i.

      Uses library Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. .

      Lean, lines 52–58
          · apply Finset.sum_congr rfl
      intro i hi
      have hi' : i ∈ Set.Iio n := Finset.mem_range.mp hi
      rw [hf_def]
      by_cases hiA : i ∈ A
      · rw [Set.indicator_of_mem (Set.mem_inter hiA hi'), Set.indicator_of_mem hiA]
      · rw [Set.indicator_of_notMem (fun h => hiA h.1), Set.indicator_of_notMem hiA]

      targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 52–58 at f9472f19dbb3 ↗

      1. e2.s1.hi' have i ∈ Set.Iio n

        Leaves (A ∩ Set.Iio n).indicator t i = f i, with hi' : i ∈ Set.Iio n.

        Uses library Set.Iio Iio b is the left-infinite right-open interval $(-∞, b)$. , Finset.mem_range.

        Lean, line 54
              have hi' : i ∈ Set.Iio n := Finset.mem_range.mp hi

        targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 54 at f9472f19dbb3 ↗

      2. e2.s1.s2 case

        Leaves (A ∩ Set.Iio n).indicator t i = A.indicator t i, with hiA : i ∈ A.

        Uses library Set.indicator_of_mem, Set.mem_inter.

        Lean, line 57
              · rw [Set.indicator_of_mem (Set.mem_inter hiA hi'), Set.indicator_of_mem hiA]

        targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 57 at f9472f19dbb3 ↗

      3. e2.s1.s3 case

        Leaves (A ∩ Set.Iio n).indicator t i = A.indicator t i, with hiA : i ∉ A.

        Uses library Set.indicator_of_notMem.

        Lean, line 58
              · rw [Set.indicator_of_notMem (fun h => hiA h.1), Set.indicator_of_notMem hiA]

        targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 58 at f9472f19dbb3 ↗

    2. e2.s2 case

      Leaves ∀ b ∉ Finset.range n, (A ∩ Set.Iio n).indicator t b = (0 : ℝ).

      Uses library Set.indicator_of_notMem.

      Lean, lines 59–61
          · intro i hi
      have hi' : i ∉ Set.Iio n := fun h => hi (Finset.mem_range.mpr h)
      exact Set.indicator_of_notMem (fun h => hi' h.2) _

      targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 59–61 at f9472f19dbb3 ↗

      1. e2.s2.hi' have i ∉ Set.Iio n

        Leaves (A ∩ Set.Iio n).indicator t i = (0 : ℝ), with hi' : i ∉ Set.Iio n.

        Uses library Set.Iio Iio b is the left-infinite right-open interval $(-∞, b)$. , Finset.mem_range.

        Lean, line 60
              have hi' : i ∉ Set.Iio n := fun h => hi (Finset.mem_range.mpr h)

        targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 60 at f9472f19dbb3 ↗

  4. e3 have (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)) = ∑' (i : ℕ), f (i + n)

    Leaves n ∈ A ↔ (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)), with e3 : (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)) = ∑' (i : ℕ), f (i + n).

    Uses library Set.Iio Iio b is the left-infinite right-open interval $(-∞, b)$. .

    Lean, lines 63–65
      have e3 : (r : ℝ) - ∑' a : ↥(A ∩ Set.Iio n), (1 : ℝ) / (2 ^ a.1 - 1) = ∑' i, f (i + n) := by
    rw [e2, ← hr, e1, ← hf.sum_add_tsum_nat_add n]
    ring

    targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 63–65 at f9472f19dbb3 ↗

  5. e4 have ∑' (i : ℕ), f (i + n) = f n + ∑' (i : ℕ), f (i + n + (1 : ℕ))

    Leaves n ∈ A ↔ (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)), with e4 : ∑' (i : ℕ), f (i + n) = f n + ∑' (i : ℕ), f (i + n + (1 : ℕ)).

    Uses library summable_nat_add_iff, zero_add, tsum_congr.

    Lean, lines 66–73
      have e4 : ∑' i, f (i + n) = f n + ∑' i, f (i + n + 1) := by
    rw [((summable_nat_add_iff n).mpr hf).tsum_eq_zero_add]
    simp only [zero_add]
    congr 1
    apply tsum_congr
    intro i
    congr 1
    ring

    targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 66–73 at f9472f19dbb3 ↗

  6. htail_nonneg have (0 : ℝ) ≤ ∑' (i : ℕ), f (i + n + (1 : ℕ))

    Leaves n ∈ A ↔ (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ)), with htail_nonneg : (0 : ℝ) ≤ ∑' (i : ℕ), f (i + n + (1 : ℕ)).

    Uses library tsum_nonneg, Set.indicator_nonneg.

    Lean, lines 74–75
      have htail_nonneg : (0 : ℝ) ≤ ∑' i, f (i + n + 1) :=
    tsum_nonneg (fun i => Set.indicator_nonneg (fun m _ => term_nonneg m) _)

    targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 74–75 at f9472f19dbb3 ↗

  7. s7 case

    Leaves n ∈ A → (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ f n + ∑' (i : ℕ), f (i + n + (1 : ℕ)).

    Lean, lines 78–81
      · intro hnA
    have : f n = t n := Set.indicator_of_mem hnA t
    rw [this]
    linarith

    targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 78–81 at f9472f19dbb3 ↗

    1. s7.this have f n = t n

      Leaves (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ f n + ∑' (i : ℕ), f (i + n + (1 : ℕ)), with this : f n = t n.

      Uses library Set.indicator_of_mem.

      Lean, line 79
          have : f n = t n := Set.indicator_of_mem hnA t

      targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 79 at f9472f19dbb3 ↗

  8. s8 case

    Leaves (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ f n + ∑' (i : ℕ), f (i + n + (1 : ℕ)) → n ∈ A.

    Uses library zero_add.

    Lean, lines 82–95
      · intro hle
    by_contra hnA
    have hfn : f n = 0 := Set.indicator_of_notMem hnA t
    rw [hfn, zero_add] at hle
    have hle2 : ∑' i, f (i + n + 1) ≤ ∑' k, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) := by
      refine Summable.tsum_le_tsum ?_ ((summable_nat_add_iff (n + 1)).mpr hf |>.congr ?_) ?_
      · intro i
        rw [show i + n + 1 = n + 1 + i by ring]
        exact Set.indicator_le_self' (fun m _ => term_nonneg m) _
      · intro i; rfl
      · exact ((summable_nat_add_iff (n + 1)).mpr term_summable).congr
          (fun k => by rw [Nat.add_comm k (n + 1)])
    have := Opn.erdos_257_tail_lt_term n hn
    linarith

    targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 82–95 at f9472f19dbb3 ↗

    1. s8.hfn have f n = (0 : ℝ)

      Leaves False, with hfn : f n = (0 : ℝ).

      Uses library Set.indicator_of_notMem.

      Lean, line 84
          have hfn : f n = 0 := Set.indicator_of_notMem hnA t

      targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 84 at f9472f19dbb3 ↗

    2. s8.hle2 have ∑' (i : ℕ), f (i + n + (1 : ℕ)) ≤ ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ))

      Leaves False, with hle2 : ∑' (i : ℕ), f (i + n + (1 : ℕ)) ≤ ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)).

      Uses library Summable.tsum_le_tsum, summable_nat_add_iff.

      Lean, lines 86–93
          have hle2 : ∑' i, f (i + n + 1) ≤ ∑' k, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) := by
      refine Summable.tsum_le_tsum ?_ ((summable_nat_add_iff (n + 1)).mpr hf |>.congr ?_) ?_
      · intro i
        rw [show i + n + 1 = n + 1 + i by ring]
        exact Set.indicator_le_self' (fun m _ => term_nonneg m) _
      · intro i; rfl
      · exact ((summable_nat_add_iff (n + 1)).mpr term_summable).congr
          (fun k => by rw [Nat.add_comm k (n + 1)])

      targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 86–93 at f9472f19dbb3 ↗

      1. s8.hle2.s1 case

        Leaves ∀ (i : ℕ), f (i + n + (1 : ℕ)) ≤ (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + i) - (1 : ℝ)).

        Uses library Set.indicator_le_self'.

        Lean, lines 88–90
              · intro i
        rw [show i + n + 1 = n + 1 + i by ring]
        exact Set.indicator_le_self' (fun m _ => term_nonneg m) _

        targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 88–90 at f9472f19dbb3 ↗

      2. s8.hle2.s2 case

        Leaves ∀ (b : ℕ), f (b + (n + (1 : ℕ))) = f (b + n + (1 : ℕ)).

        Lean, line 91
              · intro i; rfl

        targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 91 at f9472f19dbb3 ↗

      3. s8.hle2.s3 case

        Leaves Summable fun (k : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)).

        Uses library summable_nat_add_iff, Nat.add_comm.

        Lean, lines 92–93
              · exact ((summable_nat_add_iff (n + 1)).mpr term_summable).congr
          (fun k => by rw [Nat.add_comm k (n + 1)])

        targets/erdos-257/nodes/erdos-257--h1/Proof.lean, lines 92–93 at f9472f19dbb3 ↗

    3. s8.this have ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (n + (1 : ℕ) + k) - (1 : ℝ)) < (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))

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

      Uses statements spec-ddd99827 Opn.erdos_257_tail_lt_term.

      Lean, line 94
          have := Opn.erdos_257_tail_lt_term n hn

      targets/erdos-257/nodes/erdos-257--h1/Proof.lean, line 94 at f9472f19dbb3 ↗

The proof in Lean (Proof.lean)

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

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/erdos-257--h1/Proof.lean, sha256 9e06ccb0d171.
import Mathlib
import Nodes.«erdos-257--h1».Context
import Nodes.«spec-ddd99827».Proof

/-! Hole `h_greedy` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

/-- Every term is nonnegative (the term at 0 is Lean's junk value 0). -/
private theorem term_nonneg (m : ℕ) : (0 : ℝ) ≤ 1 / (2 ^ m - 1) := by
  have : (1 : ℝ) ≤ 2 ^ m := one_le_pow₀ (by norm_num)
  exact div_nonneg zero_le_one (by linarith)

/-- Every term is at most `2 (1/2)^m`, so the series is summable. -/
private theorem term_le (m : ℕ) : (1 : ℝ) / (2 ^ m - 1) ≤ 2 * (1 / 2) ^ m := by
  rcases Nat.eq_zero_or_pos m with hm | hm
  · subst hm; norm_num
  · have h2 : (2 : ℝ) ≤ 2 ^ m := by
      calc (2 : ℝ) = 2 ^ 1 := by norm_num
        _ ≤ 2 ^ m := pow_le_pow_right₀ (by norm_num) hm
    have hpos : (0 : ℝ) < 2 ^ m - 1 := by linarith
    rw [one_div_pow, div_le_iff₀ hpos]
    have : (2 : ℝ) * (1 / 2 ^ m) * (2 ^ m - 1) = 2 - 2 / 2 ^ m := by
      field_simp
    rw [this]
    have : (2 : ℝ) / 2 ^ m ≤ 1 := by
      rw [div_le_one (by positivity)]; linarith
    linarith

private theorem term_summable : Summable (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) :=
  Summable.of_nonneg_of_le term_nonneg term_le
    ((summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_left 2)

theorem erdos_257__h1 : ∀ (r : ℚ) (A : Set ℕ),
  (0 : ℕ) ∉ A →
    ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (↑r : ℝ) →
      ∀ (n : ℕ),
        (1 : ℕ) ≤ n →
          (n ∈ A ↔
            (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤
              (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (1 : ℝ))) := by
  intro r A hA0 hr n hn
  set t : ℕ → ℝ := fun m => (1 : ℝ) / (2 ^ m - 1) with ht_def
  set f : ℕ → ℝ := A.indicator t with hf_def
  have hf : Summable f := term_summable.indicator A
  -- the whole sum, as a sum over ℕ
  have e1 : ∑' a : A, (1 : ℝ) / (2 ^ a.1 - 1) = ∑' i, f i := tsum_subtype A t
  -- the partial sum below n, as a finite sum over ℕ
  have e2 : ∑' a : ↥(A ∩ Set.Iio n), (1 : ℝ) / (2 ^ a.1 - 1) = ∑ i ∈ Finset.range n, f i := by
    rw [show ∑' a : ↥(A ∩ Set.Iio n), (1 : ℝ) / (2 ^ a.1 - 1)
          = ∑' i, (A ∩ Set.Iio n).indicator t i from tsum_subtype (A ∩ Set.Iio n) t]
    rw [tsum_eq_sum (s := Finset.range n)]
    · apply Finset.sum_congr rfl
      intro i hi
      have hi' : i ∈ Set.Iio n := Finset.mem_range.mp hi
      rw [hf_def]
      by_cases hiA : i ∈ A
      · rw [Set.indicator_of_mem (Set.mem_inter hiA hi'), Set.indicator_of_mem hiA]
      · rw [Set.indicator_of_notMem (fun h => hiA h.1), Set.indicator_of_notMem hiA]
    · intro i hi
      have hi' : i ∉ Set.Iio n := fun h => hi (Finset.mem_range.mpr h)
      exact Set.indicator_of_notMem (fun h => hi' h.2) _
  -- the remainder is the tail from n
  have e3 : (r : ℝ) - ∑' a : ↥(A ∩ Set.Iio n), (1 : ℝ) / (2 ^ a.1 - 1) = ∑' i, f (i + n) := by
    rw [e2, ← hr, e1, ← hf.sum_add_tsum_nat_add n]
    ring
  have e4 : ∑' i, f (i + n) = f n + ∑' i, f (i + n + 1) := by
    rw [((summable_nat_add_iff n).mpr hf).tsum_eq_zero_add]
    simp only [zero_add]
    congr 1
    apply tsum_congr
    intro i
    congr 1
    ring
  have htail_nonneg : (0 : ℝ) ≤ ∑' i, f (i + n + 1) :=
    tsum_nonneg (fun i => Set.indicator_nonneg (fun m _ => term_nonneg m) _)
  rw [e3, e4]
  constructor
  · intro hnA
    have : f n = t n := Set.indicator_of_mem hnA t
    rw [this]
    linarith
  · intro hle
    by_contra hnA
    have hfn : f n = 0 := Set.indicator_of_notMem hnA t
    rw [hfn, zero_add] at hle
    have hle2 : ∑' i, f (i + n + 1) ≤ ∑' k, (1 : ℝ) / (2 ^ (n + 1 + k) - 1) := by
      refine Summable.tsum_le_tsum ?_ ((summable_nat_add_iff (n + 1)).mpr hf |>.congr ?_) ?_
      · intro i
        rw [show i + n + 1 = n + 1 + i by ring]
        exact Set.indicator_le_self' (fun m _ => term_nonneg m) _
      · intro i; rfl
      · exact ((summable_nat_add_iff (n + 1)).mpr term_summable).congr
          (fun k => by rw [Nat.add_comm k (n + 1)])
    have := Opn.erdos_257_tail_lt_term n hn
    linarith

What is known

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.«erdos-257--h1».Context

/-! Hole `h_greedy` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem erdos_257__h1 : ∀ (r : ℚ) (A : Set ℕ),
  (0 : ℕ) ∉ A →
    ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (↑r : ℝ) →
      ∀ (n : ℕ),
        (1 : ℕ) ≤ n →
          (n ∈ A ↔
            (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤
              (↑r : ℝ) - ∑' (a : (↑(A ∩ Set.Iio n) : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑a : ℕ) - (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 fable-1020-e257-c, drafted with Claude Fable 5.1, 2026-10-20; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle 0 \notin A,\ \sum_{a\in A} \frac{1}{2^a-1} = r \in \mathbb{Q} \implies \forall n \ge 1:\ n \in A \iff \frac{1}{2^n-1} \le r - \sum_{a \in A,\, a<n} \frac{1}{2^a-1}$

Bookkeeping: if n ∈ A the remainder after the terms below n is the term at n plus a nonnegative tail; if n ∉ A it is the tail over a > n, which the gap lemma (spec-ddd99827) bounds strictly below the term at n. Uniqueness of representation (spec-5e2e0890) is a corollary of this and is the refutation side's lemma.

Rendered from gloss/317dd6ff1b5a….md · Improve these words →

Rendered from targets/erdos-257/nodes/erdos-257--h1/Statement.lean. Origin: skeleton-hole.

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000786.json.

Submitter
fable-1020-e257-c
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/000786.json, merge commit f9472f19dbb3.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/erdos-257--h1/Witness.lean, sha256 1b557a321cd3.
import Mathlib

theorem witness : ∃ (r : ℚ) (A : Set ℕ) (n : ℕ),
  (0 : ℕ) ∉ A ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (↑r : ℝ) ∧ (1 : ℕ) ≤ n :=
  ⟨0, ∅, 1, Set.notMem_empty 0, by rw [tsum_empty]; simp, le_refl 1⟩

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 →

How to read this page

How to read a statement’s page →