IMO 2024 Q6

A function f: ℚ → ℚ is called aquaesulian if the following property holds: for every x, y ∈ ℚ, f(x + f(y)) = f(x) + y or f(f(x) + y) = x + f(y).

Show that there exists an integer c such that for any aquaesulian function f there are at most c different rational numbers of the form f(r)+f(-r) for some rational number r, and find the smallest possible value of c.

We follow Solution 1 from the official solutions. A key observation is that f(-f(-x)) = x. We then consider a pair of distinct nonzero values of f(x)+f(-x), and a series of manipulations together with the previous observation result in a contradiction, so there are at most two values of f(x)+f(-x). All this works over any AddCommGroup; over ℚ, we then show that ⌊x⌋ - Int.fract x achieves two different values of f(x)+f(-x).

def Imo2024Q6.General.Aquaesulian {G : Type u_1} [AddCommGroup G] (f : G → G) : Prop

The condition on functions in the problem (for a general AddCommGroup and in symmetric form).

Equations

• Imo2024Q6.General.Aquaesulian f = ∀ (x y : G), f (f y + x) = f x + y ∨ f (f x + y) = f y + x

theorem Imo2024Q6.General.Aquaesulian.apply_apply_add {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) (x : G) : f (f x + x) = f x + x

theorem Imo2024Q6.General.Aquaesulian.eq_of_apply_eq_inl {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) {x₁ x₂ : G} (he : f x₁ = f x₂) (hc : f (f x₁ + x₂) = f x₂ + x₁) : x₁ = x₂

theorem Imo2024Q6.General.Aquaesulian.injective {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) : Function.Injective f

@[simp]

theorem Imo2024Q6.General.Aquaesulian.apply_zero {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) : f 0 = 0

@[simp]

theorem Imo2024Q6.General.Aquaesulian.apply_neg_apply_add {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) (x : G) : f (-f x) + x = 0

@[simp]

theorem Imo2024Q6.General.Aquaesulian.apply_neg_apply {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) (x : G) : f (-f x) = -x

theorem Imo2024Q6.General.Aquaesulian.apply_neg_apply_neg {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) (x : G) : f (-f (-x)) = x

theorem Imo2024Q6.General.Aquaesulian.apply_neg_of_apply_eq {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) {x₁ x₂ : G} (hx : f x₁ = x₂) : f (-x₂) = -x₁

theorem Imo2024Q6.General.Aquaesulian.apply_neg_eq_neg_iff {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) {x₁ x₂ : G} : f (-x₂) = -x₁ ↔ f x₁ = x₂

theorem Imo2024Q6.General.Aquaesulian.pair_lemma {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) {x u v : G} (huv : u ≠ v) (hx : f x = u ∨ f u = x) (hy : f x = v ∨ f v = x) : f x = v ∨ f x = u

theorem Imo2024Q6.General.Aquaesulian.g_two {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) {x y u v : G} (huv : u ≠ v) (hx : f x + f (-x) = u) (hy : f y + f (-y) = v) : f (x + y) = -f (-x) + -f (-y) + v ∨ f (x + y) = -f (-x) + -f (-y) + u

theorem Imo2024Q6.General.Aquaesulian.u_eq_zero {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) {x y u v : G} (huv : u ≠ v) (hx : f x + f (-x) = u) (hy : f y + f (-y) = v) (hxyv : f (x + y) = -f (-x) + -f (-y) + v) : u = 0

theorem Imo2024Q6.General.Aquaesulian.u_eq_zero_or_v_eq_zero {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) {x y u v : G} (huv : u ≠ v) (hx : f x + f (-x) = u) (hy : f y + f (-y) = v) : u = 0 ∨ v = 0

theorem Imo2024Q6.General.Aquaesulian.card_le_two {G : Type u_1} [AddCommGroup G] {f : G → G} (h : Aquaesulian f) : Cardinal.mk ↑(Set.range fun (x : G) => f x + f (-x)) ≤ 2

def Imo2024Q6.Aquaesulian (f : ℚ → ℚ) : Prop

The condition on functions in the problem (for ℚ and in the original form).

Equations

• Imo2024Q6.Aquaesulian f = ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y

theorem Imo2024Q6.aquaesulian_iff_general {f : ℚ → ℚ} : Aquaesulian f ↔ General.Aquaesulian f

theorem Imo2024Q6.Aquaesulian.card_le_two {f : ℚ → ℚ} (h : Aquaesulian f) : Cardinal.mk ↑(Set.range fun (x : ℚ) => f x + f (-x)) ≤ 2

def Imo2024Q6.fExample (x : ℚ) : ℚ

An example of a function achieving the maximum number of values of f(r)+f(-r).

Equations

• Imo2024Q6.fExample x = ↑⌊x⌋ - Int.fract x

theorem Imo2024Q6.fExample_add (x y : ℚ) : fExample x + y = ↑⌊x⌋ + ↑⌊y⌋ + (Int.fract y - Int.fract x)

theorem Imo2024Q6.add_fExample (x y : ℚ) : x + fExample y = ↑⌊x⌋ + ↑⌊y⌋ + (Int.fract x - Int.fract y)

theorem Imo2024Q6.fExample_intCast_add (x : ℤ) (y : ℚ) : fExample (↑x + y) = ↑x + fExample y

theorem Imo2024Q6.fExample_of_mem_Ico {x : ℚ} (h : x ∈ Set.Ico 0 1) : fExample x = -x

theorem Imo2024Q6.apply_fExample_add_apply_of_fract_le {x y : ℚ} (h : Int.fract y ≤ Int.fract x) : fExample (x + fExample y) = fExample x + y

theorem Imo2024Q6.aquaesulian_fExample : Aquaesulian fExample

theorem Imo2024Q6.fract_fExample (x : ℚ) : Int.fract (fExample x) = if Int.fract x = 0 then 0 else 1 - Int.fract x

theorem Imo2024Q6.floor_fExample (x : ℚ) : ↑⌊fExample x⌋ = if Int.fract x = 0 then x else ↑⌊x⌋ - 1

theorem Imo2024Q6.card_range_fExample : Cardinal.mk ↑(Set.range fun (x : ℚ) => fExample x + fExample (-x)) = 2

theorem imo2024q6 : (∀ (f : ℚ → ℚ), Imo2024Q6.Aquaesulian f → Cardinal.mk ↑(Set.range fun (x : ℚ) => f x + f (-x)) ≤ ↑2) ∧ ∀ (c : ℕ), (∀ (f : ℚ → ℚ), Imo2024Q6.Aquaesulian f → Cardinal.mk ↑(Set.range fun (x : ℚ) => f x + f (-x)) ≤ ↑c) → 2 ≤ c

The answer 2 is to be determined by the solver of the original problem.