IMO 2012 A1 (P4)

A triple $(a, b, c)$ of integers is called a Heron triple if $$ a^2 + b^2 + c^2 = 2ab + 2bc + 2ca. $$ Find all functions $f : ℤ → ℤ$ such that $f(a), f(b), f(c))$ is a Heron triple for any $a, b, c ∈ ℤ$ satisfying $a + b + c = 0$.

Answer

They are precisely the functions of the following form:

• $f(n) = cn^2$;
• $f(n) = \begin{cases} c & \text{if } 2 ∤ n, \\ 0 & \text{if } 2 ∣ n, \end{cases}$;
• $f(n) = \begin{cases} c & \text{if } 2 ∤ n, \\ 4c & \text{if } n ≡ 2 \pmod{4}, \\ 0 & \text{if } 2 ∣ n. \end{cases}$

Solution

We follow the official solution. Our implementation is slightly more complicated at the final step in the case where $f(2) = 4f(1)$ and $f(3) = 9f(1)$, but it works even when the range of the function is generalized to any integral domain (of characteristic not equal to $3$). The difference is that $k(n - 1)^2 ≠ k(n - 3)^2$ is not always true this time, but $k(n - 1)^2 = k(n - 3)^2$ would imply either $k = 0$, $R$ has characteristic $2$, or $n = 2$ in $R$, and in all cases we still get $f(n + 1) = k(n + 1)^2$.

Heron triples

def IMOSL.IMO2012A1.HeronTriple {R : Type u_1} [CommSemiring R] (a b c : R) : Prop

A triple (a, b, c) ∈ R^3 is called a Heron triple if a^2 + b^2 + c^2 = 2ab + 2bc + 2ca.

Equations

• IMOSL.IMO2012A1.HeronTriple a b c = (a ^ 2 + b ^ 2 + c ^ 2 = 2 * (a * b + b * c + c * a))

instance IMOSL.IMO2012A1.HeronTriple.instDecidableOfDecidableEq {R : Type u_1} [CommSemiring R] [DecidableEq R] (a b c : R) : Decidable (HeronTriple a b c)

Equations

• IMOSL.IMO2012A1.HeronTriple.instDecidableOfDecidableEq a b c = decEq (a ^ 2 + b ^ 2 + c ^ 2) (2 * (a * b + b * c + c * a))

theorem IMOSL.IMO2012A1.HeronTriple.perm231 {R : Type u_1} [CommSemiring R] {a b c : R} (h : HeronTriple a b c) : HeronTriple b c a

If (a, b, c) is a Heron triple, then (b, c, a) is a Heron triple.

theorem IMOSL.IMO2012A1.HeronTriple.perm312 {R : Type u_1} [CommSemiring R] {a b c : R} (h : HeronTriple a b c) : HeronTriple c a b

If (a, b, c) is a Heron triple, then (c, a, b) is a Heron triple.

theorem IMOSL.IMO2012A1.HeronTriple.perm213 {R : Type u_1} [CommSemiring R] {a b c : R} (h : HeronTriple a b c) : HeronTriple b a c

If (a, b, c) is a Heron triple, then (b, a, c) is a Heron triple.

theorem IMOSL.IMO2012A1.HeronTriple.perm321 {R : Type u_1} [CommSemiring R] {a b c : R} (h : HeronTriple a b c) : HeronTriple c b a

If (a, b, c) is a Heron triple, then (c, b, a) is a Heron triple.

theorem IMOSL.IMO2012A1.HeronTriple.perm132 {R : Type u_1} [CommSemiring R] {a b c : R} (h : HeronTriple a b c) : HeronTriple a c b

If (a, b, c) is a Heron triple, then (a, c, b) is a Heron triple.

theorem IMOSL.IMO2012A1.HeronTriple.mul_left {R : Type u_1} [CommSemiring R] {a b c : R} (h : HeronTriple a b c) (r : R) : HeronTriple (r * a) (r * b) (r * c)

If (a, b, c) is a Heron triple, then (ra, rb, rc) is a Heron triple for any r.

theorem IMOSL.IMO2012A1.HeronTriple.reference_formula {R : Type u_1} [CommRing R] (a b c : R) : 2 * (a ^ 2 * b ^ 2 + b ^ 2 * c ^ 2 + c ^ 2 * a ^ 2) - ((a ^ 2) ^ 2 + (b ^ 2) ^ 2 + (c ^ 2) ^ 2) = (a + b - c) * (b + c - a) * (c + a - b) * (a + b + c)

The main formula which inspires the name "Heron triple": 2(a^2 b^2 + b^2 c^2 + c^2 a^2) - (a^4 + b^4 + c^4) is equal to (a + b - c)(b + c - a)(c + a - b)(a + b + c).

theorem IMOSL.IMO2012A1.HeronTriple.squares_of_add_eq_zero {R : Type u_1} [CommRing R] {a b c : R} (h : a + b + c = 0) : HeronTriple (a ^ 2) (b ^ 2) (c ^ 2)

