Frobenius Number in Two Variables

In this file we first define a predicate for Frobenius numbers, then solve the 2-variable variant of this problem.

Theorem Statement

Given a finite set of relatively prime integers all greater than 1, their Frobenius number is the largest positive integer that cannot be expressed as a sum of nonnegative multiples of these integers. Here we show the Frobenius number of two relatively prime integers m and n greater than 1 is m * n - m - n. This result is also known as the Chicken McNugget Theorem.

Implementation Notes

First we define Frobenius numbers in general using IsGreatest and AddSubmonoid.closure. Then we proceed to compute the Frobenius number of m and n.

For the upper bound, we begin with an auxiliary lemma showing m * n is not attainable, then show m * n - m - n is not attainable. Then for the construction, we create a k_1 which is k mod n and 0 mod m, then show it is at most k. Then k_1 is a multiple of m, so (k-k_1) is a multiple of n, and we're done.

Tags

frobenius number, chicken mcnugget, chinese remainder theorem, add_submonoid.closure

def FrobeniusNumber (n : ℕ) (s : Set ℕ) : Prop

A natural number n is the Frobenius number of a set of natural numbers s if it is an upper bound on the complement of the additive submonoid generated by s. In other words, it is the largest number that can not be expressed as a sum of numbers in s.

Equations

• FrobeniusNumber n s = IsGreatest {k : ℕ | k ∉ AddSubmonoid.closure s} n

theorem frobeniusNumber_pair {m : ℕ} {n : ℕ} (cop : m.Coprime n) (hm : 1 < m) (hn : 1 < n) : FrobeniusNumber (m * n - m - n) {m, n}

The Chicken McNugget theorem stating that the Frobenius number of positive numbers m and n is m * n - m - n.