FormalConjectures.ErdosProblems.«409»

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 409

Reference: erdosproblems.com/409

open scoped Topology ArithmeticFunction.sigma Natopen Filternamespace Erdos409

How many iterations of $n\mapsto\phi(n) + 1$ are needed before a prime is reached?

-- Formalisation note: the sequence of iterates always terminates if `n > 0`
-- since it is strictly decreasing unless the input is prime, at which point
-- it becomes static. See also https://oeis.org/A39651
@[category research open, AMS 11]
theorem erdos_409.parts.i (n : ℕ) (hn : 0 < n) :
    IsLeast { i | (φ · + 1)^[i] n |>.Prime } answer(sorry) := byn:ℕhn:0 < n⊢ IsLeast {i | Nat.Prime ((fun x ↦ φ x + 1)^[i] n)} sorry
  sorryAll goals completed! 🐙

If $n > 0$, then the iteration $n\mapsto\phi(n) + 1$ necessarily reaches a prime.


@[category test, AMS 11]
theorem erdos_409.variants.termination (n : ℕ) (hn : 0 < n) :
    ∃ i, (φ · + 1)^[i] n |>.Prime := byn:ℕhn:0 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
  induction n using Nat.strong_induction_on with
  | _ n ih =>hn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
    by_cases hp : n.Primeposn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:Nat.Prime n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)negn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
    ·posn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:Nat.Prime n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n) exact ⟨0, byn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:Nat.Prime n⊢ Nat.Prime ((fun x ↦ φ x + 1)^[0] n) simpa using hpAll goals completed! 🐙⟩
    ·negn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n) have h1 : n = 1 ∨ 1 < n := byn:ℕhn:0 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)negn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:n = 1 ∨ 1 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n) omeganegn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:n = 1 ∨ 1 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)negn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:n = 1 ∨ 1 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
      rcases h1 with h1 | h1neg.inln:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:n = 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
      ·neg.inln:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:n = 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n) subst h1neg.inlih:∀ m < 1, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < 1hp:¬Nat.Prime 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] 1)
        refine ⟨1, ?_⟩neg.inlih:∀ m < 1, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < 1hp:¬Nat.Prime 1⊢ Nat.Prime ((fun x ↦ φ x + 1)^[1] 1)
        norm_num [Function.iterate_one, Nat.totient_one]All goals completed! 🐙
      ·neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n) have hlt : φ n < n := Nat.totient_lt n h1neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
        have hne : φ n ≠ n - 1 := byn:ℕhn:0 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
          intro hn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nh:φ n = n - 1⊢ Falseneg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
          exact hp ((Nat.totient_eq_iff_prime hn).1 h)neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
        have hdec : φ n + 1 < n := byn:ℕhn:0 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n) omeganeg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
        have hpos : 0 < φ n + 1 := byn:ℕhn:0 < n⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < nhpos:0 < φ n + 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n) positivityneg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < nhpos:0 < φ n + 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < nhpos:0 < φ n + 1⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
        obtain ⟨i, hi⟩ := ih (φ n + 1) hdec hposneg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < nhpos:0 < φ n + 1i:ℕhi:Nat.Prime ((fun x ↦ φ x + 1)^[i] (φ n + 1))⊢ ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] n)
        refine ⟨i + 1, ?_⟩neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < nhpos:0 < φ n + 1i:ℕhi:Nat.Prime ((fun x ↦ φ x + 1)^[i] (φ n + 1))⊢ Nat.Prime ((fun x ↦ φ x + 1)^[i + 1] n)
        rw [Function.iterate_succ_applyneg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < nhpos:0 < φ n + 1i:ℕhi:Nat.Prime ((fun x ↦ φ x + 1)^[i] (φ n + 1))⊢ Nat.Prime ((fun x ↦ φ x + 1)^[i] (φ n + 1))neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < nhpos:0 < φ n + 1i:ℕhi:Nat.Prime ((fun x ↦ φ x + 1)^[i] (φ n + 1))⊢ Nat.Prime ((fun x ↦ φ x + 1)^[i] (φ n + 1))]neg.inrn:ℕih:∀ m < n, 0 < m → ∃ i, Nat.Prime ((fun x ↦ φ x + 1)^[i] m)hn:0 < nhp:¬Nat.Prime nh1:1 < nhlt:φ n < nhne:φ n ≠ n - 1hdec:φ n + 1 < nhpos:0 < φ n + 1i:ℕhi:Nat.Prime ((fun x ↦ φ x + 1)^[i] (φ n + 1))⊢ Nat.Prime ((fun x ↦ φ x + 1)^[i] (φ n + 1))
        exact hiAll goals completed! 🐙