The triple (a^2, b^2, c^2) is a Heron triple if a + b + c = 0.

theorem IMOSL.IMO2012A1.HeronTriple.eq_zero_of_const {R : Type u_1} [CommRing R] [NoZeroDivisors R] (hR : 3 ≠ 0) {c : R} (hc : HeronTriple c c c) : c = 0

If char(R) ≠ 3 and (x, x, x) is a Heron triple, then x = 0.

theorem IMOSL.IMO2012A1.HeronTriple.iff_eq_of_zero_right {R : Type u_1} [CommRing R] [NoZeroDivisors R] {x y : R} : HeronTriple x y 0 ↔ x = y

The triple (x, y, 0) is a Heron triple if and only if x = y.

theorem IMOSL.IMO2012A1.HeronTriple.iff_eq_mul_add_or_sub_sq {R : Type u_1} [CommRing R] [NoZeroDivisors R] {r x y z : R} : HeronTriple (r * x ^ 2) (r * y ^ 2) z ↔ z = r * (x + y) ^ 2 ∨ z = r * (x - y) ^ 2

The triple (rx^2, ry^2, z) is a Heron triple if and only if either z = r(x + y)^2 or z = r(x - y)^2.

theorem IMOSL.IMO2012A1.HeronTriple.iff_of_left_mid_eq {R : Type u_1} [CommRing R] [NoZeroDivisors R] {r z : R} : HeronTriple r r z ↔ z = r * 2 ^ 2 ∨ z = 0

The triple (r, r, z) is a Heron triple if and only if z = 4r or z = 0.

Start of the problem

def IMOSL.IMO2012A1.good {G : Type u_1} {R : Type u_2} [AddZero G] [CommSemiring R] (f : G → R) : Prop

A function f : G → R is called good if (f(a), f(b), f(c)) is a Heron triple whenever a, b, c ∈ G satisfies a + b + c = 0.

Equations

• IMOSL.IMO2012A1.good f = ∀ (a b c : G), a + b + c = 0 → IMOSL.IMO2012A1.HeronTriple (f a) (f b) (f c)

instance IMOSL.IMO2012A1.instDecidableGoodOfFintypeOfDecidableEq {G : Type u_1} {R : Type u_2} [DecidableEq G] [Fintype G] [AddZero G] [CommSemiring R] [DecidableEq R] (f : G → R) : Decidable (good f)

Equations

• IMOSL.IMO2012A1.instDecidableGoodOfFintypeOfDecidableEq f = Fintype.decidableForallFintype

theorem IMOSL.IMO2012A1.sq_is_good {R : Type u_1} [CommRing R] : good fun (r : R) => r ^ 2

The square function is good.

theorem IMOSL.IMO2012A1.ZMod2_01_is_good : good ![0, 1]

The function f : ZMod 2 → ℤ defined by f(0) = 0 and f(1) = 1 is good.

theorem IMOSL.IMO2012A1.ZMod4_0141_is_good : good ![0, 1, 4, 1]

The function f : ZMod 4 → ℤ defined by 0 ↦ 0, 1 ↦ 1, 2 ↦ 4, 3 ↦ 1 is good.

theorem IMOSL.IMO2012A1.good.alt_def {G : Type u_1} {R : Type u_2} [AddGroup G] [CommSemiring R] {f : G → R} (hf : good f) (a b : G) : HeronTriple (f a) (f b) (f (-(a + b)))

An alternative definition of good function when G is a group.

theorem IMOSL.IMO2012A1.good.smul_left {G : Type u_1} {R : Type u_2} [AddZero G] [CommSemiring R] {f : G → R} (hf : good f) (r : R) : good (r • f)

If f : G → R is good, then the function rf : x ↦ rf(x) is good for any r : R.

theorem IMOSL.IMO2012A1.good.comp_AddMonoidHom {G₀ : Type u_1} {G : Type u_2} {R : Type u_3} [AddZero G₀] [AddZero G] [CommSemiring R] {f : G → R} (hf : good f) (φ : G₀ →+ G) : good (f ∘ ⇑φ)

If f : G → R is good and φ : G₀ → G is a group homomorphism, f ∘ φ is good.

theorem IMOSL.IMO2012A1.good.map_zero_of_three_ne_zero {G : Type u_2} {R : Type u_1} [AddGroup G] [CommRing R] [NoZeroDivisors R] (hR : 3 ≠ 0) {f : G → R} (hf : good f) : f 0 = 0

Suppose that char(R) ≠ 3. If f : G → R is good then f(0) = 0.

theorem IMOSL.IMO2012A1.good.map_neg_of_map_zero {G : Type u_2} {R : Type u_1} [AddGroup G] [CommRing R] [NoZeroDivisors R] {f : G → R} (hf : good f) (hf0 : f 0 = 0) (x : G) : f (-x) = f x

If f : G → R is good with f(0) = 0 then f is even.

