English
A list l of natural numbers is a Zeckendorf representation if it is an increasing sequence of integers at least 2 with gaps of at least 2 between consecutive terms; equivalently, (l ++ [0]) is a chain under b+2 ≤ a.
Русский
Список натуральных чисел l является репрезентацией Зекендорфа, если он является возрастающей последовательностью не менее 2 с разрывами не менее 2 между соседними членами; эквивалентно, (l ++ [0]) образует цепочку относительно b+2 ≤ a.
LaTeX
$$$$ \operatorname{IsZeckendorfRep}(l) \iff (l \cup [0]) \text{ IsChain } (\lambda a,b.\; b+2 \le a). $$$$
Lean4
/-- 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. -/
def IsZeckendorfRep (l : List ℕ) : Prop :=
(l ++ [0]).IsChain (fun a b ↦ b + 2 ≤ a)
