Walking to infinity on primes

DefinitionExtended Cunningham chain#✓fully proved

For a natural number \(p\), the extended Cunningham chain generated by \(p\) is the sequence \(e_0, e_1, e_2, \ldots\) of natural numbers given by \(e_0 = p\) and \(e_k = 2 e_{k-1} + 1\) for \(k \ge 1\); in binary, \(e_k\) is obtained from \(p\) by appending \(k\) digits \(1\) on the right.

The paper requires the generator \(p\) to be prime; here \(p\) may be any natural number, and results that need primality assume it explicitly.

public def extendedCunninghamChain (p : ℕ) : ℕ → ℕ
  | 0 => p
  | k + 1 => 2 * extendedCunninghamChain p k + 1

Sources

• Steven J. Miller, Fei Peng, Tudor Popescu, Joshua M. Siktar, and Nawapan Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Definition 2.4.

Used by 5

Used byClosed form of the extended Cunningham chain · Extended Cunningham chains generated by primes contain arbitrarily long composite runs · Recurrence of the extended Cunningham chain · First terms of the extended Cunningham chain generated by 2 · Initial term of the extended Cunningham chain

TheoremInitial term of the extended Cunningham chain#✓fully proved

For every natural number \(p\), the extended Cunningham chain generated by \(p\) has initial term \(e_0 = p\).

public theorem extendedCunninghamChain_zero (p : ℕ) : extendedCunninghamChain p 0 = p

Sources

• Miller, Peng, Popescu, Siktar, and Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Definition 2.4.

Uses 1

Statement usesExtended Cunningham chain

TheoremRecurrence of the extended Cunningham chain#✓fully proved

For all natural numbers \(p\) and \(k\), the terms of the extended Cunningham chain generated by \(p\) satisfy \(e_{k+1} = 2 e_k + 1\).

public theorem extendedCunninghamChain_succ (p k : ℕ) :
    extendedCunninghamChain p (k + 1) = 2 * extendedCunninghamChain p k + 1

Sources

• Miller, Peng, Popescu, Siktar, and Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Definition 2.4.

Uses 1 · Used by 1

Statement usesExtended Cunningham chain

Used byClosed form of the extended Cunningham chain

TheoremClosed form of the extended Cunningham chain#✓fully proved

For all natural numbers \(p\) and \(k\), the \(k\)-th term \(e_k\) of the extended Cunningham chain generated by \(p\) satisfies \(e_k + 1 = 2^k (p + 1)\), that is, \(e_k = 2^k (p + 1) - 1\).

public theorem extendedCunninghamChain_add_one (p k : ℕ) :
    extendedCunninghamChain p k + 1 = 2 ^ k * (p + 1)

Sources

• Miller, Peng, Popescu, Siktar, and Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, display after Definition 2.4.

Uses 2

Statement usesExtended Cunningham chain

Proof usesRecurrence of the extended Cunningham chain

TheoremFirst terms of the extended Cunningham chain generated by 2#✓fully proved

The extended Cunningham chain \(e_0, e_1, e_2, \ldots\) generated by \(2\) has \(e_1 = 5\), \(e_2 = 11\) and \(e_3 = 23\).

public theorem extendedCunninghamChain_two_small :
    extendedCunninghamChain 2 1 = 5 ∧ extendedCunninghamChain 2 2 = 11 ∧
      extendedCunninghamChain 2 3 = 23

Sources

• Miller, Peng, Popescu, Siktar, and Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Definition 2.4.

Uses 1

Statement usesExtended Cunningham chain

TheoremWalking to infinity on primes by appending decimal digits#●ready to prove

For every prime \(p_0\) there is a sequence of primes \(p_0, p_1, p_2, \ldots\) starting at \(p_0\) such that for every \(i \ge 1\) there are integers \(n_i \ge 1\) and \(k_i\) with \(0 < k_i < 10^{n_i}\) and \(p_i = 10^{n_i} p_{i-1} + k_i\); that is, each term is obtained from the previous one by appending \(n_i\) decimal digits on the right.

public theorem_wanted exists_prime_walk_appending_decimal_digits (p₀ : ℕ) (hp₀ : p₀.Prime) :
    ∃ p : ℕ → ℕ, p 0 = p₀ ∧ (∀ i, (p i).Prime) ∧
      ∀ i, ∃ n k : ℕ, 0 < n ∧ 0 < k ∧ k < 10 ^ n ∧ p (i + 1) = 10 ^ n * p i + k

Sources

• Steven J. Miller, Fei Peng, Tudor Popescu, Joshua M. Siktar, and Nawapan Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Theorem 2.3.

TheoremA power of two minus a much smaller positive number is not a power of two#●ready to prove

Let \(p\) and \(k\) be natural numbers with \(k \ge \lceil \log_2 (p + 1) \rceil + 2\). Then \(2^k - (p + 1)\) is not a power of \(2\): there is no natural number \(m\) with \(2^k - (p + 1) = 2^m\).

Under this hypothesis \(2^k > p + 1\), so the subtraction is exact. The source assumes \(p\) is prime; the statement holds without that assumption.

public theorem_wanted two_pow_sub_succ_ne_two_pow (p k : ℕ) (hk : Nat.clog 2 (p + 1) + 2 ≤ k) :
    ¬ ∃ m : ℕ, 2 ^ k - (p + 1) = 2 ^ m

Sources

• Steven J. Miller, Fei Peng, Tudor Popescu, Joshua M. Siktar, and Nawapan Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Lemma 2.5.

