Documentation

Archive.Imo.Imo1981Q3

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.

structure Imo1981Q3.ProblemPredicate (N : ℕ) (m n : ℤ) :

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

Instances For

theorem Imo1981Q3.problemPredicate_iff (N : ℕ) (m n : ℤ) :

ProblemPredicate N m n ↔ m ∈ Set.Ioc 0 ↑N ∧ n ∈ Set.Ioc 0 ↑N ∧ (n ^ 2 - m * n - m ^ 2) ^ 2 = 1

def Imo1981Q3.specifiedSet (N : ℕ) :

Equations

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

Instances For

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

m ≤ n

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

n = 1

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

ProblemPredicate N (n - m) m

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

Equations

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

Instances For

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

m ≤ n

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

n = 1

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

NatPredicate N (n - m) m

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

0 < n

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

0 < m

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

n ≤ N

theorem Imo1981Q3.NatPredicate.imp_fib {N n : ℕ} (m : ℕ) (h : NatPredicate N m n) :

∃ (k : ℕ), m = Nat.fib k ∧ n = Nat.fib (k + 1)

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

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

theorem Imo1981Q3.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 : ProblemPredicate N m n) :

m ^ 2 + n ^ 2 ≤ ↑M

theorem Imo1981Q3.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 ∈ specifiedSet N → k ≤ ↑M

theorem Imo1981Q3.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 : ProblemPredicate N ↑(Nat.fib K) ↑(Nat.fib (K + 1))) :

IsGreatest (specifiedSet N) ↑M

theorem imo1981_q3 :

IsGreatest (Imo1981Q3.specifiedSet 1981) 3524578