Open Proof Network

Problems / erdos-257 / spec-23b0fff0

q times a binary tail of a rational sum is an integer

spec-23b0fff0 Opn.erdos_257_lambert_tail_integral

proved

Proposed by a contributor.

$\displaystyle \forall\, A \subseteq \mathbb{N},\ p \in \mathbb{Z},\ q \ge 1:\qquad \sum_{a\in A}\frac{1}{2^a-1} = \frac{p}{q}\ \Longrightarrow\ \forall j \ge 0:\quad q\,T_j \;=\; p\,2^{j} - q\sum_{m=0}^{j} f_A(m)\,2^{\,j-m},$ where $f_A(m) = \#\{a \in A : a \mid m\}$ for $m \ge 1$, $f_A(0) = 0$, and $T_j = \sum_{i \ge 1} \dfrac{f_A(j+i)}{2^{i}}$ is the tail of the binary expansion $\sum_{m\ge1} f_A(m)/2^m$ after position $j$, scaled by $2^j$.

In words: if the sum is rational with denominator $q$, then $q$ times every tail $T_j$ is an integer, and the integer is written out. On the right, $f_A(m)$ is Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} (the guard makes $f_A(0)=0$), $2^{j-m}$ is a natural-number power with $m \le j$ so the subtraction is exact, and the finite sum is Lean's Finset.sum over Finset.range (j+1), that is $m = 0, \dots, j$. On the left the tail is ∑' i, ncard {a ∈ A | a ∣ j + i + 1} / 2^(i+1), the ordinary sum of a convergent series ($f_A(m) \le d(m) \le m$). The hypothesis writes the rational as (p : ℝ) / (q : ℝ) with q : ℕ; the statement says nothing when $q = 0$ because of the hypothesis $0 < q$. A set containing $0$ changes neither side ($\frac{1}{2^0-1} = \frac10 = 0$ in Lean, and $0$ divides no $m \ge 1$).

unverified · history

Lean
theorem Opn.erdos_257_lambert_tail_integral :
    ∀ (A : Set ℕ) (p : ℤ) (q : ℕ), 0 < q →
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = p / q →
    ∀ j : ℕ,
      (q : ℝ) * ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ j + i + 1} : ℝ) / 2 ^ (i + 1) =
        ((p * 2 ^ j -
          q * ∑ m ∈ Finset.range (j + 1), (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℤ) * 2 ^ (j - m)
          : ℤ) : ℝ) := 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/4545a1ea50e5….md, written by t1026-c, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-26.

Overview

Draft · drafted, by the model named above

Write $F(m) = \#\{a \in A : 0 < m,\ a \mid m\}$ for the binary coefficients and $T_j = \sum_{i \ge 0} F(j+i+1)/2^{i+1}$ for the tail after position $j$. By the Lambert identity (the dependency Opn.erdos_257_lambert_identity, in scope through this node's Context) the hypothesis $\sum_{a\in A} 1/(2^a-1) = p/q$ reads $\sum_{m \ge 0} F(m)/2^m = p/q$. The proof splits that series at position $j$: the finite part is $\sum_{m \le j} F(m)/2^m$ and the rest is $2^{-j} T_j$. Multiplying by $q\,2^j$ and rearranging gives $q\,T_j = p\,2^j - q \sum_{m \le j} F(m)\,2^{j-m}$, which is the stated integer once the real-number identity is matched term by term with the integer expression.

Read it step by step (4 more sections)

The coefficients are summable

Draft · drafted, by the model named above

$F(m) \le m$: for $m = 0$ the counted set is empty, and for $m \ge 1$ it is a subset of the divisors of $m$, of which there are at most $m$ (hF_le). Hence $F(m)/2^m \le m/2^m$, which is summable, so $m \mapsto F(m)/2^m$ is summable (hFs). Rewriting the hypothesis through the Lambert identity gives $\sum_m F(m)/2^m = p/q$ (hlam).

The tail in the statement is the tail of $F$

Draft · drafted, by the model named above

The statement's tail counts $\{a \in A : a \mid j+i+1\}$ without the guard $0 < j+i+1$; since $j+i+1 \ge 1$ the guard holds, so the two sets agree and the statement's tail is $T_j$ (hjeq).

Splitting the series at $j$

Draft · drafted, by the model named above