TheoremExtended Cunningham chains generated by primes contain arbitrarily long composite runs#●ready to prove

Let \(p\) be a prime and let \(e_0 = p, e_1, e_2, \ldots\) be the extended Cunningham chain generated by \(p\). For every \(n \ge 1\) there is \(i \ge 1\) such that none of \(e_i, e_{i+1}, \ldots, e_{i+n-1}\) is prime.

Since \(e_i \ge 2p + 1 \ge 5\) for \(i \ge 1\), these terms are composite.

public theorem_wanted extendedCunninghamChain_exists_composite_run (p : ℕ) (hp : p.Prime)
    (n : ℕ) (hn : 0 < n) :
    ∃ i, 0 < i ∧ ∀ j < n, ¬ (extendedCunninghamChain p (i + j)).Prime

Sources

• Steven J. Miller, Fei Peng, Tudor Popescu, Joshua M. Siktar, and Nawapan Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Theorem 2.6.

Uses 1

Statement usesExtended Cunningham chain

TheoremNo binary prime walk to infinity in steps of one or two digits#●ready to prove

There is no sequence of primes \(p_0, p_1, p_2, \ldots\) such that for every \(i \ge 0\) there are \(n \in \{1, 2\}\) and a natural number \(k < 2^n\) with \(p_{i+1} = 2^n p_i + k\). That is, starting from any prime, one cannot walk to infinity on primes by appending one or two binary digits at a time on the right.

The appended blocks are the paper's \(0, 1, 00, 01, 10, 11\) (a block may begin with \(0\)).

public theorem_wanted not_exists_binary_prime_walk_appending_at_most_two_digits :
    ¬ ∃ p : ℕ → ℕ, (∀ i, (p i).Prime) ∧
      ∀ i, ∃ n k : ℕ, 1 ≤ n ∧ n ≤ 2 ∧ k < 2 ^ n ∧ p (i + 1) = 2 ^ n * p i + k

Sources

• Steven J. Miller, Fei Peng, Tudor Popescu, Joshua M. Siktar, and Nawapan Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Theorem 2.7.

DefinitionCounting right-truncatable square-free numbers#✓fully proved

For natural numbers \(b\) and \(k\), \(L_{b,k}\) is the number of right-truncatable square-free numbers with exactly \(k\) digits in base \(b\): the number of natural numbers \(x\) with \(b^{k-1} \le x < b^k\) such that \(\lfloor x / b^{\ell} \rfloor\) is square-free for every \(\ell \in \{0, \dots, k-1\}\). When \(k = 0\) the range is empty, so \(L_{b,0} = 0\).

public def rightTruncSquarefreeCount (b k : ℕ) : ℕ :=
  ((Finset.Ico (b ^ (k - 1)) (b ^ k)).filter
    (fun x => ∀ l ∈ Finset.range k, Squarefree (x / b ^ l))).card

Sources

• Steven J. Miller, Fei Peng, Tudor Popescu, Joshua M. Siktar, and Nawapan Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Definition 3.6.

Used by 2

Used byBounds on the binary expected square-free walk length · Small counts of right-truncatable square-free numbers

TheoremSmall counts of right-truncatable square-free numbers#✓fully proved

Let \(L_{b,k}\) denote the number of right-truncatable square-free numbers with exactly \(k\) digits in base \(b\). Then \(L_{2,1} = 1\), \(L_{2,2} = 2\), \(L_{2,3} = 3\), \(L_{2,4} = 5\) and \(L_{10,1} = 6\).

public theorem rightTruncSquarefreeCount_small :
    rightTruncSquarefreeCount 2 1 = 1 ∧ rightTruncSquarefreeCount 2 2 = 2 ∧
      rightTruncSquarefreeCount 2 3 = 3 ∧ rightTruncSquarefreeCount 2 4 = 5 ∧
      rightTruncSquarefreeCount 10 1 = 6

Sources

• Miller, Peng, Popescu, Siktar, and Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, proofs of Theorems 3.8 and 3.9.

Uses 1

Statement usesCounting right-truncatable square-free numbers

TheoremBounds on the binary expected square-free walk length#●ready to prove

Let \(L_{2,k}\) denote the number of right-truncatable square-free numbers with exactly \(k\) digits in base \(2\). The real series \(E_2 = \sum_{k \ge 1} L_{2,k} / 2^k\) satisfies \(636163720502 / 2^{38} \le E_2 \le 636163930777 / 2^{38}\).

This is the series the proof of Theorem 3.8 uses. The paper's Lemma 3.7 prints the denominators \(b^k - b^{k-1}\), which for \(b = 2\) would double the sum.

public theorem_wanted binary_squarefree_walk_expectation_bounds :
    (636163720502 : ℝ) / 2 ^ 38 ≤
        ∑' k : ℕ, (rightTruncSquarefreeCount 2 (k + 1) : ℝ) / 2 ^ (k + 1) ∧
      ∑' k : ℕ, (rightTruncSquarefreeCount 2 (k + 1) : ℝ) / 2 ^ (k + 1) ≤
        (636163930777 : ℝ) / 2 ^ 38

Sources

• Steven J. Miller, Fei Peng, Tudor Popescu, Joshua M. Siktar, and Nawapan Wattanawanichkul, Walking to Infinity Along Some Number Theory Sequences, INTEGERS 24 (2024), Article A78, Theorem 3.8.

Uses 1

Statement usesCounting right-truncatable square-free numbers

7 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.