IMO 1981 Q3 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Determine the maximum value of m ^ 2 + n ^ 2, where m and n are integers in {1, 2, ..., 1981} and (n ^ 2 - m * n - m ^ 2) ^ 2 = 1.

The trick to this problem is that m and n have to be consecutive Fibonacci numbers, because you can reduce any solution to a smaller one using the Fibonacci recurrence.

source

structure imo1981_q3.problem_predicate (N : ℕ) (m n : ℤ) :

Prop

m_range : m ∈ set.Ioc 0 ↑N
n_range : n ∈ set.Ioc 0 ↑N
eq_one : (n ^ 2 - m * n - m ^ 2) ^ 2 = 1

source

theorem imo1981_q3.problem_predicate_iff (N : ℕ) (m n : ℤ) :

imo1981_q3.problem_predicate N m n ↔ m ∈ set.Ioc 0 ↑N ∧ n ∈ set.Ioc 0 ↑N ∧ (n ^ 2 - m * n - m ^ 2) ^ 2 = 1

source

def imo1981_q3.specified_set (N : ℕ) :

set ℤ

Equations

imo1981_q3.specified_set N = {k : ℤ | ∃ (m n : ℤ), k = m ^ 2 + n ^ 2 ∧ imo1981_q3.problem_predicate N m n}

source

theorem imo1981_q3.problem_predicate.m_le_n {N : ℕ} {m n : ℤ} (h1 : imo1981_q3.problem_predicate N m n) :

m ≤ n

source

theorem imo1981_q3.problem_predicate.eq_imp_1 {N : ℕ} {n : ℤ} (h1 : imo1981_q3.problem_predicate N n n) :

n = 1

source

theorem imo1981_q3.problem_predicate.reduction {N : ℕ} {m n : ℤ} (h1 : imo1981_q3.problem_predicate N m n) (h2 : 1 < n) :

imo1981_q3.problem_predicate N (n - m) m

source

def imo1981_q3.nat_predicate (N m n : ℕ) :

Prop

Equations

imo1981_q3.nat_predicate N m n = imo1981_q3.problem_predicate N ↑m ↑n

source

theorem imo1981_q3.nat_predicate.m_le_n {N m n : ℕ} (h1 : imo1981_q3.nat_predicate N m n) :

m ≤ n

source

theorem imo1981_q3.nat_predicate.eq_imp_1 {N n : ℕ} (h1 : imo1981_q3.nat_predicate N n n) :

n = 1

source

theorem imo1981_q3.nat_predicate.reduction {N m n : ℕ} (h1 : imo1981_q3.nat_predicate N m n) (h2 : 1 < n) :

imo1981_q3.nat_predicate N (n - m) m

source

theorem imo1981_q3.nat_predicate.n_pos {N m n : ℕ} (h1 : imo1981_q3.nat_predicate N m n) :

0 < n

source

theorem imo1981_q3.nat_predicate.m_pos {N m n : ℕ} (h1 : imo1981_q3.nat_predicate N m n) :

0 < m

source

theorem imo1981_q3.nat_predicate.n_le_N {N m n : ℕ} (h1 : imo1981_q3.nat_predicate N m n) :

n ≤ N

source

theorem imo1981_q3.nat_predicate.imp_fib {N n : ℕ} (m : ℕ) :

imo1981_q3.nat_predicate N m n → (∃ (k : ℕ), m = nat.fib k ∧ n = nat.fib (k + 1))

source

theorem imo1981_q3.m_n_bounds {N K : ℕ} (HK : N < nat.fib K + nat.fib (K + 1)) {m n : ℕ} (h1 : imo1981_q3.nat_predicate N m n) :

m ≤ nat.fib K ∧ n ≤ nat.fib (K + 1)

source

theorem imo1981_q3.k_bound {N K : ℕ} (HK : N < nat.fib K + nat.fib (K + 1)) {M : ℕ} (HM : M = nat.fib K ^ 2 + nat.fib (K + 1) ^ 2) {m n : ℤ} (h1 : imo1981_q3.problem_predicate N m n) :

m ^ 2 + n ^ 2 ≤ ↑M

source

theorem imo1981_q3.solution_bound {N K : ℕ} (HK : N < nat.fib K + nat.fib (K + 1)) {M : ℕ} (HM : M = nat.fib K ^ 2 + nat.fib (K + 1) ^ 2) {k : ℤ} :

k ∈ imo1981_q3.specified_set N → k ≤ ↑M

source

theorem imo1981_q3.solution_greatest {N K : ℕ} (HK : N < nat.fib K + nat.fib (K + 1)) {M : ℕ} (HM : M = nat.fib K ^ 2 + nat.fib (K + 1) ^ 2) (H : imo1981_q3.problem_predicate N ↑(nat.fib K) ↑(nat.fib (K + 1))) :

is_greatest (imo1981_q3.specified_set N) ↑M

source

theorem imo1981_q3 :

is_greatest (imo1981_q3.specified_set 1981) 3524578