Zeckendorf's Theorem

This file proves Zeckendorf's theorem: Every natural number can be written uniquely as a sum of distinct non-consecutive Fibonacci numbers.

Main declarations

• List.IsZeckendorfRep: Predicate for a list to be an increasing sequence of non-consecutive natural numbers greater than or equal to 2, namely a Zeckendorf representation.
• Nat.greatestFib: Greatest index of a Fibonacci number less than or equal to some natural.
• Nat.zeckendorf: Send a natural number to its Zeckendorf representation.
• Nat.zeckendorfEquiv: Zeckendorf's theorem, in the form of an equivalence between natural numbers and Zeckendorf representations.

TODO

We could prove that the order induced by zeckendorfEquiv on Zeckendorf representations is exactly the lexicographic order.

Tags

fibonacci, zeckendorf, digit

def instIsTransNatLeInstLENatHAddInstHAddInstAddNatOfNatInstOfNatNat : IsTrans ℕ fun (a b : ℕ) => b + 2 ≤ a

Equations

• instIsTransNatLeInstLENatHAddInstHAddInstAddNatOfNatInstOfNatNat = ⋯

def List.IsZeckendorfRep (l : List ℕ) : Prop

A list of natural numbers is a Zeckendorf representation (of a natural number) if it is an increasing sequence of non-consecutive numbers greater than or equal to 2.

This is relevant for Zeckendorf's theorem, since if we write a natural n as a sum of Fibonacci numbers (l.map fib).sum, IsZeckendorfRep l exactly means that we can't simplify any expression of the form fib n + fib (n + 1) = fib (n + 2), fib 1 = fib 2 or fib 0 = 0 in the sum.

Equations

• List.IsZeckendorfRep l = List.Chain' (fun (a b : ℕ) => b + 2 ≤ a) (l ++ [0])

theorem List.IsZeckendorfRep.sum_fib_lt {n : ℕ} {l : List ℕ} : List.IsZeckendorfRep l → (∀ a ∈ List.head? (l ++ [0]), a < n) → List.sum (List.map Nat.fib l) < Nat.fib n

def Nat.greatestFib (n : ℕ) : ℕ

The greatest index of a Fibonacci number less than or equal to n.

Equations

• Nat.greatestFib n = Nat.findGreatest (fun (k : ℕ) => Nat.fib k ≤ n) (n + 1)

theorem Nat.fib_greatestFib_le (n : ℕ) : Nat.fib (Nat.greatestFib n) ≤ n

theorem Nat.greatestFib_mono : Monotone Nat.greatestFib

@[simp]

theorem Nat.le_greatestFib {m : ℕ} {n : ℕ} : m ≤ Nat.greatestFib n ↔ Nat.fib m ≤ n

@[simp]

theorem Nat.greatestFib_lt {m : ℕ} {n : ℕ} : Nat.greatestFib m < n ↔ m < Nat.fib n

theorem Nat.lt_fib_greatestFib_add_one (n : ℕ) : n < Nat.fib (Nat.greatestFib n + 1)

@[simp]

theorem Nat.greatestFib_fib {n : ℕ} : n ≠ 1 → Nat.greatestFib (Nat.fib n) = n

@[simp]

theorem Nat.greatestFib_eq_zero {n : ℕ} : Nat.greatestFib n = 0 ↔ n = 0

theorem Nat.greatestFib_ne_zero {n : ℕ} : Nat.greatestFib n ≠ 0 ↔ n ≠ 0

@[simp]

theorem Nat.greatestFib_pos {n : ℕ} : 0 < Nat.greatestFib n ↔ 0 < n

theorem Nat.greatestFib_sub_fib_greatestFib_le_greatestFib {n : ℕ} (hn : n ≠ 0) : Nat.greatestFib (n - Nat.fib (Nat.greatestFib n)) ≤ Nat.greatestFib n - 2

def Nat.zeckendorf : ℕ → List ℕ

The Zeckendorf representation of a natural number.

Note: For unfolding, you should use the equational lemmas Nat.zeckendorf_zero and Nat.zeckendorf_of_pos instead of the autogenerated one.

Equations

• Nat.zeckendorf 0 = []
• Nat.zeckendorf (Nat.succ n) = let a := Nat.greatestFib (Nat.succ n); let_fun this := ⋯; a :: Nat.zeckendorf (Nat.succ n - Nat.fib a)

@[simp]

theorem Nat.zeckendorf_zero : Nat.zeckendorf 0 = []

@[simp]

theorem Nat.zeckendorf_succ (n : ℕ) : Nat.zeckendorf (n + 1) = Nat.greatestFib (n + 1) :: Nat.zeckendorf (n + 1 - Nat.fib (Nat.greatestFib (n + 1)))

@[simp]

theorem Nat.zeckendorf_of_pos {n : ℕ} : 0 < n → Nat.zeckendorf n = Nat.greatestFib n :: Nat.zeckendorf (n - Nat.fib (Nat.greatestFib n))

theorem Nat.isZeckendorfRep_zeckendorf (n : ℕ) : List.IsZeckendorfRep (Nat.zeckendorf n)

theorem Nat.zeckendorf_sum_fib {l : List ℕ} : List.IsZeckendorfRep l → Nat.zeckendorf (List.sum (List.map Nat.fib l)) = l

@[simp]

theorem Nat.sum_zeckendorf_fib (n : ℕ) : List.sum (List.map Nat.fib (Nat.zeckendorf n)) = n

def Nat.zeckendorfEquiv : ℕ ≃ { l : List ℕ // List.IsZeckendorfRep l }

Zeckendorf's Theorem as an equivalence between natural numbers and Zeckendorf representations. Every natural number can be written uniquely as a sum of non-consecutive Fibonacci numbers (if we forget about the first two terms F₀ = 0, F₁ = 1).

Equations

• One or more equations did not get rendered due to their size.