Let $c(n)$ be the minimum number of iterations of $n\mapsto\phi(n) + 1$ before a prime is reached. What is $\Theta(c(n))$?

@[category research open, AMS 11]
theorem erdos_409.parts.i.isTheta (c : ℕ → ℕ)
    (h : ∀ n > 0, IsLeast { i | (φ · + 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) := byc:ℕ → ℕh:∀ n > 0, IsLeast {i | Nat.Prime ((fun x ↦ φ x + 1)^[i] n)} (c n)⊢ (fun n ↦ ↑(c n)) =Θ[atTop] sorry
  sorryAll goals completed! 🐙

Let $c(n)$ be the minimum number of iterations of $n\mapsto\phi(n) + 1$ before a prime is reached. Find the simplest function $g(n)$ such that $c(n) = O(g(n))$?

@[category research open, AMS 11]
theorem erdos_409.parts.i.isBigO (c : ℕ → ℕ)
    (h : ∀ n > 0, IsLeast { i | (φ · + 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =O[atTop] (answer(sorry) : ℕ → ℝ) := byc:ℕ → ℕh:∀ n > 0, IsLeast {i | Nat.Prime ((fun x ↦ φ x + 1)^[i] n)} (c n)⊢ (fun n ↦ ↑(c n)) =O[atTop] sorry
  sorryAll goals completed! 🐙

Let $c(n)$ be the minimum number of iterations of $n\mapsto\phi(n) + 1$ before a prime is reached. Find the simplest function $g(n)$ such that $c(n) = o(g(n))$?

@[category research open, AMS 11]
theorem erdos_409.parts.i.isLittleO (c : ℕ → ℕ)
    (h : ∀ n > 0, IsLeast { i | (φ · + 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =o[atTop] (answer(sorry) : ℕ → ℝ) := byc:ℕ → ℕh:∀ n > 0, IsLeast {i | Nat.Prime ((fun x ↦ φ x + 1)^[i] n)} (c n)⊢ (fun n ↦ ↑(c n)) =o[atTop] sorry
  sorryAll goals completed! 🐙

Can infinitely many $n$ reach the same prime under the iteration $n\mapsto\phi(n) + 1$?

@[category research open, AMS 11]
theorem erdos_409.parts.ii :
    answer(sorry) ↔ ∃ (p : ℕ) (hp : p.Prime), { n | ∃ i, (φ · + 1)^[i] n = p }.Infinite := by⊢ True ↔ ∃ p, ∃ (_ : Nat.Prime p), {n | ∃ i, (fun x ↦ φ x + 1)^[i] n = p}.Infinite
  sorryAll goals completed! 🐙

What is the density of $n$ which reach any fixed prime under the iteration $n\mapsto\phi(n) + 1$?

@[category research open, AMS 11]
theorem erdos_409.parts.iii (p : ℕ) (h : p.Prime) (α : ℝ)
    (hα : { n | ∃ i, (φ · + 1)^[i] n = p }.HasDensity α) :
    α = answer(sorry) := byp:ℕh:Nat.Prime pα:ℝhα:{n | ∃ i, (fun x ↦ φ x + 1)^[i] n = p}.HasDensity α⊢ α = sorry
  sorryAll goals completed! 🐙

How many iterations of $n\mapsto\sigma(n) - 1$ are needed before a prime is reached?

-- Formalisation note: non-termination of this sequence is less clear since
-- it is strictly increasing except at primes.
@[category research open, AMS 11]
theorem erdos_409.variants.sigma (n : ℕ) (hn : n > 1) :
    IsLeast { i | (σ 1 · - 1)^[i] n |>.Prime } answer(sorry) := byn:ℕhn:n > 1⊢ IsLeast {i | Nat.Prime ((fun x ↦ (σ 1) x - 1)^[i] n)} sorry
  sorryAll goals completed! 🐙

If $n > 1$ then the iteration $n\mapsto\sigma(n) - 1$ necessarily reaches a prime. Note: this is open — it is not clear that the σ iteration always terminates, since it is non-decreasing (unlike the φ iteration which is strictly decreasing).

@[category research open, AMS 11]
theorem erdos_409.variants.sigma_termination (n : ℕ) (hn : n > 1) :
    ∃ i, (σ 1 · - 1)^[i] n |>.Prime := byn:ℕhn:n > 1⊢ ∃ i, Nat.Prime ((fun x ↦ (σ 1) x - 1)^[i] n)
  sorryAll goals completed! 🐙

Let $c(n)$ be the minimum number of iterations of $n\mapsto\sigma(n) - 1$ before a prime is reached. What is $\Theta(c(n))$?

@[category research open, AMS 11]
theorem erdos_409.variants.sigma_isTheta (c : ℕ → ℕ)
    (h : ∀ n > 1, IsLeast { i | (σ 1 · - 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) := byc:ℕ → ℕh:∀ n > 1, IsLeast {i | Nat.Prime ((fun x ↦ (σ 1) x - 1)^[i] n)} (c n)⊢ (fun n ↦ ↑(c n)) =Θ[atTop] sorry
  sorryAll goals completed! 🐙

Let $c(n)$ be the minimum number of iterations of $n\mapsto\sigma(n) - 1$ before a prime is reached. Find the simplest function $g(n)$ such that $c(n) = O(g(n))$?

@[category research open, AMS 11]
theorem erdos_409.variants.sigma_isBigO (c : ℕ → ℕ)
    (h : ∀ n > 1, IsLeast { i | (σ 1 · - 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =O[atTop] (answer(sorry) : ℕ → ℝ) := byc:ℕ → ℕh:∀ n > 1, IsLeast {i | Nat.Prime ((fun x ↦ (σ 1) x - 1)^[i] n)} (c n)⊢ (fun n ↦ ↑(c n)) =O[atTop] sorry
  sorryAll goals completed! 🐙

Let $c(n)$ be the minimum number of iterations of $n\mapsto\sigma(n) - 1$ before a prime is reached. Find the simplest function $g(n)$ such that $c(n) = o(g(n))$?

@[category research open, AMS 11]
theorem erdos_409.variants.sigma_isLittleO (c : ℕ → ℕ)
    (h : ∀ n > 1, IsLeast { i | (σ 1 · - 1)^[i] n |>.Prime } (c n)) :
    (fun n => (c n : ℝ)) =o[atTop] (answer(sorry) : ℕ → ℝ) := byc:ℕ → ℕh:∀ n > 1, IsLeast {i | Nat.Prime ((fun x ↦ (σ 1) x - 1)^[i] n)} (c n)⊢ (fun n ↦ ↑(c n)) =o[atTop] sorry
  sorryAll goals completed! 🐙

Is it true that iterates of $n\mapsto\sigma(n) - 1$ always reach a prime?

@[category research open, AMS 11]
theorem erdos_409.variants.sigma_prime_termination :
    answer(sorry) ↔ ∀ n > 1, ∃ i, (σ 1 · - 1)^[i] n |>.Prime := by⊢ True ↔ ∀ n > 1, ∃ i, Nat.Prime ((fun x ↦ (σ 1) x - 1)^[i] n)
  sorryAll goals completed! 🐙

end Erdos409