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 Nat

open Filter


namespace 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 declaration uses 'sorry'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) omegaAll goals completed! 🐙
      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 := Nat.totient_lt n h1⊢ ∃ 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)
          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 < n := Nat.totient_lt n h1h:φ n = n - 1⊢ False
          exact hp ((Nat.totient_eq_iff_prime hn).1 h)All goals completed! 🐙
        have hdec : φ n + 1 < n := byn:ℕhn:0 < n⊢ ∃ i, Nat.Prime ((fun x => φ x + 1)^[i] n) omegaAll goals completed! 🐙
        have hpos : 0 < φ n + 1 := byn:ℕhn:0 < n⊢ ∃ i, Nat.Prime ((fun x => φ x + 1)^[i] n) positivityAll goals completed! 🐙
        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 < n := Nat.totient_lt n h1hne:φ n ≠ n - 1 := fun h => hp ((Nat.totient_eq_iff_prime hn).mp h)hdec:φ n + 1 < n := Decidable.byContradiction fun a => termination._proof_2 n h1 hlt hne ahpos:0 < φ n + 1 := 
  add_pos' (Nat.totient_pos.mpr hn)
    (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1)))i:ℕ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 < n := Nat.totient_lt n h1hne:φ n ≠ n - 1 := fun h => hp ((Nat.totient_eq_iff_prime hn).mp h)hdec:φ n + 1 < n := Decidable.byContradiction fun a => termination._proof_2 n h1 hlt hne ahpos:0 < φ n + 1 := 
  add_pos' (Nat.totient_pos.mpr hn)
    (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1)))i:ℕhi:Nat.Prime ((fun x => φ x + 1)^[i] (φ n + 1))⊢ Nat.Prime ((fun x => φ x + 1)^[i + 1] n)
        rw [Function.iterate_succ_apply]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 < n := Nat.totient_lt n h1hne:φ n ≠ n - 1 := fun h => hp ((Nat.totient_eq_iff_prime hn).mp h)hdec:φ n + 1 < n := Decidable.byContradiction fun a => termination._proof_2 n h1 hlt hne ahpos:0 < φ n + 1 := 
  add_pos' (Nat.totient_pos.mpr hn)
    (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1)))i:ℕ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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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 declaration uses 'sorry'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