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.
We could prove that the order induced by
zeckendorfEquiv on Zeckendorf representations is exactly
the lexicographic order.
fibonacci, zeckendorf, digit
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
This is relevant for Zeckendorf's theorem, since if we write a natural
n as a sum of Fibonacci
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.
The Zeckendorf representation of a natural number.
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).
- One or more equations did not get rendered due to their size.