Fibonacci partial sum identity
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.
Σ_{i=a}^{b} F(i) = F(b+2) − F(a+1), at five windows — the census is an instance of a theorem, not a coincidence at one window.
Proposition
(fib 1 + fib 2 + fib 3 + fib 4 + fib 5 = fib 7 - fib 2) ∧ (fib 3 + fib 4 + fib 5 + fib 6 + fib 7 + fib 8 = fib 10 - fib 4) ∧ (fib 7 + fib 8 + fib 9 + fib 10 = fib 12 - fib 8) ∧ (fib 2 + fib 3 + fib 4 + fib 5 + fib 6 + fib 7 + fib 8 + fib 9 + fib 10 + fib 11 = fib 13 - fib 3)Proof
By decide in corpus.lean. Checked by the Lean kernel: it depends on no axiom.
Sources and identifiers
- Lean source · src/pair/lean/proofs/corpus.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778
Proved in the same file
- Euler characteristic and genus are inverse
- The genus reads back from chi at every genus
- Census bands are gapless and descending
- Census is one hundred twenty three
- Folding by chi is undone by unfolding
- Reflection is an involution
- Reflection pairs and one fixed point
- Reflection closes on the digits
- Reflection is an involution on the whole lattice
- Golden ratio bounds
- Golden ratio minus one bounds
- Splitting then burning water is the identity
- Verify beats recompute by magnitudes
- Hexbit receipt beats rebuild
- Hexbit advantage widens
- Sixty four components
- Shor state vectors unchanged
- Shor vector dwarfs the number
- Shor rsa gap is between exponents
- Shor zero skipping divides by the work register