Nested Summations

on YouTube ↗16m

" summary

This work claims explicit formulas that express Fibonacci, Lucas, Jacobstahl and Jacobstahl‑Lucas sequences as finitely nested finite sums, gives the construction that generalizes to Jacobstahl sequences with arbitrary core multiplicative factor, and machine‑checks the proofs in the Coq Proof Assistant with artifacts on Zenodo. Examples include nesting n sums to get (x+1)^n, nesting with decreasing bounds to get x! and a specific choice of inner bound (1−i) that yields Fibonacci numbers; proofs are formal and executable.

AI-written summary · about

" chapters (12)

1. 0:00Nested summations intro
2. 1:53Single summations basics
3. 2:35Two-loop nested sums
4. 5:09Generalizing to three+ sums
5. 6:58Arbitrary nesting depth
6. 8:49Decreasing bounds & factorials
7. 10:14Binomial coefficients via sums
8. 12:25Catalan numbers from sums
9. 13:09Fibonacci numbers from sums
10. 14:23Moser’s theorem & DP origins
11. 15:30Lucas & Jacobsthal numbers
12. 16:14Summary