weighted block divisible by 2^k ⇒ q·T a multiple of 2^k

spec-ced1e7c5 Opn.erdos_257_block_divisibility

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 \,\Big|\, \sum_{i=1}^{k} f_A(y+i)\,2^{\,k-i}\ \ \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 weighted sum of the $k$ coefficients just after position $y$ (the coefficient at $y+i$ weighted by $2^{k-i}$) is divisible by $2^k$, then $q$ times the tail after the block is an integer multiple of $2^k$. The block sum is Lean's Finset.sum over Finset.range k, written with $i$ from $0$ to $k-1$ for the position $y+i+1$ and the weight 2 ^ (k - (i + 1)), a natural-number power whose subtraction is exact since $i < k$; with $k = 0$ the sum 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. When every $f_A(y+i)$ is itself divisible by $2^k$ the hypothesis holds; that case is the node spec-689ac1ac.

unverified · history

Lean

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

Draft · drafted, by the model named above

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 B$ for the weighted block sum $B = \sum_{i<k} F(y+i+1)\,2^{k-(i+1)}$, the proof produces an integer $N$ with $q\,T_{y+k} = 2^k N$. It is the proof of spec-689ac1ac with one change in the last step. The dependency Opn.erdos_257_lambert_tail_integral (in scope through this node's Context) says $q\,T_y$ is the explicit integer $Z = p\,2^y - q\sum_{m \le y} F(m) 2^{y-m}$ (hZ), after the statement's unguarded coefficients $\#\{a \in A : a \mid m\}$, $m \ge 1$, are identified with $F(m)$ (hFeqN, hFeq) and the two tails in play with $T_y$ and $T_{y+k}$ (hTy, hTyk). $F(m) \le m$ makes $F(m)/2^m$ summable (hF_le, hFs), hence every tail is a summable series (hTsum), and $T_y$ splits into its first $k$ terms plus $2^{-k}\,T_{y+k}$ (hsplit). The first $k$ terms are exactly $B/2^k$: the statement's block sum equals $B$ written with $F$ (hBeq), and $\sum_{i<k} F(y+i+1)/2^{i+1} = B / 2^k$ because $2^{k-(i+1)} = 2^k/2^{i+1}$ for $i < k$ (hsumR). The divisibility hypothesis gives $B = 2^k c$ for a natural number $c$ (hBdiv). From the splitting, $q\,T_{y+k} = 2^k\,(q\,T_y - q \cdot B/2^k)$ (key), and substituting $q\,T_y = Z$ and $B = 2^k c$ gives $q\,T_{y+k} = 2^k\,(Z - q\,c)$, so $N = Z - q\,c$ closes the theorem after the casts are pushed through.

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/04bc630b0a96….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 B$ for the weighted block sum $B = \sum_{i<k} F(y+i+1)\,2^{k-(i+1)}$, the proof produces an integer $N$ with $q\,T_{y+k} = 2^k N$. It is the proof of spec-689ac1ac with one change in the last step. The dependency Opn.erdos_257_lambert_tail_integral (in scope through this node's Context) says $q\,T_y$ is the explicit integer $Z = p\,2^y - q\sum_{m \le y} F(m) 2^{y-m}$ (hZ), after the statement's unguarded coefficients $\#\{a \in A : a \mid m\}$, $m \ge 1$, are identified with $F(m)$ (hFeqN, hFeq) and the two tails in play with $T_y$ and $T_{y+k}$ (hTy, hTyk). $F(m) \le m$ makes $F(m)/2^m$ summable (hF_le, hFs), hence every tail is a summable series (hTsum), and $T_y$ splits into its first $k$ terms plus $2^{-k}\,T_{y+k}$ (hsplit). The first $k$ terms are exactly $B/2^k$: the statement's block sum equals $B$ written with $F$ (hBeq), and $\sum_{i<k} F(y+i+1)/2^{i+1} = B / 2^k$ because $2^{k-(i+1)} = 2^k/2^{i+1}$ for $i < k$ (hsumR). The divisibility hypothesis gives $B = 2^k c$ for a natural number $c$ (hBdiv). From the splitting, $q\,T_{y+k} = 2^k\,(q\,T_y - q \cdot B/2^k)$ (key), and substituting $q\,T_y = Z$ and $B = 2^k c$ gives $q\,T_{y+k} = 2^k\,(Z - q\,c)$, so $N = Z - q\,c$ closes the theorem after the casts are pushed through.

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/001016.json, merge commit 87abc6042ebe.

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 29–39
```
  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-ced1e7c5/Proof.lean, lines 29–39 at 87abc6042ebe ↗
1. hFeqN.s1 case
  Leaves a ∈ A ∧ a ∣ m → a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m.
  Uses library And.intro.
  Lean, lines 36–37
  · rintro ⟨h1, h2⟩ exact ⟨h1, hm, h2⟩
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, lines 36–37 at 87abc6042ebe ↗
2. hFeqN.s2 case
  Leaves a ∈ A ∧ (0 : ℕ) < m ∧ a ∣ m → a ∈ A ∧ a ∣ m.
  Uses library And.intro.
  Lean, lines 38–39
  · rintro ⟨h1, _, h2⟩ exact ⟨h1, h2⟩
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, lines 38–39 at 87abc6042ebe ↗
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 40–42
```
  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-ced1e7c5/Proof.lean, lines 40–42 at 87abc6042ebe ↗
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 43–57
```
  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-ced1e7c5/Proof.lean, lines 43–57 at 87abc6042ebe ↗
1. hF_le.s1 case
  Leaves F (0 : ℕ) ≤ (0 : ℕ).
  Lean, lines 46–49
  · have h0 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by ext a simp simp [hF, h0]
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, lines 46–49 at 87abc6042ebe ↗
  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 46–48
  · have h0 : {a ∈ A | 0 < 0 ∧ a ∣ 0} = ∅ := by ext a simp
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, lines 46–48 at 87abc6042ebe ↗
2. hF_le.s2 case
  Leaves F m ≤ m, with hm : m > (0 : ℕ).
  Lean, lines 50–57
  · 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-ced1e7c5/Proof.lean, lines 50–57 at 87abc6042ebe ↗
  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 50–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'⟩
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, lines 50–53 at 87abc6042ebe ↗
  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 54–55
  calc F m ≤ (↑(Nat.divisors m) : Set ℕ).ncard := Set.ncard_le_ncard hsub (Finset.finite_toSet _)
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, lines 54–55 at 87abc6042ebe ↗
  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 56
  _ = (Nat.divisors m).card := Set.ncard_coe_finset _
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 56 at 87abc6042ebe ↗
  hF_le.s2.s4 calc m.divisors.card ≤ m
  Closes the goal.
  Uses library Nat.card_divisors_le_self.
  Lean, line 57
  _ ≤ m := Nat.card_divisors_le_self m
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 57 at 87abc6042ebe ↗
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 58–65
```
  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-ced1e7c5/Proof.lean, lines 58–65 at 87abc6042ebe ↗
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 59–60
  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-ced1e7c5/Proof.lean, lines 59–60 at 87abc6042ebe ↗
2. hFs.s2 have (↑(F i) : ℝ) ≤ (↑i : ℝ)
  Leaves (↑(F i) : ℝ) / (2 : ℝ) ^ i ≤ (↑i : ℝ) ^ (1 : ℕ) * (1 / 2 : ℝ) ^ i, with this : (↑(F i) : ℝ) ≤ (↑i : ℝ).
  Lean, line 62
  have : (F i : ℝ) ≤ i := by exact_mod_cast hF_le i
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 62 at 87abc6042ebe ↗
3. hFs.s3 have (0 : ℝ) ≤ ((2 : ℝ) ^ i)⁻¹ routine: positivity
  Leaves (↑(F i) : ℝ) * ((2 : ℝ) ^ i)⁻¹ ≤ (↑i : ℝ) * ((2 : ℝ) ^ i)⁻¹, with this : (0 : ℝ) ≤ ((2 : ℝ) ^ i)⁻¹.
  Lean, line 64
  have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 64 at 87abc6042ebe ↗
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 67–73
```
  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-ced1e7c5/Proof.lean, lines 67–73 at 87abc6042ebe ↗
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 69
  have h := ((summable_nat_add_iff (j + 1)).mpr hFs).mul_left ((2:ℝ) ^ j)
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 69 at 87abc6042ebe ↗
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 75
```
  have hZ := Opn.erdos_257_lambert_tail_integral A p q hq hsum y
```
targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 75 at 87abc6042ebe ↗
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 76–80
```
  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-ced1e7c5/Proof.lean, lines 76–80 at 87abc6042ebe ↗
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 82–86
```
  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-ced1e7c5/Proof.lean, lines 82–86 at 87abc6042ebe ↗
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 89–99
```
  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-ced1e7c5/Proof.lean, lines 89–99 at 87abc6042ebe ↗
hBeq have ∑ i ∈ Finset.range k, {a : ℕ | a ∈ A ∧ a ∣ y + i + (1 : ℕ)}.ncard * (2 : ℕ) ^ (k - (i + (1 : ℕ))) = Bsum
Leaves ∃ (N : ℤ), (↑q : ℝ) * T (y + k) = (2 : ℝ) ^ k * (↑N : ℝ), with hBeq : ∑ i ∈ Finset.range k, {a : ℕ | a ∈ A ∧ a ∣ y + i + (1 : ℕ)}.ncard * (2 : ℕ) ^ (k - (i + (1 : ℕ))) = Bsum.
Uses library Finset.range, Set.ncard, Finset.sum_congr, rfl.
Lean, lines 102–106
```
  have hBeq : ∑ i ∈ Finset.range k, Set.ncard {a ∈ A | a ∣ y + i + 1} * 2 ^ (k - (i + 1)) = Bsum := by
    simp only [hBsum]
    apply Finset.sum_congr rfl
    intro i hi
    rw [hFeqN _ (by omega)]
```
targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, lines 102–106 at 87abc6042ebe ↗
hsumR have ∑ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (↑Bsum : ℝ) / (2 : ℝ) ^ k
Leaves ∃ (N : ℤ), (↑q : ℝ) * T (y + k) = (2 : ℝ) ^ k * (↑N : ℝ), with hsumR : ∑ i ∈ Finset.range k, (↑(F (y + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (↑Bsum : ℝ) / (2 : ℝ) ^ k.
Uses library Finset.range, Finset.sum_div, Finset.sum_congr, rfl, pow_sub₀.
Lean, lines 108–116
```
  have hsumR : ∑ i ∈ Finset.range k, (F (y + i + 1) : ℝ) / 2 ^ (i + 1) = (Bsum : ℝ) / 2 ^ k := by
    simp only [hBsum]
    push_cast
    rw [Finset.sum_div]
    apply Finset.sum_congr rfl
    intro i hi
    have hi' : i + 1 ≤ k := Finset.mem_range.mp hi
    rw [pow_sub₀ _ (by norm_num) hi']
    field_simp
```
targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, lines 108–116 at 87abc6042ebe ↗
1. hsumR.hi' have i + (1 : ℕ) ≤ k
  Leaves (↑(F (y + i + (1 : ℕ))) : ℝ) / (2 : ℝ) ^ (i + (1 : ℕ)) = (↑(F (y + i + (1 : ℕ))) : ℝ) * (2 : ℝ) ^ (k - (i + (1 : ℕ))) / (2 : ℝ) ^ k, with hi' : i + (1 : ℕ) ≤ k.
  Uses library Finset.mem_range.
  Lean, line 114
  have hi' : i + 1 ≤ k := Finset.mem_range.mp hi
  targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 114 at 87abc6042ebe ↗
s12 obtain (2 : ℕ) ^ k ∣ Bsum
Leaves ∃ (N : ℤ), (↑q : ℝ) * T (y + k) = (2 : ℝ) ^ k * (↑N : ℝ), with c : ℕ, hc : Bsum = (2 : ℕ) ^ k * c.
Lean, line 117
```
  obtain ⟨c, hc⟩ := hblock
```
targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 117 at 87abc6042ebe ↗
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 : ℤ) * (↑c : ℤ)) : ℝ), with h2k : (2 : ℝ) ^ k ≠ (0 : ℝ).
Lean, line 120
```
  have h2k : (2:ℝ) ^ k ≠ 0 := by positivity
```
targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 120 at 87abc6042ebe ↗
hBdiv have (↑Bsum : ℝ) = (2 : ℝ) ^ k * (↑c : ℝ)
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 : ℤ) * (↑c : ℤ)) : ℝ), with hBdiv : (↑Bsum : ℝ) = (2 : ℝ) ^ k * (↑c : ℝ).
Lean, line 121
```
  have hBdiv : (Bsum : ℝ) = 2 ^ k * (c : ℝ) := by exact_mod_cast hc
```
targets/erdos-257/nodes/spec-ced1e7c5/Proof.lean, line 121 at 87abc6042ebe ↗
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 : ℤ) * (↑c : ℤ)) : ℝ), 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 122–126
```
  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-ced1e7c5/Proof.lean, lines 122–126 at 87abc6042ebe ↗

The proof in Lean (Proof.lean)

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

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-ced1e7c5/Proof.lean, sha256 08f6777a353b.

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

/-- The 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 weighted block sum `∑_{i=1}^{k} f_A(y+i) 2^(k-i)` of the `k` coefficients after
position `y` is divisible by `2^k` (as it is when every `f_A(y+i)` is divisible by `2^k`, or
when 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 the Chinese-remainder proofs contradict, Erdős 1948 (`f_ℕ = d`, each coefficient
divisible by `2^k`) and Erdős 1968 (pairwise coprime `A`: extra elements dividing `y+k` are
added until the block sum is divisible) by choosing `y` so that the tail after the block is
small on average. In Lean `2^(k-(i+1))` is a natural-number power with `i < k`, so the
subtraction is exact. -/
theorem Opn.erdos_257_block_divisibility :
    ∀ (A : Set ℕ) (p : ℤ) (q : ℕ), 0 < q →
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = p / q →
    ∀ y k : ℕ,
      2 ^ k ∣ ∑ i ∈ Finset.range k, Set.ncard {a ∈ A | a ∣ y + i + 1} * 2 ^ (k - (i + 1)) →
      ∃ 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
  -- the weighted block sum is `2^k` times a natural number
  set Bsum : ℕ := ∑ i ∈ Finset.range k, F (y + i + 1) * 2 ^ (k - (i + 1)) with hBsum
  have hBeq : ∑ i ∈ Finset.range k, Set.ncard {a ∈ A | a ∣ y + i + 1} * 2 ^ (k - (i + 1)) = Bsum := by
    simp only [hBsum]
    apply Finset.sum_congr rfl
    intro i hi
    rw [hFeqN _ (by omega)]
  rw [hBeq] at hblock
  have hsumR : ∑ i ∈ Finset.range k, (F (y + i + 1) : ℝ) / 2 ^ (i + 1) = (Bsum : ℝ) / 2 ^ k := by
    simp only [hBsum]
    push_cast
    rw [Finset.sum_div]
    apply Finset.sum_congr rfl
    intro i hi
    have hi' : i + 1 ≤ k := Finset.mem_range.mp hi
    rw [pow_sub₀ _ (by norm_num) hi']
    field_simp
  obtain ⟨c, hc⟩ := hblock
  refine ⟨(p * 2 ^ y - q * ∑ m ∈ Finset.range (y + 1), (Set.ncard {a ∈ A | 0 < m ∧ a ∣ m} : ℤ) * 2 ^ (y - m))
      - q * (c : ℤ), ?_⟩
  have h2k : (2:ℝ) ^ k ≠ 0 := by positivity
  have hBdiv : (Bsum : ℝ) = 2 ^ k * (c : ℝ) := by exact_mod_cast hc
  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, hsumR, hBdiv]
  push_cast
  field_simp

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-ced1e7c5».Context

/-- The 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 weighted block sum `∑_{i=1}^{k} f_A(y+i) 2^(k-i)` of the `k` coefficients after
position `y` is divisible by `2^k` (as it is when every `f_A(y+i)` is divisible by `2^k`, or
when 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 the Chinese-remainder proofs contradict, Erdős 1948 (`f_ℕ = d`, each coefficient
divisible by `2^k`) and Erdős 1968 (pairwise coprime `A`: extra elements dividing `y+k` are
added until the block sum is divisible) by choosing `y` so that the tail after the block is
small on average. In Lean `2^(k-(i+1))` is a natural-number power with `i < k`, so the
subtraction is exact. -/
theorem Opn.erdos_257_block_divisibility :
    ∀ (A : Set ℕ) (p : ℤ) (q : ℕ), 0 < q →
    ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = p / q →
    ∀ y k : ℕ,
      2 ^ k ∣ ∑ i ∈ Finset.range k, Set.ncard {a ∈ A | a ∣ y + i + 1} * 2 ^ (k - (i + 1)) →
      ∃ 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/bf765b013616….md · Improve these words →

Rendered from targets/erdos-257/nodes/spec-ced1e7c5/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/001016.json, merge commit 87abc6042ebe.

Verdict pass, from attestations/001016.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/001016.json, merge commit 87abc6042ebe.

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

import Nodes.«spec-ced1e7c5».Context

theorem witness : ∃ (A : Set ℕ) (p : ℤ) (q : ℕ) (y : ℕ) (k : ℕ),
  (0 : ℕ) < q ∧
    ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ) ∧
      (2 : ℕ) ^ k ∣ ∑ i ∈ Finset.range k, {a : ℕ | a ∈ A ∧ a ∣ y + i + (1 : ℕ)}.ncard * (2 : ℕ) ^ (k - (i + (1 : ℕ))) :=
  ⟨∅, 0, 1, 0, 0, one_pos, by rw [tsum_empty]; simp, by 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 (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 nat-sub finding at k - (i + 1)

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

How to read this page

How to read a statement’s page →