English
If l is a Zeckendorf representation, then the Zeckendorf representation of the sum of fib numbers from l is l: zeckendorf((l.map fib).sum) = l.
Русский
Если l является репрезентацией Зекендорфа, то zeckendorf суммы fib чисел из l равен l.
LaTeX
$$$$ \operatorname{zeckendorf}\left( \sum_{x \in l} \operatorname{fib}(x) \right) = l \quad\text{for all } l \text{ with } \operatorname{IsZeckendorfRep}(l). $$$$
Lean4
theorem zeckendorf_sum_fib : ∀ {l}, IsZeckendorfRep l → zeckendorf (l.map fib).sum = l
| [], _ => by simp only [map_nil, List.sum_nil, zeckendorf_zero]
| a :: l, hl => by
have hl' := hl
simp only [IsZeckendorfRep, cons_append, isChain_iff_pairwise, pairwise_cons, mem_append, mem_singleton, or_imp,
forall_and, forall_eq, zero_add] at hl
rw [← isChain_iff_pairwise] at hl
have ha : 0 < a := hl.1.2.trans_lt' zero_lt_two
suffices h : greatestFib (fib a + sum (map fib l)) = a by
simp only [map, List.sum_cons, add_pos_iff, fib_pos.2 ha, true_or, zeckendorf_of_pos, h, add_tsub_cancel_left,
zeckendorf_sum_fib hl.2]
simp only [add_comm, add_assoc, greatestFib, findGreatest_eq_iff, ne_eq, ha.ne', not_false_eq_true,
le_add_iff_nonneg_left, _root_.zero_le, forall_true_left, not_le, true_and]
refine ⟨le_add_of_le_right <| le_fib_add_one _, fun n hn _ ↦ ?_⟩
rw [add_comm, ← List.sum_cons, ← map_cons]
exact hl'.sum_fib_lt (by simpa)