$q > 0$ as a real (hb). Summability lets the series be split as the finite sum over $m \le j$ plus the shifted series $\sum_{i \ge 0} F(i + (j+1))/2^{i+(j+1)}$ (hsplit), and the shifted series is $2^{-j}\,T_j$ after reindexing $i + (j+1) = j + i + 1$ and factoring $2^{j+i+1} = 2^j \cdot 2^{i+1}$ (hshift).

Solving for $q\,T_j$ and matching the integer

Draft · drafted, by the model named above

With $q \ne 0$ and $2^j \ne 0$ (hb', h2j), clearing denominators in the split identity $\sum_{m \le j} F(m)/2^m + 2^{-j} T_j = p/q$ gives $q\,T_j = 2^j\bigl(p - q \sum_{m \le j} F(m)/2^m\bigr)$ (hT, a linear_combination of the cleared identity). The right side of the statement is the cast of the integer $p\,2^j - q \sum_{m \le j} F(m)\,2^{j-m}$; after pushing the cast through, the two sides agree term by term: $2^j p = p\,2^j$ (s11, ring), and for each $m \le j$, $2^j \cdot F(m)/2^m = F(m)\,2^{j-m}$ because $2^{j-m} = 2^j/2^m$ when $m \le j$ (s12). This closes the theorem.

Improve these words →

History: 1 version on record

  1. 2026-10-26 · written by t1026-c, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · explainer/4545a1ea50e5….md · the first version of its chain

    Read this version

    Overview

    Write $F(m) = \#\{a \in A : 0 < m,\ a \mid m\}$ for the binary coefficients and $T_j = \sum_{i \ge 0} F(j+i+1)/2^{i+1}$ for the tail after position $j$. By the Lambert identity (the dependency Opn.erdos_257_lambert_identity, in scope through this node's Context) the hypothesis $\sum_{a\in A} 1/(2^a-1) = p/q$ reads $\sum_{m \ge 0} F(m)/2^m = p/q$. The proof splits that series at position $j$: the finite part is $\sum_{m \le j} F(m)/2^m$ and the rest is $2^{-j} T_j$. Multiplying by $q\,2^j$ and rearranging gives $q\,T_j = p\,2^j - q \sum_{m \le j} F(m)\,2^{j-m}$, which is the stated integer once the real-number identity is matched term by term with the integer expression.

    The coefficients are summable (hF_le hFs hlam)

    $F(m) \le m$: for $m = 0$ the counted set is empty, and for $m \ge 1$ it is a subset of the divisors of $m$, of which there are at most $m$ (hF_le). Hence $F(m)/2^m \le m/2^m$, which is summable, so $m \mapsto F(m)/2^m$ is summable (hFs). Rewriting the hypothesis through the Lambert identity gives $\sum_m F(m)/2^m = p/q$ (hlam).

    The tail in the statement is the tail of $F$ (hjeq)

    The statement's tail counts $\{a \in A : a \mid j+i+1\}$ without the guard $0 < j+i+1$; since $j+i+1 \ge 1$ the guard holds, so the two sets agree and the statement's tail is $T_j$ (hjeq).

    Splitting the series at $j$ (hb hsplit hshift)

    $q > 0$ as a real (hb). Summability lets the series be split as the finite sum over $m \le j$ plus the shifted series $\sum_{i \ge 0} F(i + (j+1))/2^{i+(j+1)}$ (hsplit), and the shifted series is $2^{-j}\,T_j$ after reindexing $i + (j+1) = j + i + 1$ and factoring $2^{j+i+1} = 2^j \cdot 2^{i+1}$ (hshift).

    Solving for $q\,T_j$ and matching the integer (hb' h2j hT s11 s12)

    With $q \ne 0$ and $2^j \ne 0$ (hb', h2j), clearing denominators in the split identity $\sum_{m \le j} F(m)/2^m + 2^{-j} T_j = p/q$ gives $q\,T_j = 2^j\bigl(p - q \sum_{m \le j} F(m)/2^m\bigr)$ (hT, a linear_combination of the cleared identity). The right side of the statement is the cast of the integer $p\,2^j - q \sum_{m \le j} F(m)\,2^{j-m}$; after pushing the cast through, the two sides agree term by term: $2^j p = p\,2^j$ (s11, ring), and for each $m \le j$, $2^j \cdot F(m)/2^m = F(m)\,2^{j-m}$ because $2^{j-m} = 2^j/2^m$ when $m \le j$ (s12). This closes the theorem.

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000980.json, merge commit 60042fb834d8.

Outline of Proof.lean, extracted by the gate at be99b4fba02b 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_le have ∀ (m : ℕ), F m ≤ m

    Leaves (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ j + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with hF_le : ∀ (m : ℕ), F m ≤ m.

    Uses library Nat.eq_zero_or_pos.

    Lean, lines 26–40
      have hF_le : ∀ m, F m ≤ m := by
    intro m
    rcases Nat.eq_zero_or_pos m with rfl | hm
    · have h0 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by
        ext a
        simp
      simp [hF, h0]
    · have hsub : {a ∈ A | 0 < m ∧ a ∣ m} ⊆ ↑(Nat.divisors m) := by
        intro a ha
        simp only [Finset.mem_coe, Nat.mem_divisors]
        exact ⟨ha.2.2, hm.ne'⟩
      calc F m ≤ (↑(Nat.divisors m) : Set ℕ).ncard :=
            Set.ncard_le_ncard hsub (Finset.finite_toSet _)
        _ = (Nat.divisors m).card := Set.ncard_coe_finset _
        _ ≤ m := Nat.card_divisors_le_self m

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 26–40 at 60042fb834d8 ↗

    1. hF_le.s1 case

      Leaves F (0 : ℕ) ≤ (0 : ℕ).

      Lean, lines 29–32
          · have h0 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by
        ext a
        simp
      simp [hF, h0]

      targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 29–32 at 60042fb834d8 ↗

      1. hF_le.s1.h0 have {a : ℕ | a ∈ A ∧ (0 : ℕ) < (0 : ℕ) ∧ a ∣ (0 : ℕ)} = ∅

        Leaves F (0 : ℕ) ≤ (0 : ℕ), with h0 : {a : ℕ | a ∈ A ∧ (0 : ℕ) < (0 : ℕ) ∧ a ∣ (0 : ℕ)} = ∅.

        Lean, lines 29–31
            · have h0 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by
        ext a
        simp

        targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 29–31 at 60042fb834d8 ↗

    2. hF_le.s2 case

      Leaves F m ≤ m, with hm : m > (0 : ℕ).

      Lean, lines 33–40
          · have hsub : {a ∈ A | 0 < m ∧ a ∣ m} ⊆ ↑(Nat.divisors m) := by
        intro a ha
        simp only [Finset.mem_coe, Nat.mem_divisors]
        exact ⟨ha.2.2, hm.ne'⟩
      calc F m ≤ (↑(Nat.divisors m) : Set ℕ).ncard :=
            Set.ncard_le_ncard hsub (Finset.finite_toSet _)
        _ = (Nat.divisors m).card := Set.ncard_coe_finset _
        _ ≤ m := Nat.card_divisors_le_self m

      targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 33–40 at 60042fb834d8 ↗

      1. hF_le.s2.hsub have {a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m} ⊆ (↑m.divisors : Set ℕ)

        Leaves F m ≤ m, with hsub : {a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m} ⊆ (↑m.divisors : Set ℕ).

        Uses library Nat.divisors divisors n is the Finset of divisors of n. , Finset.mem_coe, Nat.mem_divisors, And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

        Lean, lines 33–36
            · have hsub : {a ∈ A | 0 < m ∧ a ∣ m} ⊆ ↑(Nat.divisors m) := by
        intro a ha
        simp only [Finset.mem_coe, Nat.mem_divisors]
        exact ⟨ha.2.2, hm.ne'⟩

        targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 33–36 at 60042fb834d8 ↗

      2. hF_le.s2.s2 calc F m ≤ (↑m.divisors : Set ℕ).ncard

        Closes the goal.

        Uses library Nat.divisors divisors n is the Finset of divisors of n. , Set A set is a collection of elements of some type α. , Set.ncard_le_ncard, Finset.finite_toSet Gives a Set.Finite for the Finset coerced to a Set. .

        Lean, lines 37–38
              calc F m ≤ (↑(Nat.divisors m) : Set ℕ).ncard :=
            Set.ncard_le_ncard hsub (Finset.finite_toSet _)

        targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 37–38 at 60042fb834d8 ↗

      3. hF_le.s2.s3 calc (↑m.divisors : Set ℕ).ncard = m.divisors.card

        Closes the goal.

        Uses library Nat.divisors divisors n is the Finset of divisors of n. , Set.ncard_coe_finset.

        Lean, line 39
                _ = (Nat.divisors m).card := Set.ncard_coe_finset _

        targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 39 at 60042fb834d8 ↗

      4. hF_le.s2.s4 calc m.divisors.card ≤ m

        Closes the goal.

        Uses library Nat.card_divisors_le_self.

        Lean, line 40
                _ ≤ m := Nat.card_divisors_le_self m

        targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 40 at 60042fb834d8 ↗

  2. hFs have Summable fun (m : ℕ) => (↑(F m) : ℝ) / (2 : ℝ) ^ m

    Leaves (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ j + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with hFs : Summable fun (m : ℕ) => (↑(F m) : ℝ) / (2 : ℝ) ^ m.

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Summable.of_nonneg_of_le Comparison test of convergence of series of non-negative real numbers. , div_eq_mul_inv Dividing by an element is the same as multiplying by its inverse. , one_div, inv_pow, pow_one.

    Lean, lines 41–48
      have hFs : Summable (fun m : ℕ => (F m : ℝ) / 2 ^ m) := by
    have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
      (by norm_num [abs_of_pos])
    refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h2
    have : (F i : ℝ) ≤ i := by exact_mod_cast hF_le i
    rw [div_eq_mul_inv, one_div, inv_pow, pow_one]
    have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
    nlinarith

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 41–48 at 60042fb834d8 ↗

    1. hFs.h2 have Summable fun (n : ℕ) => (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n

      Leaves Summable fun (m : ℕ) => (↑(F m) : ℝ) / (2 : ℝ) ^ m, with h2 : Summable fun (n : ℕ) => (↑n : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ n.

      Uses library summable_pow_mul_geometric_of_norm_lt_one, abs_of_pos.

      Lean, lines 42–43
          have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
      (by norm_num [abs_of_pos])

      targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 42–43 at 60042fb834d8 ↗

    2. hFs.s2 have (↑(F i) : ℝ) ≤ (↑i : ℝ)

      Leaves (↑(F i) : ℝ) / (2 : ℝ) ^ i ≤ (↑i : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ i, with this : (↑(F i) : ℝ) ≤ (↑i : ℝ).

      Lean, line 45
          have : (F i : ℝ) ≤ i := by exact_mod_cast hF_le i

      targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 45 at 60042fb834d8 ↗

    3. hFs.s3 have (0 : ℝ) ≤ ((2 : ℝ) ^ i)⁻¹ routine: positivity

      Leaves (↑(F i) : ℝ) * ((2 : ℝ) ^ i)⁻¹ ≤ (↑i : ℝ) * ((2 : ℝ) ^ i)⁻¹, with this : (0 : ℝ) ≤ ((2 : ℝ) ^ i)⁻¹.

      Lean, line 47
          have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity

      targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 47 at 60042fb834d8 ↗

  3. hlam have ∑' (m : ℕ), (↑(F m) : ℝ) / (2 : ℝ) ^ m = (↑p : ℝ) / (↑q : ℝ)

    Leaves (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ j + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with hlam : ∑' (m : ℕ), (↑(F m) : ℝ) / (2 : ℝ) ^ m = (↑p : ℝ) / (↑q : ℝ).

    Uses statements spec-137537c8 Opn.erdos_257_lambert_identity.

    Lean, lines 49–51
      have hlam : ∑' m : ℕ, (F m : ℝ) / 2 ^ m = p / q := by
    rw [← Opn.erdos_257_lambert_identity A]
    exact hsum

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 49–51 at 60042fb834d8 ↗

  4. hjeq have ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ j + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = tail

    Leaves (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ j + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with hjeq : ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ j + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = tail.

    Uses library Set.ncard The cardinality of s : Set α . , tsum_congr, Set.mem_ofPred_eq.

    Lean, lines 54–65
      have hjeq : ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ j + i + 1} : ℝ) / 2 ^ (i + 1) = tail := by
    simp only [htaildef, hF]
    apply tsum_congr
    intro i
    congr 3
    ext a
    simp only [Set.mem_ofPred_eq]
    constructor
    · rintro ⟨h1, h2⟩
      exact ⟨h1, by omega, h2⟩
    · rintro ⟨h1, _, h2⟩
      exact ⟨h1, h2⟩

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 54–65 at 60042fb834d8 ↗

    1. hjeq.s1 case

      Leaves a ∈ A ∧ a ∣ j + i + (1 : ℕ) → a ∈ A ∧ (0 : ℕ) < j + i + (1 : ℕ) ∧ a ∣ j + i + (1 : ℕ).

      Uses library And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

      Lean, lines 62–63
          · rintro ⟨h1, h2⟩
      exact ⟨h1, by omega, h2⟩

      targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 62–63 at 60042fb834d8 ↗

    2. hjeq.s2 case

      Leaves a ∈ A ∧ (0 : ℕ) < j + i + (1 : ℕ) ∧ a ∣ j + i + (1 : ℕ) → a ∈ A ∧ a ∣ j + i + (1 : ℕ).

      Uses library And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

      Lean, lines 64–65
          · rintro ⟨h1, _, h2⟩
      exact ⟨h1, h2⟩

      targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 64–65 at 60042fb834d8 ↗

  5. hb have (0 : ℝ) < (↑q : ℝ)

    Leaves (↑q : ℝ) * tail = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with hb : (0 : ℝ) < (↑q : ℝ).

    Lean, line 67
      have hb : (0 : ℝ) < q := by exact_mod_cast hq

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 67 at 60042fb834d8 ↗

  6. hsplit have ∑ i ∈ Finset.range (j + (1 : ℕ)), (↑(F i) : ℝ) / (2 : ℝ) ^ i + ∑' (i : ℕ), (↑(F (i + (j + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (j + (1 : ℕ))) = ∑' (i : ℕ), (↑(F i) : ℝ) / (2 : ℝ) ^ i

    Leaves (↑q : ℝ) * tail = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with hsplit : ∑ i ∈ Finset.range (j + (1 : ℕ)), (↑(F i) : ℝ) / (2 : ℝ) ^ i + ∑' (i : ℕ), (↑(F (i + (j + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (j + (1 : ℕ))) = ∑' (i : ℕ), (↑(F i) : ℝ) / (2 : ℝ) ^ i.

    Lean, line 68
      have hsplit := hFs.sum_add_tsum_nat_add (j + 1)

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 68 at 60042fb834d8 ↗

  7. hshift have ∑' (i : ℕ), (↑(F (i + (j + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (j + (1 : ℕ))) = (1 : ℝ) / (2 : ℝ) ^ j * tail

    Leaves (↑q : ℝ) * tail = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with hshift : ∑' (i : ℕ), (↑(F (i + (j + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (j + (1 : ℕ))) = (1 : ℝ) / (2 : ℝ) ^ j * tail.

    Uses library tsum_mul_left, tsum_congr.

    Lean, lines 69–76
      have hshift : ∑' i : ℕ, (F (i + (j + 1)) : ℝ) / 2 ^ (i + (j + 1)) = (1 / 2 ^ j) * tail := by
    simp only [htaildef]
    rw [← tsum_mul_left]
    apply tsum_congr
    intro i
    rw [show i + (j + 1) = j + i + 1 by ring,
      show (2:ℝ) ^ (j + i + 1) = 2 ^ j * 2 ^ (i + 1) by ring]
    field_simp

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 69–76 at 60042fb834d8 ↗

  8. hb' have (↑q : ℝ) ≠ (0 : ℝ)

    Leaves (↑q : ℝ) * tail = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with hb' : (↑q : ℝ) ≠ (0 : ℝ).

    Lean, line 78
      have hb' : (q : ℝ) ≠ 0 := hb.ne'

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 78 at 60042fb834d8 ↗

  9. h2j have (2 : ℝ) ^ j ≠ (0 : ℝ) routine: positivity

    Leaves (↑q : ℝ) * tail = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with h2j : (2 : ℝ) ^ j ≠ (0 : ℝ).

    Lean, line 79
      have h2j : (2:ℝ) ^ j ≠ 0 := by positivity

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 79 at 60042fb834d8 ↗

  10. hT have (↑q : ℝ) * tail = (2 : ℝ) ^ j * ((↑p : ℝ) - (↑q : ℝ) * ∑ n ∈ Finset.range (j + (1 : ℕ)), (↑(F n) : ℝ) / (2 : ℝ) ^ n)

    Leaves (↑q : ℝ) * tail = (↑(p * (2 : ℤ) ^ j - (↑q : ℤ) * ∑ m ∈ Finset.range (j + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (j - m)) : ℝ), with hT : (↑q : ℝ) * tail = (2 : ℝ) ^ j * ((↑p : ℝ) - (↑q : ℝ) * ∑ n ∈ Finset.range (j + (1 : ℕ)), (↑(F n) : ℝ) / (2 : ℝ) ^ n).

    Uses library Finset.range range n is the set of natural numbers less than n. .

    Lean, lines 80–84
      have hT : (q : ℝ) * tail =
      2 ^ j * (p - q * ∑ n ∈ Finset.range (j + 1), (F n : ℝ) / 2 ^ n) := by
    field_simp at hsplit
    field_simp
    linear_combination hsplit

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 80–84 at 60042fb834d8 ↗

  11. s11 case routine: ring

    Leaves (2 : ℝ) ^ j * (↑p : ℝ) = (↑p : ℝ) * (2 : ℝ) ^ j.

    Lean, line 89
      · ring

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 89 at 60042fb834d8 ↗

  12. s12 case

    Leaves ∑ i ∈ Finset.range (j + (1 : ℕ)), (2 : ℝ) ^ j * ((↑q : ℝ) * ((↑(F i) : ℝ) / (2 : ℝ) ^ i)) = ∑ i ∈ Finset.range (j + (1 : ℕ)), (↑q : ℝ) * ((↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < i ∧ a ∣ i}.ncard : ℝ) * (2 : ℝ) ^ (j - i)).

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

    Lean, lines 90–95
      · apply Finset.sum_congr rfl
    intro n hn
    have hn' : n ≤ j := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
    rw [pow_sub₀ _ (by norm_num) hn']
    field_simp
    simp only [hF]

    targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, lines 90–95 at 60042fb834d8 ↗

    1. s12.hn' have n ≤ j

      Leaves (2 : ℝ) ^ j * ((↑q : ℝ) * ((↑(F n) : ℝ) / (2 : ℝ) ^ n)) = (↑q : ℝ) * ((↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < n ∧ a ∣ n}.ncard : ℝ) * (2 : ℝ) ^ (j - n)), with hn' : n ≤ j.

      Uses library Nat.lt_succ_iff, Finset.mem_range.

      Lean, line 92
          have hn' : n ≤ j := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)

      targets/erdos-257/nodes/spec-23b0fff0/Proof.lean, line 92 at 60042fb834d8 ↗

The proof in Lean (Proof.lean)

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

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-23b0fff0/Proof.lean, sha256 7418d5bc6886.
import Mathlib
import Nodes.«spec-23b0fff0».Context

/-- Integrality of the binary tails, the second line of every digit-method proof for Erdős 257
(Erdős 1948 and 1968, Duverney–Tachiya 2019). Write `f_A(m) = #{a ∈ A : a ∣ m}` for the
coefficients of the binary expansion `∑_{a ∈ A} 1/(2^a - 1) = ∑_{m ≥ 1} f_A(m)/2^m`
(`Opn.erdos_257_lambert_identity`) and `T_j = ∑_{i ≥ 1} f_A(j+i)/2^i` for the tail after
position `j`, scaled by `2^j`. If the sum is the rational `p/q` then, for every `j`,
`q · T_j = p · 2^j - q · ∑_{m ≤ j} f_A(m) 2^(j-m)`, an integer. Every proof of a special case
then shows that for a well-chosen `j` this integer cannot exist: it is positive whenever some
element of `A` exceeds `j` (so `T_j ≥ 1/q`), while a block of coefficients `f_A(j+1), …,
f_A(j+k)` that vanish, or are divisible by `2^k`, forces `q · T_{j+k} ≥ 2^k` against an upper
bound on that tail. In Lean `2^(j-m)` is a natural-number power with `m ≤ j`, so the subtraction
is exact, and `f_A(0) = 0` by the guard `0 < m`. -/
theorem Opn.erdos_257_lambert_tail_integral :
    ∀ (A : Set ℕ) (p : ℤ) (q : ℕ), 0 < q →
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = p / q →
    ∀ j : ℕ,
      (q : ℝ) * ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ j + i + 1} : ℝ) / 2 ^ (i + 1) =
        ((p * 2 ^ j -
          q * ∑ m ∈ Finset.range (j + 1), (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℤ) * 2 ^ (j - m)
          : ℤ) : ℝ) := by
  intro A p q hq hsum j
  classical
  set F : ℕ → ℕ := fun m => Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} with hF
  have hF_le : ∀ m, F m ≤ m := by
    intro m
    rcases Nat.eq_zero_or_pos m with rfl | hm
    · have h0 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by
        ext a
        simp
      simp [hF, h0]
    · have hsub : {a ∈ A | 0 < m ∧ a ∣ m} ⊆ ↑(Nat.divisors m) := by
        intro a ha
        simp only [Finset.mem_coe, Nat.mem_divisors]
        exact ⟨ha.2.2, hm.ne'⟩
      calc F m ≤ (↑(Nat.divisors m) : Set ℕ).ncard :=
            Set.ncard_le_ncard hsub (Finset.finite_toSet _)
        _ = (Nat.divisors m).card := Set.ncard_coe_finset _
        _ ≤ m := Nat.card_divisors_le_self m
  have hFs : Summable (fun m : ℕ => (F m : ℝ) / 2 ^ m) := by
    have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
      (by norm_num [abs_of_pos])
    refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h2
    have : (F i : ℝ) ≤ i := by exact_mod_cast hF_le i
    rw [div_eq_mul_inv, one_div, inv_pow, pow_one]
    have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
    nlinarith
  have hlam : ∑' m : ℕ, (F m : ℝ) / 2 ^ m = p / q := by
    rw [← Opn.erdos_257_lambert_identity A]
    exact hsum
  -- the tail in the statement is the tail of `F`
  set tail : ℝ := ∑' i : ℕ, (F (j + i + 1) : ℝ) / 2 ^ (i + 1) with htaildef
  have hjeq : ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ j + i + 1} : ℝ) / 2 ^ (i + 1) = tail := by
    simp only [htaildef, hF]
    apply tsum_congr
    intro i
    congr 3
    ext a
    simp only [Set.mem_ofPred_eq]
    constructor
    · rintro ⟨h1, h2⟩
      exact ⟨h1, by omega, h2⟩
    · rintro ⟨h1, _, h2⟩
      exact ⟨h1, h2⟩
  rw [hjeq]
  have hb : (0 : ℝ) < q := by exact_mod_cast hq
  have hsplit := hFs.sum_add_tsum_nat_add (j + 1)
  have hshift : ∑' i : ℕ, (F (i + (j + 1)) : ℝ) / 2 ^ (i + (j + 1)) = (1 / 2 ^ j) * tail := by
    simp only [htaildef]
    rw [← tsum_mul_left]
    apply tsum_congr
    intro i
    rw [show i + (j + 1) = j + i + 1 by ring,
      show (2:ℝ) ^ (j + i + 1) = 2 ^ j * 2 ^ (i + 1) by ring]
    field_simp
  rw [hshift, hlam] at hsplit
  have hb' : (q : ℝ) ≠ 0 := hb.ne'
  have h2j : (2:ℝ) ^ j ≠ 0 := by positivity
  have hT : (q : ℝ) * tail =
      2 ^ j * (p - q * ∑ n ∈ Finset.range (j + 1), (F n : ℝ) / 2 ^ n) := by
    field_simp at hsplit
    field_simp
    linear_combination hsplit
  rw [hT]
  push_cast
  rw [mul_sub, Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]
  congr 1
  · ring
  · apply Finset.sum_congr rfl
    intro n hn
    have hn' : n ≤ j := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
    rw [pow_sub₀ _ (by norm_num) hn']
    field_simp
    simp only [hF]

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.«spec-23b0fff0».Context

/-- Integrality of the binary tails, the second line of every digit-method proof for Erdős 257
(Erdős 1948 and 1968, Duverney–Tachiya 2019). Write `f_A(m) = #{a ∈ A : a ∣ m}` for the
coefficients of the binary expansion `∑_{a ∈ A} 1/(2^a - 1) = ∑_{m ≥ 1} f_A(m)/2^m`
(`Opn.erdos_257_lambert_identity`) and `T_j = ∑_{i ≥ 1} f_A(j+i)/2^i` for the tail after
position `j`, scaled by `2^j`. If the sum is the rational `p/q` then, for every `j`,
`q · T_j = p · 2^j - q · ∑_{m ≤ j} f_A(m) 2^(j-m)`, an integer. Every proof of a special case
then shows that for a well-chosen `j` this integer cannot exist: it is positive whenever some
element of `A` exceeds `j` (so `T_j ≥ 1/q`), while a block of coefficients `f_A(j+1), …,
f_A(j+k)` that vanish, or are divisible by `2^k`, forces `q · T_{j+k} ≥ 2^k` against an upper
bound on that tail. In Lean `2^(j-m)` is a natural-number power with `m ≤ j`, so the subtraction
is exact, and `f_A(0) = 0` by the guard `0 < m`. -/
theorem Opn.erdos_257_lambert_tail_integral :
    ∀ (A : Set ℕ) (p : ℤ) (q : ℕ), 0 < q →
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = p / q →
    ∀ j : ℕ,
      (q : ℝ) * ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ j + i + 1} : ℝ) / 2 ^ (i + 1) =
        ((p * 2 ^ j -
          q * ∑ m ∈ Finset.range (j + 1), (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℤ) * 2 ^ (j - m)
          : ℤ) : ℝ) := 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 t1026-c, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-26; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \forall\, A \subseteq \mathbb{N},\ p \in \mathbb{Z},\ q \ge 1:\qquad \sum_{a\in A}\frac{1}{2^a-1} = \frac{p}{q}\ \Longrightarrow\ \forall j \ge 0:\quad q\,T_j \;=\; p\,2^{j} - q\sum_{m=0}^{j} f_A(m)\,2^{\,j-m},$ where $f_A(m) = \#\{a \in A : a \mid m\}$ for $m \ge 1$, $f_A(0) = 0$, and $T_j = \sum_{i \ge 1} \dfrac{f_A(j+i)}{2^{i}}$ is the tail of the binary expansion $\sum_{m\ge1} f_A(m)/2^m$ after position $j$, scaled by $2^j$.

In words: if the sum is rational with denominator $q$, then $q$ times every tail $T_j$ is an integer, and the integer is written out. On the right, $f_A(m)$ is Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} (the guard makes $f_A(0)=0$), $2^{j-m}$ is a natural-number power with $m \le j$ so the subtraction is exact, and the finite sum is Lean's Finset.sum over Finset.range (j+1), that is $m = 0, \dots, j$. On the left the tail is ∑' i, ncard {a ∈ A | a ∣ j + i + 1} / 2^(i+1), the ordinary sum of a convergent series ($f_A(m) \le d(m) \le m$). The hypothesis writes the rational as (p : ℝ) / (q : ℝ) with q : ℕ; the statement says nothing when $q = 0$ because of the hypothesis $0 < q$. A set containing $0$ changes neither side ($\frac{1}{2^0-1} = \frac10 = 0$ in Lean, and $0$ divides no $m \ge 1$).

Rendered from gloss/673332d6c86f….md · Improve these words →

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

Depends on (1), each in words

Depends on, each in words where someone has written them:

  • spec-137537c8 Opn.erdos_257_lambert_identity: $\forall\, A \subseteq \mathbb{N}:\qquad \sum_{a\in A}\frac{1}{2^a-1} \;=\; \sum_{m\ge 1}\frac{f_A(m)}{2^m},\qquad f_A(m) = \#\{a \in A : a \mid m\}.$ · used by the proof
Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000980.json, merge commit 60042fb834d8.

Verdict pass, from attestations/000980.json.

Submitter
t1026-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/000980.json, merge commit 60042fb834d8.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/spec-23b0fff0/Witness.lean, sha256 34e28f0e1fb4.
import Nodes.«spec-23b0fff0».Context

theorem witness : ∃ (A : Set ℕ) (p : ℤ) (q : ℕ) (j : ℕ),
  (0 : ℕ) < q ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ) :=
  ⟨∅, 0, 1, 0, one_pos, by rw [tsum_empty]; simp⟩

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 (5)

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

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

The divisor is zero only at n = 0, where Lean's junk value makes the term 0, the convention every node of this target uses.

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

Untrusted: acknowledgment of a div-zero finding at ↑p / ↑q

q is a natural number with the hypothesis 0 < q, so the division is by a positive real; p / q is the rational value of the sum.

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

Untrusted: acknowledgment of a div-zero finding at ↑{a | a ∈ A ∧ a ∣ j + i + 1}.ncard / 2 ^ (i + 1)

The divisor 2^(i+1) is a positive real for every natural i.

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

Untrusted: acknowledgment of a nat-sub finding at j - m

m ranges over Finset.range (j + 1), so m ≤ j and the natural-number subtraction j - m is exact; 2^(j-m) is the weight of the m-th coefficient scaled to position j.

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

Untrusted: acknowledgment of a off-by-one-range finding at Finset.range (j + 1)

The finite sum runs over m = 0, …, j inclusive, the coefficients up to and including position j; the m = 0 term is 0 because the counted set is guarded by 0 < m.

How to read this page

How to read a statement’s page →