# 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

IsTrans fun (a b : ) => b + 2 a
Equations
Instances For

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
Instances For
@[simp]
theorem List.IsZeckendorfRep_nil :
[].IsZeckendorfRep
theorem List.IsZeckendorfRep.sum_fib_lt {n : } {l : } :
l.IsZeckendorfRep(a(l ++ [0]).head?, a < n)().sum <

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

Equations
Instances For
theorem Nat.fib_greatestFib_le (n : ) :
Nat.fib n.greatestFib n
@[simp]
theorem Nat.le_greatestFib {m : } {n : } :
m n.greatestFib n
@[simp]
theorem Nat.greatestFib_lt {m : } {n : } :
m.greatestFib < n m <
theorem Nat.lt_fib_greatestFib_add_one (n : ) :
n < Nat.fib (n.greatestFib + 1)
@[simp]
theorem Nat.greatestFib_fib {n : } :
n 1().greatestFib = n
@[simp]
theorem Nat.greatestFib_eq_zero {n : } :
n.greatestFib = 0 n = 0
theorem Nat.greatestFib_ne_zero {n : } :
n.greatestFib 0 n 0
@[simp]
theorem Nat.greatestFib_pos {n : } :
0 < n.greatestFib 0 < n
theorem Nat.greatestFib_sub_fib_greatestFib_le_greatestFib {n : } (hn : n 0) :
(n - Nat.fib n.greatestFib).greatestFib n.greatestFib - 2
@[irreducible]

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
• = []
• n.succ.zeckendorf = n.succ.greatestFib :: (n.succ - Nat.fib n.succ.greatestFib).zeckendorf
Instances For
@[simp]
theorem Nat.zeckendorf_zero :
= []
@[simp]
theorem Nat.zeckendorf_succ (n : ) :
(n + 1).zeckendorf = (n + 1).greatestFib :: (n + 1 - Nat.fib (n + 1).greatestFib).zeckendorf
@[simp]
theorem Nat.zeckendorf_of_pos {n : } :
0 < nn.zeckendorf = n.greatestFib :: (n - Nat.fib n.greatestFib).zeckendorf
@[irreducible]
theorem Nat.isZeckendorfRep_zeckendorf (n : ) :
n.zeckendorf.IsZeckendorfRep
theorem Nat.zeckendorf_sum_fib {l : } :
l.IsZeckendorfRep().sum.zeckendorf = l
@[simp]
theorem Nat.sum_zeckendorf_fib (n : ) :
(List.map Nat.fib n.zeckendorf).sum = n
def Nat.zeckendorfEquiv :
{ l : // l.IsZeckendorfRep }

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.
Instances For