Juggler conjecture

Reference: Wikipedia

noncomputable def JugglerConjecture.jugglerStep (n : ℕ) : ℕ

Consider the following operation on the natural numbers: If the number is even, take the floor of the square root. If the number is odd, take the floor of n raised to the 3/2 power.

Equations

• JugglerConjecture.jugglerStep n = if Even n then ⌊↑n ^ (1 / 2)⌋₊ else ⌊↑n ^ (3 / 2)⌋₊

theorem JugglerConjecture.juggler_conjecture (n : ℕ) (hn : n > 0) : ∃ (m : ℕ), jugglerStep^[m] n = 1

Now form a sequence beginning with any positive integer, where each subsequent term is obtained by applying the operation defined above to the previous term. The Juggler Conjecture states that for any positive integer $n$, there exists a natural number $m$ such that the $m$-th term of the sequence is $1$.

theorem JugglerConjecture.jugglerStep_36 : jugglerStep 36 = 6

Example: jugglerStep 36 = ⌊36^(1/2)⌋ = ⌊6⌋ = 6 (since 36 is even).