IMO 2025 Q3

Let ℕ+ denote the set of positive integers. A function f : ℕ+ → ℕ+ is said to be bonza if f a ∣ b ^ a - (f b) ^ (f a) for all positive integers a and b. Determine the smallest real constant c such that f n ≤ c * n for all bonza functions f and all positive integers n.

Solution

We follow solution from https://web.evanchen.cc/exams/IMO-2025-notes.pdf.

We first plug in a = b = n to get the basic constraint ∀ n, f n ∣ n ^ n. Next, one shows that unless f is the identity, every odd prime must satisfy f p = 1. From here, any odd prime divisor of f n is ruled out by taking a = n, b = p, so f n is always a power of 2. Finally, evaluating a = n, b = 3 gives f n ∣ 3 ^ n - 1, and according to the LTE lemma, we have padicValNat 2 (3 ^ n - 1) = padicValNat 2 n + 2 for Even n. Therefore, f(n) ≤ 2 ^ (padicValNat 2 n + 2) ≤ 4 * n, so c=4 works.

A matching construction is f n = 1 for Odd n, f 4 = 16, and f n = 2 for other Even n, which attains the bound, showing the optimal answer is c = 4.

def Imo2025Q3.IsBonza : (ℕ → ℕ) → Prop

Define bonza functions

Equations

• Imo2025Q3.IsBonza f = ((∀ (a b : ℕ), 0 < a → 0 < b → ↑(f a) ∣ ↑b ^ a - ↑(f b) ^ f a) ∧ ∀ (n : ℕ), 0 < n → 0 < f n)

theorem Imo2025Q3.IsBonza.apply_dvd_pow {f : ℕ → ℕ} (hf : IsBonza f) {n : ℕ} (hn : 0 < n) : f n ∣ n ^ n

For each bonza function f, we have f n ∣ n ^ n

theorem Imo2025Q3.IsBonza.apply_prime_eq_one_or_dvd_self_sub_apply {f : ℕ → ℕ} (hf : IsBonza f) {p : ℕ} (hp : Nat.Prime p) : f p = 1 ∨ ∀ b > 0, ↑p ∣ ↑b - ↑(f b)

theorem Imo2025Q3.IsBonza.not_id_apply_prime_of_gt_eq_one {f : ℕ → ℕ} (hf : IsBonza f) (hnf : ¬∀ x > 0, f x = x) : ∃ (N : ℕ), ∀ p > N, Nat.Prime p → f p = 1

For each bonza function f, then f p = 1 for sufficient big prime p

theorem Imo2025Q3.IsBonza.apply_prime_gt_two_eq_one {f : ℕ → ℕ} (hf : IsBonza f) (hnf : ¬∀ x > 0, f x = x) (p : ℕ) : p > 2 → Nat.Prime p → f p = 1

theorem Imo2025Q3.IsBonza.not_id_two_pow {f : ℕ → ℕ} (hf : IsBonza f) (hnf : ¬∀ x > 0, f x = x) (n : ℕ) : 0 < n → ∃ (a : ℕ), f n = 2 ^ a

Therefore, if a bonza function is not identity, then every f x is a pow of two

def Imo2025Q3.fExample : ℕ → ℕ

An example of a bonza function achieving the maximum number of values of c.

Equations

• Imo2025Q3.fExample x = if ¬2 ∣ x then 1 else if x = 2 then 4 else 2 ^ (padicValNat 2 x + 2)

theorem Imo2025Q3.fExample.dvd_pow_sub {a b : ℕ} {x : ℤ} (hb : 2 ∣ b) (ha : a ≥ 4) (hx : 2 ∣ x) : 2 ^ (padicValNat 2 a + 2) ∣ ↑b ^ a - x ^ 2 ^ (padicValNat 2 a + 2)

theorem Imo2025Q3.fExample.isBonza : IsBonza fExample

To verify the example is a bonza function

theorem Imo2025Q3.fExample.apply_le {f : ℕ → ℕ} (hf : IsBonza f) {n : ℕ} (hn : 0 < n) : f n ≤ 4 * n

theorem Imo2025Q3.result : IsLeast {c : ℝ | ∀ (f : ℕ → ℕ), IsBonza f → ∀ (n : ℕ), 0 < n → ↑(f n) ≤ c * ↑n} 4