Rational binary series has eventually periodic tails mod 1

spec-c390279b Opn.erdos_69_rational_tails_periodic

proved

Proposed by a contributor.

$\displaystyle \exists p>0,\ N_0\ \ \forall n,n'\ge N_0,\ n\equiv n' \pmod p\ \ \exists z\in\mathbb{Z}:\quad \sum_{j=0}^{\infty}\frac{f(n+1+j)}{2^{j+1}} - \sum_{j=0}^{\infty}\frac{f(n'+1+j)}{2^{j+1}} = z$

For every f : ℕ → ℕ and rational q, if the family f(n)/2^n is summable in ℝ and q equals its sum ∑_{n≥0} f(n)/2^n, then there are a positive natural p and a natural N₀ such that any two tails taken from n, n' ≥ N₀ with n ≡ n' (mod p) differ by an integer. The tails are tsums over ℝ (0 when not summable); the hypotheses are the "if" part and the display is the conclusion.

unverified · history

Lean

theorem Opn.erdos_69_rational_tails_periodic :
    ∀ (f : ℕ → ℕ) (q : ℚ), Summable (fun n : ℕ => (f n : ℝ) / 2 ^ n) →
      (q : ℝ) = ∑' n : ℕ, (f n : ℝ) / 2 ^ n →
      ∃ p N₀ : ℕ, 0 < p ∧ ∀ n n' : ℕ, N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] →
        ∃ z : ℤ, ∑' j : ℕ, (f (n + 1 + j) : ℝ) / 2 ^ (j + 1)
          - ∑' j : ℕ, (f (n' + 1 + j) : ℝ) / 2 ^ (j + 1) = z := 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 →

How it was proved

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000306.json, merge commit 7965601f1a79.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 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.

