IMO 2009 C2

For each $n ∈ ℕ$, find the largest integer $k$ such that there exist $k$ triples $(a_1, b_1, c_1), …, (a_k, b_k, c_k)$ with the following properties:

• $a_i + b_i + c_i = n$ for all $i ≤ k$;
• for any $i ≠ j$, we have $a_i ≠ a_j$, $b_i ≠ b_j$, and $c_i ≠ c_j$.

Answer

$⌊2n/3⌋ + 1$.

Solution

We follow the official solution.

Extra lemmas

theorem IMOSL.IMO2009C2.card_choose_le_nat_sum (S : Finset ℕ) : S.card.choose 2 ≤ ∑ s ∈ S, s

For any finite set S ⊆ ℕ, the sum of all elements of S is at least C(#S, 2).

theorem IMOSL.IMO2009C2.card_choose_le_sum_of_inj {ι : Type u_1} {f : ι → ℕ} (hf : Function.Injective f) (I : Finset ι) : I.card.choose 2 ≤ ∑ i ∈ I, f i

If f : ι → ℕ is injective, thenf or any finite set I ⊆ ι, the sum of f(i) across all i ∈ I is at least C(#I, 2).

theorem IMOSL.IMO2009C2.fin_cast_sub_two_mul_injective (k : ℕ) : Function.Injective fun (i : Fin k) => 2 * (k - 1 - ↑i)

The map f : Fin k → ℕ defined by f(i) = 2(k - i - 1) is injective.

Start of the problem

structure IMOSL.IMO2009C2.GoodTripleFn (n : ℕ) (ι : Type u_1) : Type u_1

A collection ((x_{0i}, x_{1i}, x_{2i}))_{i ∈ ι} of triples is called n-good if x_{ji} ≠ x_{ji'} whenever i ≠ i' and x_{0i} + x_{1i} + x_{2i} = n for all i.

• toFun : Fin 3 → ι → ℕ
• toFun_inj (j : Fin 3) : Function.Injective (self.toFun j)
• toFun_sum (i : ι) : ∑ j : Fin 3, self.toFun j i = n

def IMOSL.IMO2009C2.GoodTripleFn.ofEmbedding {κ : Type u_1} {ι : Type u_2} {n : ℕ} (f : κ ↪ ι) (X : GoodTripleFn n ι) : GoodTripleFn n κ

Subcollection of an n-good collection, which is also an n-good collection.

Equations

• IMOSL.IMO2009C2.GoodTripleFn.ofEmbedding f X = { toFun := fun (j : Fin 3) (k : κ) => X.toFun j (f k), toFun_inj := ⋯, toFun_sum := ⋯ }

theorem IMOSL.IMO2009C2.GoodTripleFn.nonempty_of_card_le {ι : Type u_1} {κ : Type u_2} {n : ℕ} [Fintype ι] [Fintype κ] (hι : Nonempty (GoodTripleFn n ι)) (h : Fintype.card κ ≤ Fintype.card ι) : Nonempty (GoodTripleFn n κ)

If there is an ι-indexed n-good collection and |κ| ≤ |ι|, then there is also a κ-indexed n-good collection.

theorem IMOSL.IMO2009C2.GoodTripleFn.card_bound {ι : Type u_1} {n : ℕ} [Fintype ι] (X : GoodTripleFn n ι) : Fintype.card ι ≤ 2 * n / 3 + 1

If there is an ι-indexed n-good collection, then |ι| ≤ 2n/3 + 1.

def IMOSL.IMO2009C2.GoodTripleFn.add_val {n : ℕ} {ι : Type u_1} (X : GoodTripleFn n ι) (j₀ : Fin 3) (v : ℕ) : GoodTripleFn (n + v) ι

Creating a new n-good collection by adding a fixed value to a fixed coordinate.

Equations

• X.add_val j₀ v = { toFun := fun (j : Fin 3) (i : ι) => X.toFun j i + if j = j₀ then v else 0, toFun_inj := ⋯, toFun_sum := ⋯ }

def IMOSL.IMO2009C2.GoodTripleFn.default_of_0mod3 (k : ℕ) : GoodTripleFn (3 * k) (Fin (k + 1) ⊕ Fin k)

Construction of a 3k-good collection of 2k + 1 triples.

Equations

• One or more equations did not get rendered due to their size.

def IMOSL.IMO2009C2.GoodTripleFn.default_of_1mod3 (k : ℕ) : GoodTripleFn (3 * k + 1) (Fin (k + 1) ⊕ Fin k)

Construction of a 3k + 1-good collection of 2k + 1 triples.

Equations

• IMOSL.IMO2009C2.GoodTripleFn.default_of_1mod3 k = (IMOSL.IMO2009C2.GoodTripleFn.default_of_0mod3 k).add_val 2 1

def IMOSL.IMO2009C2.GoodTripleFn.default_of_2mod3 (k : ℕ) : GoodTripleFn (3 * k + 2) (Fin (k + 1) ⊕ Fin (k + 1))

Construction of a 3k + 2-good collection of 2k + 2 triples.

Equations

• One or more equations did not get rendered due to their size.

theorem IMOSL.IMO2009C2.GoodTripleFn.nonempty_of_le_bound {ι : Type u_1} {n : ℕ} [Fintype ι] (h : Fintype.card ι ≤ 2 * n / 3 + 1) : Nonempty (GoodTripleFn n ι)

If |ι| ≤ 2n/3 + 1, then there is an ι-indexed n-good collection.

theorem IMOSL.IMO2009C2.GoodTripleFn.nonempty_iff {ι : Type u_1} {n : ℕ} [Fintype ι] : Nonempty (GoodTripleFn n ι) ↔ Fintype.card ι ≤ 2 * n / 3 + 1

There exists an ι-indexed n-good collection if and only if ι ≤ ⌊2n/3⌋ + 1.

theorem IMOSL.IMO2009C2.final_solution {n : ℕ} : IsGreatest {k : ℕ | Nonempty (GoodTripleFn n (Fin k))} (2 * n / 3 + 1)

Final solution