IMO 1981 Q3

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.

theorem Imo1981Q3.problemPredicate_iff (N : ℕ) (m : ℤ) (n : ℤ) : Imo1981Q3.ProblemPredicate N m n ↔ m ∈ Set.Ioc 0 ↑N ∧ n ∈ Set.Ioc 0 ↑N ∧ (n ^ 2 - m * n - m ^ 2) ^ 2 = 1

structure Imo1981Q3.ProblemPredicate (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

theorem Imo1981Q3.ProblemPredicate.m_range {N : ℕ} {m : ℤ} {n : ℤ} (self : Imo1981Q3.ProblemPredicate N m n) : m ∈ Set.Ioc 0 ↑N

theorem Imo1981Q3.ProblemPredicate.n_range {N : ℕ} {m : ℤ} {n : ℤ} (self : Imo1981Q3.ProblemPredicate N m n) : n ∈ Set.Ioc 0 ↑N

theorem Imo1981Q3.ProblemPredicate.eq_one {N : ℕ} {m : ℤ} {n : ℤ} (self : Imo1981Q3.ProblemPredicate N m n) : (n ^ 2 - m * n - m ^ 2) ^ 2 = 1

def Imo1981Q3.specifiedSet (N : ℕ) : Set ℤ

Equations

• Imo1981Q3.specifiedSet N = {k : ℤ | ∃ (m : ℤ) (n : ℤ), k = m ^ 2 + n ^ 2 ∧ Imo1981Q3.ProblemPredicate N m n}

theorem Imo1981Q3.ProblemPredicate.m_le_n {N : ℕ} {m : ℤ} {n : ℤ} (h1 : Imo1981Q3.ProblemPredicate N m n) : m ≤ n

theorem Imo1981Q3.ProblemPredicate.eq_imp_1 {N : ℕ} {n : ℤ} (h1 : Imo1981Q3.ProblemPredicate N n n) : n = 1

theorem Imo1981Q3.ProblemPredicate.reduction {N : ℕ} {m : ℤ} {n : ℤ} (h1 : Imo1981Q3.ProblemPredicate N m n) (h2 : 1 < n) : Imo1981Q3.ProblemPredicate N (n - m) m

def Imo1981Q3.NatPredicate (N : ℕ) (m : ℕ) (n : ℕ) : Prop

Equations

• Imo1981Q3.NatPredicate N m n = Imo1981Q3.ProblemPredicate N ↑m ↑n

theorem Imo1981Q3.NatPredicate.m_le_n {N : ℕ} {m : ℕ} {n : ℕ} (h1 : Imo1981Q3.NatPredicate N m n) : m ≤ n

theorem Imo1981Q3.NatPredicate.eq_imp_1 {N : ℕ} {n : ℕ} (h1 : Imo1981Q3.NatPredicate N n n) : n = 1

theorem Imo1981Q3.NatPredicate.reduction {N : ℕ} {m : ℕ} {n : ℕ} (h1 : Imo1981Q3.NatPredicate N m n) (h2 : 1 < n) : Imo1981Q3.NatPredicate N (n - m) m

theorem Imo1981Q3.NatPredicate.n_pos {N : ℕ} {m : ℕ} {n : ℕ} (h1 : Imo1981Q3.NatPredicate N m n) : 0 < n

theorem Imo1981Q3.NatPredicate.m_pos {N : ℕ} {m : ℕ} {n : ℕ} (h1 : Imo1981Q3.NatPredicate N m n) : 0 < m

theorem Imo1981Q3.NatPredicate.n_le_N {N : ℕ} {m : ℕ} {n : ℕ} (h1 : Imo1981Q3.NatPredicate N m n) : n ≤ N

theorem Imo1981Q3.NatPredicate.imp_fib {N : ℕ} {n : ℕ} (m : ℕ) : Imo1981Q3.NatPredicate N m n → ∃ (k : ℕ), m = k.fib ∧ n = (k + 1).fib

theorem Imo1981Q3.m_n_bounds {N : ℕ} {K : ℕ} (HK : N < K.fib + (K + 1).fib) {m : ℕ} {n : ℕ} (h1 : Imo1981Q3.NatPredicate N m n) : m ≤ K.fib ∧ n ≤ (K + 1).fib

theorem Imo1981Q3.k_bound {N : ℕ} {K : ℕ} (HK : N < K.fib + (K + 1).fib) {M : ℕ} (HM : M = K.fib ^ 2 + (K + 1).fib ^ 2) {m : ℤ} {n : ℤ} (h1 : Imo1981Q3.ProblemPredicate N m n) : m ^ 2 + n ^ 2 ≤ ↑M

theorem Imo1981Q3.solution_bound {N : ℕ} {K : ℕ} (HK : N < K.fib + (K + 1).fib) {M : ℕ} (HM : M = K.fib ^ 2 + (K + 1).fib ^ 2) {k : ℤ} : k ∈ Imo1981Q3.specifiedSet N → k ≤ ↑M

theorem Imo1981Q3.solution_greatest {N : ℕ} {K : ℕ} (HK : N < K.fib + (K + 1).fib) {M : ℕ} (HM : M = K.fib ^ 2 + (K + 1).fib ^ 2) (H : Imo1981Q3.ProblemPredicate N ↑K.fib ↑(K + 1).fib) : IsGreatest (Imo1981Q3.specifiedSet N) ↑M

theorem imo1981_q3 : IsGreatest (Imo1981Q3.specifiedSet 1981) 3524578