htail have ∀ (n : ℕ), ∑' (j : ℕ), (↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (2 : ℝ) ^ n * ∑' (m : ℕ), (↑(f m) : ℝ) / (2 : ℝ) ^ m - (↑(∑ i ∈ Finset.range (n + (1 : ℕ)), f i * (2 : ℕ) ^ (n - i)) : ℝ)
Leaves ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), ∑' (j : ℕ), (↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) - ∑' (j : ℕ), (↑(f (n' + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (↑z : ℝ), with htail : ∀ (n : ℕ), ∑' (j : ℕ), (↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (2 : ℝ) ^ n * ∑' (m : ℕ), (↑(f m) : ℝ) / (2 : ℝ) ^ m - (↑(∑ i ∈ Finset.range (n + (1 : ℕ)), f i * (2 : ℕ) ^ (n - i)) : ℝ).
Uses library Finset.range, tsum_congr, tsum_mul_left, mul_add, mul_assoc, mul_one_div_cancel, one_mul.
Lean, lines 25–47
```
  have htail : ∀ n : ℕ, ∑' j : ℕ, (f (n + 1 + j) : ℝ) / 2 ^ (j + 1)
      = 2 ^ n * ∑' m : ℕ, (f m : ℝ) / 2 ^ m
        - ((∑ i ∈ Finset.range (n + 1), f i * 2 ^ (n - i) : ℕ) : ℝ) := by
    intro n
    have h1 := Summable.sum_add_tsum_nat_add (n + 1) hs
    have h2 : ∀ j : ℕ, (f (j + (n + 1)) : ℝ) / 2 ^ (j + (n + 1))
        = (1 / 2 ^ n) * ((f (n + 1 + j) : ℝ) / 2 ^ (j + 1)) := by
      intro j
      rw [show j + (n + 1) = n + 1 + j by omega, show n + 1 + j = n + (j + 1) by omega, pow_add]
      field_simp
    rw [tsum_congr h2, tsum_mul_left] at h1
    have h3 : (2 : ℝ) ^ n * ∑ i ∈ Finset.range (n + 1), (f i : ℝ) / 2 ^ i
        = ((∑ i ∈ Finset.range (n + 1), f i * 2 ^ (n - i) : ℕ) : ℝ) := by
      push_cast
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl (fun i hi => ?_)
      have hi' : i ≤ n := Nat.lt_succ_iff.1 (Finset.mem_range.1 hi)
      have : (2 : ℝ) ^ n = 2 ^ (n - i) * 2 ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [this]
      field_simp
    rw [← h1, mul_add, h3, ← mul_assoc, mul_one_div_cancel (by positivity), one_mul]
    ring
```
targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 25–47 at 7965601f1a79 ↗
1. htail.h1 have ∑ i ∈ Finset.range (n + (1 : ℕ)), (↑(f i) : ℝ) / (2 : ℝ) ^ i + ∑' (i : ℕ), (↑(f (i + (n + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (n + (1 : ℕ))) = ∑' (i : ℕ), (↑(f i) : ℝ) / (2 : ℝ) ^ i
  Leaves ∑' (j : ℕ), (↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (2 : ℝ) ^ n * ∑' (m : ℕ), (↑(f m) : ℝ) / (2 : ℝ) ^ m - (↑(∑ i ∈ Finset.range (n + (1 : ℕ)), f i * (2 : ℕ) ^ (n - i)) : ℝ), with h1 : ∑ i ∈ Finset.range (n + (1 : ℕ)), (↑(f i) : ℝ) / (2 : ℝ) ^ i + ∑' (i : ℕ), (↑(f (i + (n + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (i + (n + (1 : ℕ))) = ∑' (i : ℕ), (↑(f i) : ℝ) / (2 : ℝ) ^ i.
  Uses library Summable.sum_add_tsum_nat_add.
  Lean, line 29
  have h1 := Summable.sum_add_tsum_nat_add (n + 1) hs
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 29 at 7965601f1a79 ↗
2. htail.h2 have ∀ (j : ℕ), (↑(f (j + (n + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (j + (n + (1 : ℕ))) = (1 : ℝ) / (2 : ℝ) ^ n * ((↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)))
  Leaves ∑' (j : ℕ), (↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (2 : ℝ) ^ n * ∑' (m : ℕ), (↑(f m) : ℝ) / (2 : ℝ) ^ m - (↑(∑ i ∈ Finset.range (n + (1 : ℕ)), f i * (2 : ℕ) ^ (n - i)) : ℝ), with h2 : ∀ (j : ℕ), (↑(f (j + (n + (1 : ℕ)))) : ℝ) / (2 : ℝ) ^ (j + (n + (1 : ℕ))) = (1 : ℝ) / (2 : ℝ) ^ n * ((↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ))).
  Uses library pow_add.
  Lean, lines 30–34
  have h2 : ∀ j : ℕ, (f (j + (n + 1)) : ℝ) / 2 ^ (j + (n + 1)) = (1 / 2 ^ n) * ((f (n + 1 + j) : ℝ) / 2 ^ (j + 1)) := by intro j rw [show j + (n + 1) = n + 1 + j by omega, show n + 1 + j = n + (j + 1) by omega, pow_add] field_simp
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 30–34 at 7965601f1a79 ↗
3. htail.h3 have (2 : ℝ) ^ n * ∑ i ∈ Finset.range (n + (1 : ℕ)), (↑(f i) : ℝ) / (2 : ℝ) ^ i = (↑(∑ i ∈ Finset.range (n + (1 : ℕ)), f i * (2 : ℕ) ^ (n - i)) : ℝ)
  Leaves ∑' (j : ℕ), (↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (2 : ℝ) ^ n * ∑' (m : ℕ), (↑(f m) : ℝ) / (2 : ℝ) ^ m - (↑(∑ i ∈ Finset.range (n + (1 : ℕ)), f i * (2 : ℕ) ^ (n - i)) : ℝ), with h3 : (2 : ℝ) ^ n * ∑ i ∈ Finset.range (n + (1 : ℕ)), (↑(f i) : ℝ) / (2 : ℝ) ^ i = (↑(∑ i ∈ Finset.range (n + (1 : ℕ)), f i * (2 : ℕ) ^ (n - i)) : ℝ).
  Uses library Finset.range, Finset.mul_sum, Finset.sum_congr, rfl.
  Lean, lines 36–45
  have h3 : (2 : ℝ) ^ n * ∑ i ∈ Finset.range (n + 1), (f i : ℝ) / 2 ^ i = ((∑ i ∈ Finset.range (n + 1), f i * 2 ^ (n - i) : ℕ) : ℝ) := by push_cast rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun i hi => ?_) have hi' : i ≤ n := Nat.lt_succ_iff.1 (Finset.mem_range.1 hi) have : (2 : ℝ) ^ n = 2 ^ (n - i) * 2 ^ i := by rw [← pow_add, Nat.sub_add_cancel hi'] rw [this] field_simp
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 36–45 at 7965601f1a79 ↗
  htail.h3.hi' have i ≤ n
  Leaves (2 : ℝ) ^ n * ((↑(f i) : ℝ) / (2 : ℝ) ^ i) = (↑(f i) : ℝ) * (2 : ℝ) ^ (n - i), with hi' : i ≤ n.
  Uses library Nat.lt_succ_iff, Finset.mem_range.
  Lean, line 41
  have hi' : i ≤ n := Nat.lt_succ_iff.1 (Finset.mem_range.1 hi)
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 41 at 7965601f1a79 ↗
  htail.h3.this have (2 : ℝ) ^ n = (2 : ℝ) ^ (n - i) * (2 : ℝ) ^ i
  Leaves (2 : ℝ) ^ n * ((↑(f i) : ℝ) / (2 : ℝ) ^ i) = (↑(f i) : ℝ) * (2 : ℝ) ^ (n - i), with this : (2 : ℝ) ^ n = (2 : ℝ) ^ (n - i) * (2 : ℝ) ^ i.
  Uses library pow_add, Nat.sub_add_cancel.
  Lean, lines 42–43
  have : (2 : ℝ) ^ n = 2 ^ (n - i) * 2 ^ i := by rw [← pow_add, Nat.sub_add_cancel hi']
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 42–43 at 7965601f1a79 ↗
hper have ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ)
Leaves ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), ∑' (j : ℕ), (↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) - ∑' (j : ℕ), (↑(f (n' + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (↑z : ℝ), with hper : ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ).
Uses library ZMod, Exists.intro, le_total.
Lean, lines 49–97
```
  have hper : ∃ p N₀ : ℕ, 0 < p ∧ ∀ n n' : ℕ, N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] →
      ∃ z : ℤ, (2 : ℝ) ^ n * (q : ℝ) - 2 ^ n' * (q : ℝ) = z := by
    have : NeZero q.den := ⟨q.den_nz⟩
    let g : ℕ → ZMod q.den := fun n => ((2 ^ n * q.num : ℤ) : ZMod q.den)
    obtain ⟨x, y, hxy, hg⟩ := Finite.exists_ne_map_eq_of_infinite g
    have hkey : ∃ n₀ p : ℕ, 0 < p ∧ (q.den : ℤ) ∣ 2 ^ (n₀ + p) * q.num - 2 ^ n₀ * q.num := by
      have h := (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).1 hg
      rcases lt_or_gt_of_ne hxy with hlt | hlt
      · refine ⟨x, y - x, by omega, ?_⟩
        rw [show x + (y - x) = y by omega]
        exact h
      · refine ⟨y, x - y, by omega, ?_⟩
        rw [show y + (x - y) = x by omega, ← dvd_neg, neg_sub]
        exact h
    obtain ⟨n₀, p, hp, hd⟩ := hkey
    have hmul : ∀ m t : ℕ, (q.den : ℤ) ∣ 2 ^ (n₀ + t + m * p) * q.num - 2 ^ (n₀ + t) * q.num := by
      intro m t
      induction m with
      | zero => simp
      | succ m ih =>
        have e : (2 : ℤ) ^ (n₀ + t + (m + 1) * p) * q.num - 2 ^ (n₀ + t) * q.num
            = 2 ^ (t + m * p) * (2 ^ (n₀ + p) * q.num - 2 ^ n₀ * q.num)
              + (2 ^ (n₀ + t + m * p) * q.num - 2 ^ (n₀ + t) * q.num) := by
          rw [show n₀ + t + (m + 1) * p = (t + m * p) + (n₀ + p) by ring,
            show n₀ + t + m * p = (t + m * p) + n₀ by ring, pow_add, pow_add]
          ring
        rw [e]
        exact dvd_add (dvd_mul_of_dvd_right hd _) ih
    have hle : ∀ n n' : ℕ, n₀ ≤ n → n ≤ n' → n ≡ n' [MOD p] →
        ∃ z : ℤ, (2 : ℝ) ^ n * (q : ℝ) - 2 ^ n' * (q : ℝ) = z := by
      intro n n' hn hnn' hmod
      obtain ⟨m, hm⟩ := (Nat.modEq_iff_dvd' hnn').1 hmod
      have h1 := hmul m (n - n₀)
      rw [show n₀ + (n - n₀) = n by omega, show n + m * p = n' by
        rw [mul_comm]; omega] at h1
      obtain ⟨w, hw⟩ := h1
      refine ⟨-w, ?_⟩
      have hden : (q.den : ℝ) ≠ 0 := by exact_mod_cast q.den_nz
      have hw' : (2 : ℝ) ^ n' * (q.num : ℝ) - 2 ^ n * (q.num : ℝ) = (q.den : ℝ) * (w : ℝ) := by
        exact_mod_cast hw
      rw [Rat.cast_def]
      field_simp
      push_cast
      linarith
    refine ⟨p, n₀, hp, fun n n' hn hn' hmod => ?_⟩
    rcases le_total n n' with h | h
    · exact hle n n' hn h hmod
    · obtain ⟨z, hz⟩ := hle n' n hn' h hmod.symm
      exact ⟨-z, by push_cast; linarith⟩
```
targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 49–97 at 7965601f1a79 ↗
1. hper.this have NeZero q.den
  Leaves ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with this : NeZero q.den.
  Uses library NeZero, NeZero.mk.
  Lean, line 51
  have : NeZero q.den := ⟨q.den_nz⟩
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 51 at 7965601f1a79 ↗
2. hper.s2 obtain ∃ (x : ℕ) (y : ℕ), x ≠ y ∧ g x = g y
  Leaves ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with x : ℕ, y : ℕ, hxy : x ≠ y, hg : g x = g y.
  Uses library Finite.exists_ne_map_eq_of_infinite.
  Lean, line 53
  obtain ⟨x, y, hxy, hg⟩ := Finite.exists_ne_map_eq_of_infinite g
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 53 at 7965601f1a79 ↗
3. hper.hkey have ∃ (n₀ : ℕ) (p : ℕ), (0 : ℕ) < p ∧ (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + p) * q.num - (2 : ℤ) ^ n₀ * q.num
  Leaves ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with hkey : ∃ (n₀ : ℕ) (p : ℕ), (0 : ℕ) < p ∧ (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + p) * q.num - (2 : ℤ) ^ n₀ * q.num.
  Uses library lt_or_gt_of_ne.
  Lean, lines 54–62
  have hkey : ∃ n₀ p : ℕ, 0 < p ∧ (q.den : ℤ) ∣ 2 ^ (n₀ + p) * q.num - 2 ^ n₀ * q.num := by have h := (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).1 hg rcases lt_or_gt_of_ne hxy with hlt | hlt · refine ⟨x, y - x, by omega, ?_⟩ rw [show x + (y - x) = y by omega] exact h · refine ⟨y, x - y, by omega, ?_⟩ rw [show y + (x - y) = x by omega, ← dvd_neg, neg_sub] exact h
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 54–62 at 7965601f1a79 ↗
  hper.hkey.h have (↑q.den : ℤ) ∣ (2 : ℤ) ^ y * q.num - (2 : ℤ) ^ x * q.num
  Leaves ∃ (n₀ : ℕ) (p : ℕ), (0 : ℕ) < p ∧ (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + p) * q.num - (2 : ℤ) ^ n₀ * q.num, with h : (↑q.den : ℤ) ∣ (2 : ℤ) ^ y * q.num - (2 : ℤ) ^ x * q.num.
  Uses library ZMod.intCast_eq_intCast_iff_dvd_sub.
  Lean, line 55
  have h := (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).1 hg
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 55 at 7965601f1a79 ↗
  hper.hkey.s2 case
  Leaves ∃ (n₀ : ℕ) (p : ℕ), (0 : ℕ) < p ∧ (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + p) * q.num - (2 : ℤ) ^ n₀ * q.num.
  Uses library Exists.intro.
  Lean, lines 57–59
  · refine ⟨x, y - x, by omega, ?_⟩ rw [show x + (y - x) = y by omega] exact h
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 57–59 at 7965601f1a79 ↗
  hper.hkey.s3 case
  Leaves ∃ (n₀ : ℕ) (p : ℕ), (0 : ℕ) < p ∧ (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + p) * q.num - (2 : ℤ) ^ n₀ * q.num.
  Uses library Exists.intro, dvd_neg, neg_sub.
  Lean, lines 60–62
  · refine ⟨y, x - y, by omega, ?_⟩ rw [show y + (x - y) = x by omega, ← dvd_neg, neg_sub] exact h
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 60–62 at 7965601f1a79 ↗
4. hper.s4 obtain ∃ (n₀ : ℕ) (p : ℕ), (0 : ℕ) < p ∧ (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + p) * q.num - (2 : ℤ) ^ n₀ * q.num
  Leaves ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with n₀ : ℕ, p : ℕ, hp : (0 : ℕ) < p, hd : (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + p) * q.num - (2 : ℤ) ^ n₀ * q.num.
  Lean, line 63
  obtain ⟨n₀, p, hp, hd⟩ := hkey
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 63 at 7965601f1a79 ↗
5. hper.hmul have ∀ (m t : ℕ), (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + t + m * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num
  Leaves ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with hmul : ∀ (m t : ℕ), (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + t + m * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num.
  Lean, lines 64–76
  have hmul : ∀ m t : ℕ, (q.den : ℤ) ∣ 2 ^ (n₀ + t + m * p) * q.num - 2 ^ (n₀ + t) * q.num := by intro m t induction m with | zero => simp | succ m ih => have e : (2 : ℤ) ^ (n₀ + t + (m + 1) * p) * q.num - 2 ^ (n₀ + t) * q.num = 2 ^ (t + m * p) * (2 ^ (n₀ + p) * q.num - 2 ^ n₀ * q.num) + (2 ^ (n₀ + t + m * p) * q.num - 2 ^ (n₀ + t) * q.num) := by rw [show n₀ + t + (m + 1) * p = (t + m * p) + (n₀ + p) by ring, show n₀ + t + m * p = (t + m * p) + n₀ by ring, pow_add, pow_add] ring rw [e] exact dvd_add (dvd_mul_of_dvd_right hd _) ih
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 64–76 at 7965601f1a79 ↗
  hper.hmul.s1 case routine: simp
  Leaves (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + t + (0 : ℕ) * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num.
  Uses library Nat.zero.
  Lean, line 67
  | zero => simp
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 67 at 7965601f1a79 ↗
  hper.hmul.s2 case
  Leaves (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + t + (m + (1 : ℕ)) * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num, with m : ℕ, ih : (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + t + m * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num.
  Uses library Nat.succ, dvd_add, dvd_mul_of_dvd_right.
  Lean, lines 68–76
  | succ m ih => have e : (2 : ℤ) ^ (n₀ + t + (m + 1) * p) * q.num - 2 ^ (n₀ + t) * q.num = 2 ^ (t + m * p) * (2 ^ (n₀ + p) * q.num - 2 ^ n₀ * q.num) + (2 ^ (n₀ + t + m * p) * q.num - 2 ^ (n₀ + t) * q.num) := by rw [show n₀ + t + (m + 1) * p = (t + m * p) + (n₀ + p) by ring, show n₀ + t + m * p = (t + m * p) + n₀ by ring, pow_add, pow_add] ring rw [e] exact dvd_add (dvd_mul_of_dvd_right hd _) ih
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 68–76 at 7965601f1a79 ↗
  hper.hmul.s2.e have (2 : ℤ) ^ (n₀ + t + (m + (1 : ℕ)) * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num = (2 : ℤ) ^ (t + m * p) * ((2 : ℤ) ^ (n₀ + p) * q.num - (2 : ℤ) ^ n₀ * q.num) + ((2 : ℤ) ^ (n₀ + t + m * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num)
  Leaves (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + t + (m + (1 : ℕ)) * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num, with e : (2 : ℤ) ^ (n₀ + t + (m + (1 : ℕ)) * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num = (2 : ℤ) ^ (t + m * p) * ((2 : ℤ) ^ (n₀ + p) * q.num - (2 : ℤ) ^ n₀ * q.num) + ((2 : ℤ) ^ (n₀ + t + m * p) * q.num - (2 : ℤ) ^ (n₀ + t) * q.num).
  Uses library pow_add.
  Lean, lines 69–74
  have e : (2 : ℤ) ^ (n₀ + t + (m + 1) * p) * q.num - 2 ^ (n₀ + t) * q.num = 2 ^ (t + m * p) * (2 ^ (n₀ + p) * q.num - 2 ^ n₀ * q.num) + (2 ^ (n₀ + t + m * p) * q.num - 2 ^ (n₀ + t) * q.num) := by rw [show n₀ + t + (m + 1) * p = (t + m * p) + (n₀ + p) by ring, show n₀ + t + m * p = (t + m * p) + n₀ by ring, pow_add, pow_add] ring
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 69–74 at 7965601f1a79 ↗
6. hper.hle have ∀ (n n' : ℕ), n₀ ≤ n → n ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ)
  Leaves ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with hle : ∀ (n n' : ℕ), n₀ ≤ n → n ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ).
  Uses library mul_comm, Exists.intro, Rat.cast_def.
  Lean, lines 77–92
  have hle : ∀ n n' : ℕ, n₀ ≤ n → n ≤ n' → n ≡ n' [MOD p] → ∃ z : ℤ, (2 : ℝ) ^ n * (q : ℝ) - 2 ^ n' * (q : ℝ) = z := by intro n n' hn hnn' hmod obtain ⟨m, hm⟩ := (Nat.modEq_iff_dvd' hnn').1 hmod have h1 := hmul m (n - n₀) rw [show n₀ + (n - n₀) = n by omega, show n + m * p = n' by rw [mul_comm]; omega] at h1 obtain ⟨w, hw⟩ := h1 refine ⟨-w, ?_⟩ have hden : (q.den : ℝ) ≠ 0 := by exact_mod_cast q.den_nz have hw' : (2 : ℝ) ^ n' * (q.num : ℝ) - 2 ^ n * (q.num : ℝ) = (q.den : ℝ) * (w : ℝ) := by exact_mod_cast hw rw [Rat.cast_def] field_simp push_cast linarith
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 77–92 at 7965601f1a79 ↗
  hper.hle.s1 obtain p ∣ n' - n
  Leaves ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with m : ℕ, hm : n' - n = p * m.
  Uses library Nat.modEq_iff_dvd'.
  Lean, line 80
  obtain ⟨m, hm⟩ := (Nat.modEq_iff_dvd' hnn').1 hmod
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 80 at 7965601f1a79 ↗
  hper.hle.h1 have (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + (n - n₀) + m * p) * q.num - (2 : ℤ) ^ (n₀ + (n - n₀)) * q.num
  Leaves ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with h1 : (↑q.den : ℤ) ∣ (2 : ℤ) ^ (n₀ + (n - n₀) + m * p) * q.num - (2 : ℤ) ^ (n₀ + (n - n₀)) * q.num.
  Lean, line 81
  have h1 := hmul m (n - n₀)
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 81 at 7965601f1a79 ↗
  hper.hle.s3 obtain (↑q.den : ℤ) ∣ (2 : ℤ) ^ n' * q.num - (2 : ℤ) ^ n * q.num
  Leaves ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with w : ℤ, hw : (2 : ℤ) ^ n' * q.num - (2 : ℤ) ^ n * q.num = (↑q.den : ℤ) * w.
  Lean, line 84
  obtain ⟨w, hw⟩ := h1
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 84 at 7965601f1a79 ↗
  hper.hle.hden have (↑q.den : ℝ) ≠ (0 : ℝ)
  Leaves (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑(-w) : ℝ), with hden : (↑q.den : ℝ) ≠ (0 : ℝ).
  Lean, line 86
  have hden : (q.den : ℝ) ≠ 0 := by exact_mod_cast q.den_nz
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 86 at 7965601f1a79 ↗
  hper.hle.hw' have (2 : ℝ) ^ n' * (↑q.num : ℝ) - (2 : ℝ) ^ n * (↑q.num : ℝ) = (↑q.den : ℝ) * (↑w : ℝ)
  Leaves (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑(-w) : ℝ), with hw' : (2 : ℝ) ^ n' * (↑q.num : ℝ) - (2 : ℝ) ^ n * (↑q.num : ℝ) = (↑q.den : ℝ) * (↑w : ℝ).
  Lean, lines 87–88
  have hw' : (2 : ℝ) ^ n' * (q.num : ℝ) - 2 ^ n * (q.num : ℝ) = (q.den : ℝ) * (w : ℝ) := by exact_mod_cast hw
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 87–88 at 7965601f1a79 ↗
7. hper.s7 case
  Leaves ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ).
  Lean, line 95
  · exact hle n n' hn h hmod
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 95 at 7965601f1a79 ↗
8. hper.s8 case
  Leaves ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ).
  Uses library Exists.intro.
  Lean, lines 96–97
  · obtain ⟨z, hz⟩ := hle n' n hn' h hmod.symm exact ⟨-z, by push_cast; linarith⟩
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, lines 96–97 at 7965601f1a79 ↗
  hper.s8.s1 obtain ∃ (z : ℤ), (2 : ℝ) ^ n' * (↑q : ℝ) - (2 : ℝ) ^ n * (↑q : ℝ) = (↑z : ℝ)
  Leaves ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ), with z : ℤ, hz : (2 : ℝ) ^ n' * (↑q : ℝ) - (2 : ℝ) ^ n * (↑q : ℝ) = (↑z : ℝ).
  Lean, line 96
  · obtain ⟨z, hz⟩ := hle n' n hn' h hmod.symm
  targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 96 at 7965601f1a79 ↗
s3 obtain ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ)
Leaves ∃ (p : ℕ) (N₀ : ℕ), (0 : ℕ) < p ∧ ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), ∑' (j : ℕ), (↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) - ∑' (j : ℕ), (↑(f (n' + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (↑z : ℝ), with p : ℕ, N₀ : ℕ, hp : (0 : ℕ) < p, h : ∀ (n n' : ℕ), N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] → ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ).
Lean, line 99
```
  obtain ⟨p, N₀, hp, h⟩ := hper
```
targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 99 at 7965601f1a79 ↗
s4 obtain ∃ (z : ℤ), (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ)
Leaves ∃ (z : ℤ), ∑' (j : ℕ), (↑(f (n + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) - ∑' (j : ℕ), (↑(f (n' + (1 : ℕ) + j)) : ℝ) / (2 : ℝ) ^ (j + (1 : ℕ)) = (↑z : ℝ), with z : ℤ, hz : (2 : ℝ) ^ n * (↑q : ℝ) - (2 : ℝ) ^ n' * (↑q : ℝ) = (↑z : ℝ).
Lean, line 101
```
  obtain ⟨z, hz⟩ := h n n' hn hn' hmod
```
targets/erdos-69/nodes/spec-c390279b/Proof.lean, line 101 at 7965601f1a79 ↗

The proof in Lean (Proof.lean)

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

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-69/nodes/spec-c390279b/Proof.lean, sha256 7d621b770af1.

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

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): if a binary-weighted series `∑ f(n)/2^n`
of natural numbers is rational, its tails `∑' j, f (n + 1 + j) / 2^(j+1)` are eventually
periodic modulo 1: there are `p > 0` and `N₀` such that any two tails from `n, n' ≥ N₀` with
`n ≡ n' [MOD p]` differ by an integer. Proof: the tail is `2^n x` minus an integer, and `2^n q`
is eventually periodic mod 1 by pigeonhole on `2^n · num mod den`. With `f = ω` this is the
first step of a proof of erdos-69 by contradiction (the tails the nodes under erdos-69--h2-v2
use are exactly these, with `f = ω`); what would remain is to exhibit two tails in one class
that do not differ by an integer, which is the hard part and is not here. The statement is
over any `f` so that its hypotheses are satisfiable (for `f = ω` they are not, the target's
sum being irrational), as step 7 requires. -/

theorem Opn.erdos_69_rational_tails_periodic :
    ∀ (f : ℕ → ℕ) (q : ℚ), Summable (fun n : ℕ => (f n : ℝ) / 2 ^ n) →
      (q : ℝ) = ∑' n : ℕ, (f n : ℝ) / 2 ^ n →
      ∃ p N₀ : ℕ, 0 < p ∧ ∀ n n' : ℕ, N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] →
        ∃ z : ℤ, ∑' j : ℕ, (f (n + 1 + j) : ℝ) / 2 ^ (j + 1)
          - ∑' j : ℕ, (f (n' + 1 + j) : ℝ) / 2 ^ (j + 1) = z := by
  intro f q hs hq
  -- (a) the tail formula: tail_n = 2^n x - A_n with A_n a natural number
  have htail : ∀ n : ℕ, ∑' j : ℕ, (f (n + 1 + j) : ℝ) / 2 ^ (j + 1)
      = 2 ^ n * ∑' m : ℕ, (f m : ℝ) / 2 ^ m
        - ((∑ i ∈ Finset.range (n + 1), f i * 2 ^ (n - i) : ℕ) : ℝ) := by
    intro n
    have h1 := Summable.sum_add_tsum_nat_add (n + 1) hs
    have h2 : ∀ j : ℕ, (f (j + (n + 1)) : ℝ) / 2 ^ (j + (n + 1))
        = (1 / 2 ^ n) * ((f (n + 1 + j) : ℝ) / 2 ^ (j + 1)) := by
      intro j
      rw [show j + (n + 1) = n + 1 + j by omega, show n + 1 + j = n + (j + 1) by omega, pow_add]
      field_simp
    rw [tsum_congr h2, tsum_mul_left] at h1
    have h3 : (2 : ℝ) ^ n * ∑ i ∈ Finset.range (n + 1), (f i : ℝ) / 2 ^ i
        = ((∑ i ∈ Finset.range (n + 1), f i * 2 ^ (n - i) : ℕ) : ℝ) := by
      push_cast
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl (fun i hi => ?_)
      have hi' : i ≤ n := Nat.lt_succ_iff.1 (Finset.mem_range.1 hi)
      have : (2 : ℝ) ^ n = 2 ^ (n - i) * 2 ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [this]
      field_simp
    rw [← h1, mul_add, h3, ← mul_assoc, mul_one_div_cancel (by positivity), one_mul]
    ring
  -- (b) 2^n q is eventually periodic mod 1 (pigeonhole on 2^n num mod den)
  have hper : ∃ p N₀ : ℕ, 0 < p ∧ ∀ n n' : ℕ, N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] →
      ∃ z : ℤ, (2 : ℝ) ^ n * (q : ℝ) - 2 ^ n' * (q : ℝ) = z := by
    have : NeZero q.den := ⟨q.den_nz⟩
    let g : ℕ → ZMod q.den := fun n => ((2 ^ n * q.num : ℤ) : ZMod q.den)
    obtain ⟨x, y, hxy, hg⟩ := Finite.exists_ne_map_eq_of_infinite g
    have hkey : ∃ n₀ p : ℕ, 0 < p ∧ (q.den : ℤ) ∣ 2 ^ (n₀ + p) * q.num - 2 ^ n₀ * q.num := by
      have h := (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).1 hg
      rcases lt_or_gt_of_ne hxy with hlt | hlt
      · refine ⟨x, y - x, by omega, ?_⟩
        rw [show x + (y - x) = y by omega]
        exact h
      · refine ⟨y, x - y, by omega, ?_⟩
        rw [show y + (x - y) = x by omega, ← dvd_neg, neg_sub]
        exact h
    obtain ⟨n₀, p, hp, hd⟩ := hkey
    have hmul : ∀ m t : ℕ, (q.den : ℤ) ∣ 2 ^ (n₀ + t + m * p) * q.num - 2 ^ (n₀ + t) * q.num := by
      intro m t
      induction m with
      | zero => simp
      | succ m ih =>
        have e : (2 : ℤ) ^ (n₀ + t + (m + 1) * p) * q.num - 2 ^ (n₀ + t) * q.num
            = 2 ^ (t + m * p) * (2 ^ (n₀ + p) * q.num - 2 ^ n₀ * q.num)
              + (2 ^ (n₀ + t + m * p) * q.num - 2 ^ (n₀ + t) * q.num) := by
          rw [show n₀ + t + (m + 1) * p = (t + m * p) + (n₀ + p) by ring,
            show n₀ + t + m * p = (t + m * p) + n₀ by ring, pow_add, pow_add]
          ring
        rw [e]
        exact dvd_add (dvd_mul_of_dvd_right hd _) ih
    have hle : ∀ n n' : ℕ, n₀ ≤ n → n ≤ n' → n ≡ n' [MOD p] →
        ∃ z : ℤ, (2 : ℝ) ^ n * (q : ℝ) - 2 ^ n' * (q : ℝ) = z := by
      intro n n' hn hnn' hmod
      obtain ⟨m, hm⟩ := (Nat.modEq_iff_dvd' hnn').1 hmod
      have h1 := hmul m (n - n₀)
      rw [show n₀ + (n - n₀) = n by omega, show n + m * p = n' by
        rw [mul_comm]; omega] at h1
      obtain ⟨w, hw⟩ := h1
      refine ⟨-w, ?_⟩
      have hden : (q.den : ℝ) ≠ 0 := by exact_mod_cast q.den_nz
      have hw' : (2 : ℝ) ^ n' * (q.num : ℝ) - 2 ^ n * (q.num : ℝ) = (q.den : ℝ) * (w : ℝ) := by
        exact_mod_cast hw
      rw [Rat.cast_def]
      field_simp
      push_cast
      linarith
    refine ⟨p, n₀, hp, fun n n' hn hn' hmod => ?_⟩
    rcases le_total n n' with h | h
    · exact hle n n' hn h hmod
    · obtain ⟨z, hz⟩ := hle n' n hn' h hmod.symm
      exact ⟨-z, by push_cast; linarith⟩
  -- (c) combine
  obtain ⟨p, N₀, hp, h⟩ := hper
  refine ⟨p, N₀, hp, fun n n' hn hn' hmod => ?_⟩
  obtain ⟨z, hz⟩ := h n n' hn hn' hmod
  refine ⟨z - ((∑ i ∈ Finset.range (n + 1), f i * 2 ^ (n - i) : ℕ) : ℤ)
    + ((∑ i ∈ Finset.range (n' + 1), f i * 2 ^ (n' - i) : ℕ) : ℤ), ?_⟩
  rw [htail n, htail n', ← hq]
  push_cast
  linarith

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

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

open scoped ArithmeticFunction.omega

/-! A speculative ingredient for erdos-69 (D-29): if a binary-weighted series `∑ f(n)/2^n`
of natural numbers is rational, its tails `∑' j, f (n + 1 + j) / 2^(j+1)` are eventually
periodic modulo 1: there are `p > 0` and `N₀` such that any two tails from `n, n' ≥ N₀` with
`n ≡ n' [MOD p]` differ by an integer. Proof: the tail is `2^n x` minus an integer, and `2^n q`
is eventually periodic mod 1 by pigeonhole on `2^n · num mod den`. With `f = ω` this is the
first step of a proof of erdos-69 by contradiction (the tails the nodes under erdos-69--h2-v2
use are exactly these, with `f = ω`); what would remain is to exhibit two tails in one class
that do not differ by an integer, which is the hard part and is not here. The statement is
over any `f` so that its hypotheses are satisfiable (for `f = ω` they are not, the target's
sum being irrational), as step 7 requires. -/

theorem Opn.erdos_69_rational_tails_periodic :
    ∀ (f : ℕ → ℕ) (q : ℚ), Summable (fun n : ℕ => (f n : ℝ) / 2 ^ n) →
      (q : ℝ) = ∑' n : ℕ, (f n : ℝ) / 2 ^ n →
      ∃ p N₀ : ℕ, 0 < p ∧ ∀ n n' : ℕ, N₀ ≤ n → N₀ ≤ n' → n ≡ n' [MOD p] →
        ∃ z : ℤ, ∑' j : ℕ, (f (n + 1 + j) : ℝ) / 2 ^ (j + 1)
          - ∑' j : ℕ, (f (n' + 1 + j) : ℝ) / 2 ^ (j + 1) = z := by
  sorry

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

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

Rendered from targets/erdos-69/nodes/spec-c390279b/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000306.json, merge commit 7965601f1a79.

Verdict pass, from attestations/000306.json.

Submitter: t0929-3
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (calibration)

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/000306.json, merge commit 7965601f1a79.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/spec-c390279b/Witness.lean, sha256 353491dd7fba.

import Mathlib

open scoped ArithmeticFunction.omega

theorem witness : ∃ (f : ℕ → ℕ) (q : ℚ), Summable (fun n : ℕ => (f n : ℝ) / 2 ^ n) ∧
    (q : ℝ) = ∑' n : ℕ, (f n : ℝ) / 2 ^ n :=
  ⟨fun _ => 0, 0, by 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 (3)

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

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

The real divisor 2^(j+1) is positive for every j, never 0.

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

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

The real divisor 2^(j+1) is positive for every j, never 0.

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

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

The real divisor 2^n is positive for every n, never 0.

How to read this page

How to read a statement’s page →