theorem IMOSL.IMO2012A1.good.def_of_map_zero {G : Type u_2} {R : Type u_1} [AddGroup G] [CommRing R] [NoZeroDivisors R] {f : G → R} (hf : good f) (hf0 : f 0 = 0) (x y : G) : HeronTriple (f x) (f y) (f (x + y))

If f : G → R is good with f(0) = 0 then (f(x), f(y), f(x + y)) is a Heron triple for any x, y : G.

theorem IMOSL.IMO2012A1.good.map_add_of_map_eq_zero {G : Type u_2} {R : Type u_1} [AddGroup G] [CommRing R] [NoZeroDivisors R] {f : G → R} (hf : good f) (hf0 : f 0 = 0) {c : G} (hc : f c = 0) (x : G) : f (x + c) = f x

If f : G → R is good with f(0) = 0 and c : G satisfies f(c) = 0, then f(x + c) = f(x) for any x : G.

theorem IMOSL.IMO2012A1.good.map_nsmul_of_map_eq_zero {G : Type u_2} {R : Type u_1} [AddGroup G] [CommRing R] [NoZeroDivisors R] {f : G → R} (hf : good f) (hf0 : f 0 = 0) {c : G} (hc : f c = 0) (n : ℤ) : f (n • c) = 0

If f : G → R is good with f(0) = 0 and c : G satisfies f(c) = 0, then f(nc) = 0 for every integer n.

theorem IMOSL.IMO2012A1.good.Int_map_ZMod_of_map_eq_zero {R : Type u_1} [CommRing R] [NoZeroDivisors R] {f : ℤ → R} (hf : good f) (hf0 : f 0 = 0) {N : ℕ} [NeZero N] (hN : f ↑N = 0) (n : ℤ) : f ↑(↑n).val = f n

If f(0) = 0 and f(N) = 0 for some N : ℕ nonzero, then for any n : ℕ, we have f(n) = f(x) where x is the image of n in Fin N.

theorem IMOSL.IMO2012A1.good.Int_map_two_eq {R : Type u_1} [CommRing R] [NoZeroDivisors R] {f : ℤ → R} (hf : good f) (hf0 : f 0 = 0) : f 2 = f 1 * 2 ^ 2 ∨ f 2 = 0

If f(0) = 0, then f(2) is equal to either 4 f(1) or 0.

theorem IMOSL.IMO2012A1.good.Int_eq_smul_ZMod2_01_of_map_two {R : Type u_1} [CommRing R] [NoZeroDivisors R] {f : ℤ → R} (hf : good f) (hf0 : f 0 = 0) (hf1 : f 2 = 0) : f = fun (n : ℤ) => f 1 * ![0, 1] ↑n

If f(0) = f(2) = 0, then f(n) = f(1) if n is odd and f(n) = 0 if n is even.

theorem IMOSL.IMO2012A1.good.Int_map_three_eq_of_map_two {R : Type u_1} [CommRing R] [NoZeroDivisors R] {f : ℤ → R} (hf : good f) (hf0 : f 0 = 0) (hf1 : f 2 = f 1 * 2 ^ 2) : f 3 = f 1 * 3 ^ 2 ∨ f 3 = f 1

If f(0) = 0 0 and f(2) = 4 f(1), then f(3) is either 9 f(1) or f(1).

theorem IMOSL.IMO2012A1.good.Int_eq_smul_sq_of_map_three {R : Type u_1} [CommRing R] [NoZeroDivisors R] {f : ℤ → R} (hf : good f) (hf0 : f 0 = 0) (hf1 : f 2 = f 1 * 2 ^ 2) (hf2 : f 3 = f 1 * 3 ^ 2) : f = fun (n : ℤ) => f 1 * ↑n ^ 2

If f(0) = 0, f(2) = 4 f(1), and f(3) = 9 f(1), then f(n) = f(1) n^2 for all integers n.

theorem IMOSL.IMO2012A1.good.Int_eq_smul_ZMod4_0141_of_map_three {R : Type u_1} [CommRing R] [NoZeroDivisors R] (hR : 3 ≠ 0) {f : ℤ → R} (hf : good f) (hf0 : f 2 = f 1 * 2 ^ 2) (hf1 : f 3 = f 1) : f = fun (n : ℤ) => f 1 * ![0, 1, 4, 1] ↑n

If char(R) ≠ 3, f(2) = 4 f(1), and f(3) = f(1), then f(n) = f(1) if n is odd, f(n) = 4f(1) if n ≡ 2 (mod 4), and f(n) = 0 if 4 ∣ n.

theorem IMOSL.IMO2012A1.final_solution {f : ℤ → ℤ} : good f ↔ (∃ (c : ℤ), f = fun (n : ℤ) => c * ![0, 1] ↑n) ∨ (∃ (c : ℤ), f = fun (n : ℤ) => c * ![0, 1, 4, 1] ↑n) ∨ ∃ (c : ℤ), f = fun (n : ℤ) => c * n ^ 2

Final solution