coefficients divisible by 2^k ⇒ q·T is a multiple of 2^k

spec-689ac1ac Opn.erdos_257_divisible_block

proved

Proposed by a contributor.

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

In words: if the sum is rational with denominator $q$, and the $k$ coefficients just after position $y$ are all divisible by $2^k$ (in particular if they all vanish), then $q$ times the tail after the block is an integer multiple of $2^k$. The block condition is ∀ i, 1 ≤ i → i ≤ k → 2 ^ k ∣ Set.ncard {a ∈ A | a ∣ y + i}, positions $y+1, \dots, y+k$ inclusive; with $k = 0$ it is empty and the conclusion only says $q\,T_y$ is an integer. The tail is ∑' i, ncard {a ∈ A | a ∣ y + k + 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 : ℕ and $0 < q$. The statement does not say the multiple is nonzero: for infinite $A$ the tail is positive, so $N \ge 1$ and $q\,T_{y+k} \ge 2^k$, but that step is not part of this statement.

unverified · history

Lean

theorem Opn.erdos_257_divisible_block :
    ∀ (A : Set ℕ) (p : ℤ) (q : ℕ), 0 < q →
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = p / q →
    ∀ y k : ℕ, (∀ i, 1 ≤ i → i ≤ k → 2 ^ k ∣ Set.ncard {a ∈ A | a ∣ y + i}) →
      ∃ N : ℤ,
        (q : ℝ) * ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ y + k + i + 1} : ℝ) / 2 ^ (i + 1) =
          2 ^ k * N := 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/392c70638981….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$. Given $\sum_{a\in A} 1/(2^a-1) = p/q$ and $2^k \mid F(y+i)$ for $i = 1, \dots, k$, the proof produces an integer $N$ with $q\,T_{y+k} = 2^k N$. The two facts it combines are the dependency Opn.erdos_257_lambert_tail_integral (in scope through this node's Context), which says $q\,T_y$ is the explicit integer $Z = p\,2^y - q\sum_{m \le y} F(m) 2^{y-m}$, and the splitting $T_y = \sum_{i<k} F(y+i+1)/2^{i+1} + 2^{-k}\,T_{y+k}$. Hence $q\,T_{y+k} = 2^k\bigl(Z - q\sum_{i<k} F(y+i+1)/2^{i+1}\bigr)$, and each $F(y+i+1)/2^{i+1} = (F(y+i+1)/2^k)\cdot 2^{k-i-1}$ is an integer by the divisibility, so $N = Z - q \sum_{i<k} (F(y+i+1)/2^k)\, 2^{k-(i+1)}$.

Read it step by step (5 more sections)

The coefficients, with and without the guard

Draft · drafted, by the model named above

The statement writes a coefficient at a position $m \ge 1$ as $\#\{a \in A : a \mid m\}$, without the guard $0 < m$; for $m > 0$ this is $F(m)$, as a natural number (hFeqN) and as a real (hFeq). $F(m) \le m$ (the counted set is empty at $m = 0$ and a subset of the divisors of $m$ otherwise; hF_le), so $m \mapsto F(m)/2^m$ is dominated by $m/2^m$ and summable (hFs).

The tails

Draft · drafted, by the model named above

Each tail $j \mapsto T_j$ is a summable series: it is $2^j$ times a shift of the summable $F(m)/2^m$ (hTsum). The dependency applied at $j = y$ gives $q\,T_y = Z$ (hZ), once the statement's unguarded tail is identified with $T_y$ (hTy); the goal's tail is likewise $T_{y+k}$ (hTyk).

Splitting $T_y$ at the block

Draft · drafted, by the model named above

Summability lets $T_y$ be split into its first $k$ terms $\sum_{i<k} F(y+i+1)/2^{i+1}$ and the remaining series, which after reindexing $y + (i+k) + 1 = (y+k) + i + 1$ and factoring $2^{i+k+1} = 2^k \cdot 2^{i+1}$ is $2^{-k}\,T_{y+k}$ (hsplit).

The block coefficients are multiples of $2^k$

Draft · drafted, by the model named above

For $i < k$, the hypothesis at $i + 1$ (which lies in $[1, k]$), read through hFeqN, says $2^k \mid F(y+i+1)$; so $F(y+i+1) = 2^k \cdot (F(y+i+1) / 2^k)$ with exact natural-number division, as reals (hdiv).

Assembling the integer

Draft · drafted, by the model named above

$2^k \ne 0$ (h2k). From the splitting, $q\,T_{y+k} = 2^k\,(q\,T_y - q \sum_{i<k} F(y+i+1)/2^{i+1})$ (key). Substituting $q\,T_y = Z$ and pushing the integer cast through, the claim $q\,T_{y+k} = 2^k N$ reduces to matching, for each $i < k$, the real term $q \cdot F(y+i+1)/2^{i+1}$ with $q \cdot (F(y+i+1)/2^k) \cdot 2^{k-(i+1)}$: using hdiv and $2^{k-(i+1)} = 2^k / 2^{i+1}$ for $i + 1 \le k$ (hi'), the two agree, and a final cast step identifies the natural-number quotient with its integer image.

Improve these words →

History: 1 version on record

2026-10-26 · written by t1026-c, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · explainer/392c70638981….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$. Given $\sum_{a\in A} 1/(2^a-1) = p/q$ and $2^k \mid F(y+i)$ for $i = 1, \dots, k$, the proof produces an integer $N$ with $q\,T_{y+k} = 2^k N$. The two facts it combines are the dependency Opn.erdos_257_lambert_tail_integral (in scope through this node's Context), which says $q\,T_y$ is the explicit integer $Z = p\,2^y - q\sum_{m \le y} F(m) 2^{y-m}$, and the splitting $T_y = \sum_{i<k} F(y+i+1)/2^{i+1} + 2^{-k}\,T_{y+k}$. Hence $q\,T_{y+k} = 2^k\bigl(Z - q\sum_{i<k} F(y+i+1)/2^{i+1}\bigr)$, and each $F(y+i+1)/2^{i+1} = (F(y+i+1)/2^k)\cdot 2^{k-i-1}$ is an integer by the divisibility, so $N = Z - q \sum_{i<k} (F(y+i+1)/2^k)\, 2^{k-(i+1)}$.
The coefficients, with and without the guard (hFeqN hFeq hF_le hFs)
The statement writes a coefficient at a position $m \ge 1$ as $\#\{a \in A : a \mid m\}$, without the guard $0 < m$; for $m > 0$ this is $F(m)$, as a natural number (hFeqN) and as a real (hFeq). $F(m) \le m$ (the counted set is empty at $m = 0$ and a subset of the divisors of $m$ otherwise; hF_le), so $m \mapsto F(m)/2^m$ is dominated by $m/2^m$ and summable (hFs).
The tails (hTsum hZ hTy hTyk)
Each tail $j \mapsto T_j$ is a summable series: it is $2^j$ times a shift of the summable $F(m)/2^m$ (hTsum). The dependency applied at $j = y$ gives $q\,T_y = Z$ (hZ), once the statement's unguarded tail is identified with $T_y$ (hTy); the goal's tail is likewise $T_{y+k}$ (hTyk).
Splitting $T_y$ at the block (hsplit)
Summability lets $T_y$ be split into its first $k$ terms $\sum_{i<k} F(y+i+1)/2^{i+1}$ and the remaining series, which after reindexing $y + (i+k) + 1 = (y+k) + i + 1$ and factoring $2^{i+k+1} = 2^k \cdot 2^{i+1}$ is $2^{-k}\,T_{y+k}$ (hsplit).
The block coefficients are multiples of $2^k$ (hdiv)
For $i < k$, the hypothesis at $i + 1$ (which lies in $[1, k]$), read through hFeqN, says $2^k \mid F(y+i+1)$; so $F(y+i+1) = 2^k \cdot (F(y+i+1) / 2^k)$ with exact natural-number division, as reals (hdiv).
Assembling the integer (h2k key hi')
$2^k \ne 0$ (h2k). From the splitting, $q\,T_{y+k} = 2^k\,(q\,T_y - q \sum_{i<k} F(y+i+1)/2^{i+1})$ (key). Substituting $q\,T_y = Z$ and pushing the integer cast through, the claim $q\,T_{y+k} = 2^k N$ reduces to matching, for each $i < k$, the real term $q \cdot F(y+i+1)/2^{i+1}$ with $q \cdot (F(y+i+1)/2^k) \cdot 2^{k-(i+1)}$: using hdiv and $2^{k-(i+1)} = 2^k / 2^{i+1}$ for $i + 1 \le k$ (hi'), the two agree, and a final cast step identifies the natural-number quotient with its integer image.

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/001011.json, merge commit 49cc5cb37483.

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.

hFeqN have ∀ (m : ℕ), (0 : ℕ) < m → {a : ℕ | a ∈ A ∧ a ∣ m}.ncard = F m
Leaves ∃ (N : ℤ), (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (2 : ℝ) ^ k * (↑N : ℝ), with hFeqN : ∀ (m : ℕ), (0 : ℕ) < m → {a : ℕ | a ∈ A ∧ a ∣ m}.ncard = F m.
Uses library Set.ncard, Set.mem_ofPred_eq.
Lean, lines 25–35
```
  have hFeqN : ∀ m, 0 < m → Set.ncard {a ∈ A | a ∣ m} = F m := by
    intro m hm
    simp only [hF]
    congr 1
    ext a
    simp only [Set.mem_ofPred_eq]
    constructor
    · rintro ⟨h1, h2⟩
      exact ⟨h1, hm, h2⟩
    · rintro ⟨h1, _, h2⟩
      exact ⟨h1, h2⟩
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 25–35 at 49cc5cb37483 ↗
1. hFeqN.s1 case
  Leaves a ∈ A ∧ a ∣ m → a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m.
  Uses library And.intro.
  Lean, lines 32–33
  · rintro ⟨h1, h2⟩ exact ⟨h1, hm, h2⟩
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 32–33 at 49cc5cb37483 ↗
2. hFeqN.s2 case
  Leaves a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m → a ∈ A ∧ a ∣ m.
  Uses library And.intro.
  Lean, lines 34–35
  · rintro ⟨h1, _, h2⟩ exact ⟨h1, h2⟩
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 34–35 at 49cc5cb37483 ↗
hFeq have ∀ (m : ℕ), (0 : ℕ) < m → (↑{a : ℕ | a ∈ A ∧ a ∣ m}.ncard : ℝ) = (↑(F m) : ℝ)
Leaves ∃ (N : ℤ), (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (2 : ℝ) ^ k * (↑N : ℝ), with hFeq : ∀ (m : ℕ), (0 : ℕ) < m → (↑{a : ℕ | a ∈ A ∧ a ∣ m}.ncard : ℝ) = (↑(F m) : ℝ).
Uses library Set.ncard.
Lean, lines 36–38
```
  have hFeq : ∀ m, 0 < m → (Set.ncard {a ∈ A | a ∣ m} : ℝ) = F m := by
    intro m hm
    exact_mod_cast hFeqN m hm
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 36–38 at 49cc5cb37483 ↗
hF_le have ∀ (m : ℕ), F m ≤ m
Leaves ∃ (N : ℤ), (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (2 : ℝ) ^ k * (↑N : ℝ), with hF_le : ∀ (m : ℕ), F m ≤ m.
Uses library Nat.eq_zero_or_pos.
Lean, lines 39–53
```
  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-689ac1ac/Proof.lean, lines 39–53 at 49cc5cb37483 ↗
1. hF_le.s1 case
  Leaves F (0 : ℕ) ≤ (0 : ℕ).
  Lean, lines 42–45
  · have h0 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by ext a simp simp [hF, h0]
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 42–45 at 49cc5cb37483 ↗
  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 42–44
  · have h0 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by ext a simp
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 42–44 at 49cc5cb37483 ↗
2. hF_le.s2 case
  Leaves F m ≤ m, with hm : m > (0 : ℕ).
  Lean, lines 46–53
  · 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-689ac1ac/Proof.lean, lines 46–53 at 49cc5cb37483 ↗
  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, Finset.mem_coe, Nat.mem_divisors, And.intro.
  Lean, lines 46–49
  · 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-689ac1ac/Proof.lean, lines 46–49 at 49cc5cb37483 ↗
  hF_le.s2.s2 calc F m ≤ (↑m.divisors : Set ℕ).ncard
  Closes the goal.
  Uses library Nat.divisors, Set, Set.ncard_le_ncard, Finset.finite_toSet.
  Lean, lines 50–51
  calc F m ≤ (↑(Nat.divisors m) : Set ℕ).ncard := Set.ncard_le_ncard hsub (Finset.finite_toSet _)
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 50–51 at 49cc5cb37483 ↗
  hF_le.s2.s3 calc (↑m.divisors : Set ℕ).ncard = m.divisors.card
  Closes the goal.
  Uses library Nat.divisors, Set.ncard_coe_finset.
  Lean, line 52
  _ = (Nat.divisors m).card := Set.ncard_coe_finset _
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 52 at 49cc5cb37483 ↗
  hF_le.s2.s4 calc m.divisors.card ≤ m
  Closes the goal.
  Uses library Nat.card_divisors_le_self.
  Lean, line 53
  _ ≤ m := Nat.card_divisors_le_self m
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 53 at 49cc5cb37483 ↗
hFs have Summable fun (m : ℕ) => (↑(F m) : ℝ) / (2 : ℝ) ^ m
Leaves ∃ (N : ℤ), (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (2 : ℝ) ^ k * (↑N : ℝ), with hFs : Summable fun (m : ℕ) => (↑(F m) : ℝ) / (2 : ℝ) ^ m.
Uses library Summable, Summable.of_nonneg_of_le, div_eq_mul_inv, one_div, inv_pow, pow_one.
Lean, lines 54–61
```
  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-689ac1ac/Proof.lean, lines 54–61 at 49cc5cb37483 ↗
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 55–56
  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-689ac1ac/Proof.lean, lines 55–56 at 49cc5cb37483 ↗
2. hFs.s2 have (↑(F i) : ℝ) ≤ (↑i : ℝ)
  Leaves (↑(F i) : ℝ) / (2 : ℝ) ^ i ≤ (↑i : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ i, with this : (↑(F i) : ℝ) ≤ (↑i : ℝ).
  Lean, line 58
  have : (F i : ℝ) ≤ i := by exact_mod_cast hF_le i
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 58 at 49cc5cb37483 ↗
3. hFs.s3 have (0 : ℝ) ≤ ((2 : ℝ) ^ i)⁻¹ routine: positivity
  Leaves (↑(F i) : ℝ) * ((2 : ℝ) ^ i)⁻¹ ≤ (↑i : ℝ) * ((2 : ℝ) ^ i)⁻¹, with this : (0 : ℝ) ≤ ((2 : ℝ) ^ i)⁻¹.
  Lean, line 60
  have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 60 at 49cc5cb37483 ↗
hTsum have ∀ (j : ℕ), Summable fun (i : ℕ) => (↑(F (j + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ))
Leaves ∃ (N : ℤ), (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (2 : ℝ) ^ k * (↑N : ℝ), with hTsum : ∀ (j : ℕ), Summable fun (i : ℕ) => (↑(F (j + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)).
Uses library Summable.
Lean, lines 63–69
```
  have hTsum : ∀ j, Summable (fun i : ℕ => (F (j + i + 1) : ℝ) / 2 ^ (i + 1)) := by
    intro j
    have h := ((summable_nat_add_iff (j + 1)).mpr hFs).mul_left ((2:ℝ) ^ j)
    refine h.congr (fun 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-689ac1ac/Proof.lean, lines 63–69 at 49cc5cb37483 ↗
1. hTsum.h have Summable fun (i : ℕ) => (2 : ℝ) ^ j * ((↑(F (i + (j + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (j + (1 : ℕ))))
  Leaves Summable fun (i : ℕ) => (↑(F (j + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)), with h : Summable fun (i : ℕ) => (2 : ℝ) ^ j * ((↑(F (i + (j + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (j + (1 : ℕ)))).
  Uses library summable_nat_add_iff.
  Lean, line 65
  have h := ((summable_nat_add_iff (j + 1)).mpr hFs).mul_left ((2:ℝ) ^ j)
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 65 at 49cc5cb37483 ↗
hZ have (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (↑(p * (2 : ℤ) ^ y - (↑q : ℤ) * ∑ m ∈ Finset.range (y + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (y - m)) : ℝ)
Leaves ∃ (N : ℤ), (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (2 : ℝ) ^ k * (↑N : ℝ), with hZ : (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (↑(p * (2 : ℤ) ^ y - (↑q : ℤ) * ∑ m ∈ Finset.range (y + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (y - m)) : ℝ).
Uses statements spec-23b0fff0 Opn.erdos_257_lambert_tail_integral.
Lean, line 71
```
  have hZ := Opn.erdos_257_lambert_tail_integral A p q hq hsum y
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 71 at 49cc5cb37483 ↗
hTy have ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = T y
Leaves ∃ (N : ℤ), (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (2 : ℝ) ^ k * (↑N : ℝ), with hTy : ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = T y.
Uses library Set.ncard, tsum_congr.
Lean, lines 72–76
```
  have hTy : ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ y + i + 1} : ℝ) / 2 ^ (i + 1) = T y := by
    simp only [hT]
    apply tsum_congr
    intro i
    rw [hFeq _ (by omega)]
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 72–76 at 49cc5cb37483 ↗
hTyk have ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = T (y + k)
Leaves ∃ (N : ℤ), (↑q : ℝ) * ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (2 : ℝ) ^ k * (↑N : ℝ), with hTyk : ∑' (i : ℕ), (↑{a : ℕ | a ∈ A ∧ a ∣ y + k + i + (1 : ℕ)}.ncard : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = T (y + k).
Uses library Set.ncard, tsum_congr.
Lean, lines 78–82
```
  have hTyk : ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ y + k + i + 1} : ℝ) / 2 ^ (i + 1) = T (y + k) := by
    simp only [hT]
    apply tsum_congr
    intro i
    rw [hFeq _ (by omega)]
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 78–82 at 49cc5cb37483 ↗
hsplit have T y = ∑ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) + (1 : ℝ) / (2 : ℝ) ^ k * T (y + k)
Leaves ∃ (N : ℤ), (↑q : ℝ) * T (y + k) = (2 : ℝ) ^ k * (↑N : ℝ), with hsplit : T y = ∑ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) + (1 : ℝ) / (2 : ℝ) ^ k * T (y + k).
Uses library Finset.range, tsum_mul_left, tsum_congr.
Lean, lines 85–95
```
  have hsplit : T y = ∑ i ∈ Finset.range k, (F (y + i + 1) : ℝ) / 2 ^ (i + 1)
      + (1 / 2 ^ k) * T (y + k) := by
    simp only [hT]
    rw [← (hTsum y).sum_add_tsum_nat_add k]
    congr 1
    rw [← tsum_mul_left]
    apply tsum_congr
    intro i
    rw [show y + (i + k) + 1 = y + k + i + 1 by ring,
      show (2:ℝ) ^ (i + k + 1) = 2 ^ k * 2 ^ (i + 1) by ring]
    field_simp
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 85–95 at 49cc5cb37483 ↗
hdiv have ∀ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ))) : ℝ) = (2 : ℝ) ^ k * (↑(F (y + i + (1 : ℕ)) / (2 : ℕ) ^ k) : ℝ)
Leaves ∃ (N : ℤ), (↑q : ℝ) * T (y + k) = (2 : ℝ) ^ k * (↑N : ℝ), with hdiv : ∀ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ))) : ℝ) = (2 : ℝ) ^ k * (↑(F (y + i + (1 : ℕ)) / (2 : ℕ) ^ k) : ℝ).
Uses library Finset.range, Nat.mul_div_cancel'.
Lean, lines 97–104
```
  have hdiv : ∀ i ∈ Finset.range k, (F (y + i + 1) : ℝ) = 2 ^ k * ((F (y + i + 1) / 2 ^ k : ℕ) : ℝ) := by
    intro i hi
    have hi' : i < k := Finset.mem_range.mp hi
    have hd : 2 ^ k ∣ F (y + i + 1) := by
      have h := hblock (i + 1) (by omega) (by omega)
      rw [show y + (i + 1) = y + i + 1 by ring, hFeqN _ (by omega)] at h
      exact h
    exact_mod_cast (Nat.mul_div_cancel' hd).symm
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 97–104 at 49cc5cb37483 ↗
1. hdiv.hi' have i < k
  Leaves (↑(F (y + i + (1 : ℕ))) : ℝ) = (2 : ℝ) ^ k * (↑(F (y + i + (1 : ℕ)) / (2 : ℕ) ^ k) : ℝ), with hi' : i < k.
  Uses library Finset.mem_range.
  Lean, line 99
  have hi' : i < k := Finset.mem_range.mp hi
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 99 at 49cc5cb37483 ↗
2. hdiv.hd have (2 : ℕ) ^ k ∣ F (y + i + (1 : ℕ))
  Leaves (↑(F (y + i + (1 : ℕ))) : ℝ) = (2 : ℝ) ^ k * (↑(F (y + i + (1 : ℕ)) / (2 : ℕ) ^ k) : ℝ), with hd : (2 : ℕ) ^ k ∣ F (y + i + (1 : ℕ)).
  Lean, lines 100–103
  have hd : 2 ^ k ∣ F (y + i + 1) := by have h := hblock (i + 1) (by omega) (by omega) rw [show y + (i + 1) = y + i + 1 by ring, hFeqN _ (by omega)] at h exact h
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 100–103 at 49cc5cb37483 ↗
  hdiv.hd.h have (2 : ℕ) ^ k ∣ {a : ℕ | a ∈ A ∧ a ∣ y + (i + (1 : ℕ))}.ncard
  Leaves (2 : ℕ) ^ k ∣ F (y + i + (1 : ℕ)), with h : (2 : ℕ) ^ k ∣ {a : ℕ | a ∈ A ∧ a ∣ y + (i + (1 : ℕ))}.ncard.
  Lean, line 101
  have h := hblock (i + 1) (by omega) (by omega)
  targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 101 at 49cc5cb37483 ↗
h2k have (2 : ℝ) ^ k ≠ (0 : ℝ) routine: positivity
Leaves (↑q : ℝ) * T (y + k) = (2 : ℝ) ^ k * (↑(p * (2 : ℤ) ^ y - (↑q : ℤ) * ∑ m ∈ Finset.range (y + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (y - m) - (↑q : ℤ) * ∑ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ)) / (2 : ℕ) ^ k) : ℤ) * (2 : ℤ) ^ (k - (i + (1 : ℕ)))) : ℝ), with h2k : (2 : ℝ) ^ k ≠ (0 : ℝ).
Lean, line 107
```
  have h2k : (2:ℝ) ^ k ≠ 0 := by positivity
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 107 at 49cc5cb37483 ↗
key have (↑q : ℝ) * T (y + k) = (2 : ℝ) ^ k * ((↑q : ℝ) * T y - (↑q : ℝ) * ∑ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)))
Leaves (↑q : ℝ) * T (y + k) = (2 : ℝ) ^ k * (↑(p * (2 : ℤ) ^ y - (↑q : ℤ) * ∑ m ∈ Finset.range (y + (1 : ℕ)), (↑{a : ℕ | a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m}.ncard : ℤ) * (2 : ℤ) ^ (y - m) - (↑q : ℤ) * ∑ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ)) / (2 : ℕ) ^ k) : ℤ) * (2 : ℤ) ^ (k - (i + (1 : ℕ)))) : ℝ), with key : (↑q : ℝ) * T (y + k) = (2 : ℝ) ^ k * ((↑q : ℝ) * T y - (↑q : ℝ) * ∑ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ))).
Uses library Finset.range.
Lean, lines 108–112
```
  have key : (q : ℝ) * T (y + k) =
      2 ^ k * ((q : ℝ) * T y - q * ∑ i ∈ Finset.range k, (F (y + i + 1) : ℝ) / 2 ^ (i + 1)) := by
    rw [hsplit]
    field_simp
    ring
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, lines 108–112 at 49cc5cb37483 ↗
hi' have i + (1 : ℕ) ≤ k
Leaves (↑q : ℝ) * ((↑(F (y + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ))) = (↑q : ℝ) * ((↑((↑(F (y + i + (1 : ℕ))) : ℤ) / (2 : ℤ) ^ k) : ℝ) * (2 : ℝ) ^ (k - (i + (1 : ℕ)))), with hi' : i + (1 : ℕ) ≤ k.
Uses library Finset.mem_range.
Lean, line 120
```
  have hi' : i + 1 ≤ k := Finset.mem_range.mp hi
```
targets/erdos-257/nodes/spec-689ac1ac/Proof.lean, line 120 at 49cc5cb37483 ↗

The proof in Lean (Proof.lean)

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

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-689ac1ac/Proof.lean, sha256 1cd661217631.

import Mathlib
import Nodes.«spec-689ac1ac».Context

/-- The divisible-block step of the Chowla–Erdős method for Erdős 257. Write
`f_A(m) = #{a ∈ A : a ∣ m}` for the binary coefficients of `∑_{a ∈ A} 1/(2^a - 1)`
(`Opn.erdos_257_lambert_identity`) and `T_j = ∑_{i ≥ 1} f_A(j+i)/2^i` for the tail after
position `j`. Suppose the sum is the rational `p/q`. If the `k` coefficients after position `y`,
`f_A(y+1), …, f_A(y+k)`, are all divisible by `2^k` (a block of zeros is the case they all
vanish), then `q · T_{y+k}` is an integer multiple of `2^k`. Since `q · T_y` is an integer
(`Opn.erdos_257_lambert_tail_integral`) and `T_y = ∑_{i=1}^k f_A(y+i)/2^i + 2^{-k} T_{y+k}`,
the divisibility makes the finite part an integer too. For infinite `A` the tail `T_{y+k}` is
positive, so the multiple is at least `1` and `q · T_{y+k} ≥ 2^k`: this is the inequality every
Chinese-remainder proof (Erdős 1948 with `f_ℕ = d`, Duverney–Tachiya 2019) contradicts by
choosing `y` so that the tail after the block is small on average. -/
theorem Opn.erdos_257_divisible_block :
    ∀ (A : Set ℕ) (p : ℤ) (q : ℕ), 0 < q →
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = p / q →
    ∀ y k : ℕ, (∀ i, 1 ≤ i → i ≤ k → 2 ^ k ∣ Set.ncard {a ∈ A | a ∣ y + i}) →
      ∃ N : ℤ,
        (q : ℝ) * ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ y + k + i + 1} : ℝ) / 2 ^ (i + 1) =
          2 ^ k * N := by
  intro A p q hq hsum y k hblock
  classical
  set F : ℕ → ℕ := fun m => Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} with hF
  have hFeqN : ∀ m, 0 < m → Set.ncard {a ∈ A | a ∣ m} = F m := by
    intro m hm
    simp only [hF]
    congr 1
    ext a
    simp only [Set.mem_ofPred_eq]
    constructor
    · rintro ⟨h1, h2⟩
      exact ⟨h1, hm, h2⟩
    · rintro ⟨h1, _, h2⟩
      exact ⟨h1, h2⟩
  have hFeq : ∀ m, 0 < m → (Set.ncard {a ∈ A | a ∣ m} : ℝ) = F m := by
    intro m hm
    exact_mod_cast hFeqN m hm
  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
  set T : ℕ → ℝ := fun j => ∑' i : ℕ, (F (j + i + 1) : ℝ) / 2 ^ (i + 1) with hT
  have hTsum : ∀ j, Summable (fun i : ℕ => (F (j + i + 1) : ℝ) / 2 ^ (i + 1)) := by
    intro j
    have h := ((summable_nat_add_iff (j + 1)).mpr hFs).mul_left ((2:ℝ) ^ j)
    refine h.congr (fun 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
  -- the tail lemma at `y`, with its tail written as `T y`
  have hZ := Opn.erdos_257_lambert_tail_integral A p q hq hsum y
  have hTy : ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ y + i + 1} : ℝ) / 2 ^ (i + 1) = T y := by
    simp only [hT]
    apply tsum_congr
    intro i
    rw [hFeq _ (by omega)]
  rw [hTy] at hZ
  have hTyk : ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ y + k + i + 1} : ℝ) / 2 ^ (i + 1) = T (y + k) := by
    simp only [hT]
    apply tsum_congr
    intro i
    rw [hFeq _ (by omega)]
  rw [hTyk]
  -- `T y` splits at `k`
  have hsplit : T y = ∑ i ∈ Finset.range k, (F (y + i + 1) : ℝ) / 2 ^ (i + 1)
      + (1 / 2 ^ k) * T (y + k) := by
    simp only [hT]
    rw [← (hTsum y).sum_add_tsum_nat_add k]
    congr 1
    rw [← tsum_mul_left]
    apply tsum_congr
    intro i
    rw [show y + (i + k) + 1 = y + k + i + 1 by ring,
      show (2:ℝ) ^ (i + k + 1) = 2 ^ k * 2 ^ (i + 1) by ring]
    field_simp
  -- each block coefficient is `2^k` times a natural number
  have hdiv : ∀ i ∈ Finset.range k, (F (y + i + 1) : ℝ) = 2 ^ k * ((F (y + i + 1) / 2 ^ k : ℕ) : ℝ) := by
    intro i hi
    have hi' : i < k := Finset.mem_range.mp hi
    have hd : 2 ^ k ∣ F (y + i + 1) := by
      have h := hblock (i + 1) (by omega) (by omega)
      rw [show y + (i + 1) = y + i + 1 by ring, hFeqN _ (by omega)] at h
      exact h
    exact_mod_cast (Nat.mul_div_cancel' hd).symm
  refine ⟨(p * 2 ^ y - q * ∑ m ∈ Finset.range (y + 1), (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℤ) * 2 ^ (y - m))
      - q * ∑ i ∈ Finset.range k, ((F (y + i + 1) / 2 ^ k : ℕ) : ℤ) * 2 ^ (k - (i + 1)), ?_⟩
  have h2k : (2:ℝ) ^ k ≠ 0 := by positivity
  have key : (q : ℝ) * T (y + k) =
      2 ^ k * ((q : ℝ) * T y - q * ∑ i ∈ Finset.range k, (F (y + i + 1) : ℝ) / 2 ^ (i + 1)) := by
    rw [hsplit]
    field_simp
    ring
  rw [key, hZ]
  push_cast
  congr 1
  simp only [Finset.mul_sum]
  congr 1
  apply Finset.sum_congr rfl
  intro i hi
  have hi' : i + 1 ≤ k := Finset.mem_range.mp hi
  rw [hdiv i hi, pow_sub₀ _ (by norm_num) hi']
  field_simp
  norm_cast

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-689ac1ac».Context

/-- The divisible-block step of the Chowla–Erdős method for Erdős 257. Write
`f_A(m) = #{a ∈ A : a ∣ m}` for the binary coefficients of `∑_{a ∈ A} 1/(2^a - 1)`
(`Opn.erdos_257_lambert_identity`) and `T_j = ∑_{i ≥ 1} f_A(j+i)/2^i` for the tail after
position `j`. Suppose the sum is the rational `p/q`. If the `k` coefficients after position `y`,
`f_A(y+1), …, f_A(y+k)`, are all divisible by `2^k` (a block of zeros is the case they all
vanish), then `q · T_{y+k}` is an integer multiple of `2^k`. Since `q · T_y` is an integer
(`Opn.erdos_257_lambert_tail_integral`) and `T_y = ∑_{i=1}^k f_A(y+i)/2^i + 2^{-k} T_{y+k}`,
the divisibility makes the finite part an integer too. For infinite `A` the tail `T_{y+k}` is
positive, so the multiple is at least `1` and `q · T_{y+k} ≥ 2^k`: this is the inequality every
Chinese-remainder proof (Erdős 1948 with `f_ℕ = d`, Duverney–Tachiya 2019) contradicts by
choosing `y` so that the tail after the block is small on average. -/
theorem Opn.erdos_257_divisible_block :
    ∀ (A : Set ℕ) (p : ℤ) (q : ℕ), 0 < q →
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = p / q →
    ∀ y k : ℕ, (∀ i, 1 ≤ i → i ≤ k → 2 ^ k ∣ Set.ncard {a ∈ A | a ∣ y + i}) →
      ∃ N : ℤ,
        (q : ℝ) * ∑' i : ℕ, (Set.ncard {a ∈ A | a ∣ y + k + i + 1} : ℝ) / 2 ^ (i + 1) =
          2 ^ k * N := by
  sorry

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

Rendered from gloss/4b0db1307f30….md · Improve these words →

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

Depends on (1), each in words

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

spec-23b0fff0 Opn.erdos_257_lambert_tail_integral: $\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},$ · used by the proof

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/001011.json, merge commit 49cc5cb37483.

Verdict pass, from attestations/001011.json.

Submitter: t1026-c
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (intermediate)

Step	Check	Result
1	toolchain	pass
2	paths	pass
4	kernel-replay	pass
5	axioms	pass
6	hazards	pass
7	witness	pass
8	deps	pass

Witness

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

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/spec-689ac1ac/Witness.lean, sha256 a9aa5e410e9b.

import Nodes.«spec-689ac1ac».Context

theorem witness : ∃ (A : Set ℕ) (p : ℤ) (q : ℕ) (y : ℕ) (k : ℕ),
  (0 : ℕ) < q ∧
    ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ) ∧
      ∀ (i : ℕ), (1 : ℕ) ≤ i → i ≤ k → (2 : ℕ) ^ k ∣ {a : ℕ | a ∈ A ∧ a ∣ y + i}.ncard :=
  ⟨∅, 0, 1, 0, 0, one_pos, by rw [tsum_empty]; simp, fun i h1 h2 => absurd (h1.trans h2) (by norm_num)⟩

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

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.

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

Untrusted: acknowledgment of a div-zero finding at ↑{a | a ∈ A ∧ a ∣ y + k + 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 off-by-one-range finding at 1 ≤ i

The block is the k coefficients at positions y+1, …, y+k inclusive: i runs from 1 to k, and i = 0 (position y itself) is deliberately outside it.

How to read this page

How to read a statement’s page →

Explainer

Overview

The coefficients, with and without the guard

The tails

Splitting $T_y$ at the block

The block coefficients are multiples of $2^k$

Assembling the integer

Overview

The coefficients, with and without the guard (hFeqN hFeq hF_le hFs)

The tails (hTsum hZ hTy hTyk)

Splitting $T_y$ at the block (hsplit)

The block coefficients are multiples of $2^k$ (hdiv)

Assembling the integer (h2k key hi')

How it was proved

What is known

Work on it

Record