<SYSTEM_TASK:>
Given the following text description, write Python code to implement the functionality described below step by step
<END_TASK>
<USER_TASK:>
Description:
 <p>
<img src="http
Step1:  OEIS
We start our study asking the OEIS the sequence of Fibonacci numbers, which is denoted by A000045
Step2:  Recurrence
Spec
In this section we define the classic recurrence for the sequence of Fibonacci numbers, using on the lhs subscript that makes sense for all $n\in\mathbb{N}$.
Step3:  Unfolding
Step4:  Involution
Step5:  Subsuming
Step6:  We can abstract the following conjecture
Step7:  Instantiation
Raw
Step8:  Based
Step9:  Computing
Step10:  Collecting
Spec as symbolic matrix-vector product
Step11:  Spec as based matrix-vector product
Step12:  Identities and conjectures
Relation with binomial coefficients
Step13:  which is known but left as an exercise by Benjamin and Quinn, in the following form
Step14:  instantiating $m=n$ we get a closed representation of the matrix-vector product seen before
Step15:  A little application of the previous identity is in the following cells
Step16:  symbolic expansion of the Sum object
Step17:  instantiate to let $f_{0}$ appears in the identity (our concept of based instantiation)
Step18:  finally, check the consistency using the sequence of Fibonacci numbers
Step19:  Looking at bottom left to top right diagonal sums
Another well known recurrence about those numbers involving Pascal triangle is the following
Step20:  we build the sum for each diagonal, manually
Step21:  looking at the sequence composed by coeffients in the rhs of each equation we recognize A059633. According to the reference, the sequence is built by the following recurrence
Step23:  therefore we can conjecture the following identity
<ASSISTANT_TASK:>
Python Code:
%run "../src/start_session.py"
%run "../src/recurrences.py"
%run "../src/sums.py"
from sympy.abc import i
from oeis import oeis_search, ListData
import knowledge
sys.setrecursionlimit(10000000)
Explanation: <p>
<img src="http://www.cerm.unifi.it/chianti/images/logo%20unifi_positivo.jpg" 
        alt="UniFI logo" style="float: left; width: 20%; height: 20%;">
<div align="right"> Massimo Nocentini<br>
<small>
<br>October 3, 2016: conjectures
<br>September 30, 2016: cleaning, matrix-vector product
<br>September 29, 2016: ordered set-wise spec representation, terms cache subs & project
<br>September 28, 2016: graphical representations, simple unfolding
</small>
</div>
</p>
<br>
<p>
<div align="center">
<b>abstract</b><br>
In this document we explore the sequence of <i>Fibonacci numbers</i>, from the point of view of <i>recurrence unfolding</i>, an algorithmic/symbolical idea under development. We're going to apply such technique aiming to show new interesting identities among these wonderful numbers. Moreover, we collect in this very document some content directly from the OEIS and some funny graphical interpretations of the defining recurrence.
</div>
</p>
End of explanation
s = oeis_search(id=45)
s(data_only=True)#, data_representation=ListData(upper_limit=20))
Explanation: OEIS
We start our study asking the OEIS the sequence of Fibonacci numbers, which is denoted by A000045:
End of explanation
with bind(IndexedBase('y'), single=True) as y,\
     bind(IndexedBase('b'), single=True) as b:
    stirling_second_kind_rec_spec = recurrence_spec(recurrence_eq=Eq(y[i],x*y[i-1]+b[i]), 
                                         recurrence_symbol=y, 
                                         variables=[i])
stirling_second_kind_rec_spec
Explanation: Recurrence
Spec
In this section we define the classic recurrence for the sequence of Fibonacci numbers, using on the lhs subscript that makes sense for all $n\in\mathbb{N}$.
End of explanation
unfolded = stirling_second_kind_rec_spec.unfold(depth=4)
unfolded
Explanation: Unfolding
End of explanation
unfolded.involute(depth=1)
unfolded.involute()
Explanation: Involution
End of explanation
subsumed=unfolded.subsume()
subsumed
Explanation: Subsuming
End of explanation
im=knowledge.fibonacci_numbers_inverted_mapping(start=2, limit=20)
im
subsumed.subs(im)
Explanation: We can abstract the following conjecture: $ f_{n+k-2d+2} = f_{k} f_{n-2d} + f_{k+1} f_{n-2d+1} $, for $k\in{0,\ldots, 2d-1}$
Substitution
End of explanation
unfolded.instantiate(strategy=raw(substitutions={n:20}))
Explanation: Instantiation
Raw
End of explanation
instantiated = unfolded.instantiate(strategy=based(arity=unary_indexed()))
instantiated
Explanation: Based
End of explanation
almost_valued = instantiated.subsume(additional_terms={f[0]:Integer(0), f[1]:Integer(1)})
almost_valued
almost_valued.involute()
Explanation: Computing
End of explanation
m, v, r, eqs = stirling_second_kind_rec_spec.matrix_vector_product(depth=10, arity=unary_indexed(), 
                                                        segment=[n-k for k in range(-2, 19)])
latex_array_src(eqs)
m, v, r
sols=solve(Eq(m*v, r), v)
eq_system = [Eq(k, v) for k, v in sols.items()]
latex_array_src(eq_system)
to_matrix_notation(eq_system, f, [n-k for k in range(8,19)])
example={n:30}
to_check = Eq(m*v.subs(example), r.subs(example))
to_check
to_check.subs(knowledge.fibonacci_numbers(), simultaneous=True)
Explanation: Collecting
Spec as symbolic matrix-vector product
End of explanation
m, v, r, eqs = fibonacci_rec_spec.matrix_vector_product(depth=10, arity=unary_indexed(), 
                                                        segment=[Integer(k) for k in range(0, 11)],
                                                        based_instantiation=True)
latex_array_src(eqs)
m,v,r
Explanation: Spec as based matrix-vector product
End of explanation
m = symbols('m')
thm = Eq(f[n], Sum(binomial(m,k)*f[n-2*m+k], (k,0,m)))
thm
Explanation: Identities and conjectures
Relation with binomial coefficients
End of explanation
benjamin_quinn_thm = thm.subs({n:n+m})
benjamin_quinn_thm
Explanation: which is known but left as an exercise by Benjamin and Quinn, in the following form:
End of explanation
benjamin_quinn_thm.subs({m:n})
Explanation: instantiating $m=n$ we get a closed representation of the matrix-vector product seen before:
End of explanation
def expand_sum_in_eq(eq_term, in_lhs=False, in_rhs=True):
    lhs, rhs = eq_term.lhs, eq_term.rhs
    return Eq(expand_Sum(lhs) if in_lhs else lhs, expand_Sum(rhs) if in_rhs else rhs)
Explanation: A little application of the previous identity is in the following cells:
End of explanation
expanded_eq = expand_sum_in_eq(thm.subs({m:20}))
expanded_eq
Explanation: symbolic expansion of the Sum object:
End of explanation
subsed = expanded_eq.subs(n, 40)
subsed
Explanation: instantiate to let $f_{0}$ appears in the identity (our concept of based instantiation):
End of explanation
subsed.subs(knowledge.fibonacci_numbers())
Explanation: finally, check the consistency using the sequence of Fibonacci numbers:
End of explanation
fibs = knowledge.fibonacci_numbers()
Explanation: Looking at bottom left to top right diagonal sums
Another well known recurrence about those numbers involving Pascal triangle is the following: 
$$ f_{n+1} = \sum_{k\geq 0}{{{n-k}\choose{k}}}$$
namely, a fibonacci number equals the sum in diagonals. Here we do something similar...
End of explanation
f2_diag = f[0]
f4_diag = f[0]+f[1]
f6_diag = f[0]+2*f[1]
f8_diag = f[0]+3*f[1]+f[2]
f10_diag = f[0]+4*f[1]+3*f[2]
f12_diag = f[0]+5*f[1]+6*f[2]+f[3]
f14_diag = f[0]+6*f[1]+10*f[2]+4*f[3]
f16_diag = f[0]+7*f[1]+15*f[2]+10*f[3]+f[4]
f18_diag = f[0]+8*f[1]+21*f[2]+20*f[3]+5*f[4]
f20_diag = f[0]+9*f[1]+28*f[2]+35*f[3]+15*f[4]+f[5]
f22_diag = f[0]+10*f[1]+36*f[2]+56*f[3]+35*f[4]+6*f[5]
f24_diag = f[0]+11*f[1]+45*f[2]+84*f[3]+70*f[4]+21*f[5]+f[6]
f26_diag = f[0]+12*f[1]+55*f[2]+120*f[3]+126*f[4]+56*f[5]+7*f[6]
diagonals = [Eq(f2_diag, f2_diag.subs(fibs)),
             Eq(f4_diag, f4_diag.subs(fibs)),
             Eq(f6_diag, f6_diag.subs(fibs)),
             Eq(f8_diag, f8_diag.subs(fibs)),
             Eq(f10_diag, f10_diag.subs(fibs)),
             Eq(f12_diag, f12_diag.subs(fibs)),
             Eq(f14_diag, f14_diag.subs(fibs)),
             Eq(f16_diag, f16_diag.subs(fibs)),
             Eq(f18_diag, f18_diag.subs(fibs)),
             Eq(f20_diag, f20_diag.subs(fibs)),
             Eq(f22_diag, f22_diag.subs(fibs)),
             Eq(f24_diag, f24_diag.subs(fibs)),
             Eq(f26_diag, f26_diag.subs(fibs))]
latex_array_src(diagonals)
Explanation: we build the sum for each diagonal, manually: it is ugly, so we hope to refactor it and introduce a function to do so:
End of explanation
def A059633_gf(x): 
    return 1/(1-2*x+x**3-x**4)
A059633_gf(t).series(t,n=14)
Explanation: looking at the sequence composed by coeffients in the rhs of each equation we recognize A059633. According to the reference, the sequence is built by the following recurrence: $a_{n} = 2a_{n-1}-a_{n-3}+a_{n-4}$, as the following expansion confirms:
End of explanation
def do_memberwise_on_eqs(an_eq, another_eq, operator=lambda x, y: Add(x,y,evaluate=True)):
    return Eq(operator(an_eq.lhs, another_eq.lhs), operator(an_eq.rhs, another_eq.rhs))
def swap_eq(eq_term): return Eq(eq_term.rhs, eq_term.lhs)
reduce(do_memberwise_on_eqs, eqs)
even_subscript_fibonacci_eq = Eq(f[2*n+1]-1, Sum(f[2*k],(k,0,n)))
even_subscript_fibonacci_eq
example = even_subscript_fibonacci_eq.subs(n,21)
example_expanded = expand_sum_in_eq(example)
example_expanded, example_expanded.subs(fibs)
from itertools import accumulate
enum_range = range(0,50,2)
def worker(accumulated_pair, current_pair):
    index, current = current_pair
    _, accumulated = accumulated_pair
    
    summed_eq = do_memberwise_on_eqs(accumulated, current)
    
    return index, summed_eq
def subs_fib_thm(pair):
    index, current_eq = pair
    expanded_thm = expand_sum_in_eq(even_subscript_fibonacci_eq.subs({n:Integer(index)/2}))
    return index, current_eq, expanded_thm
#def eq_to_subs_dict(eq_term): return {eq_term.lhs:eq_term.rhs}
def apply_subs_on_lhs(triple):
    index, current_eq, thm = triple
    return current_eq.subs({thm.rhs:thm.lhs})
def latex_array_env_of_eqs(mapped):
    from string import Template
    template = Template(r\begin{array}{c}$content\end{array})
    return template.substitute(content="\n".join(mapped))
triangle = accumulate(zip(enum_range, eqs), worker)
triangle = map(subs_fib_thm, triangle)
triangle = list(map(apply_subs_on_lhs, triangle))
triangle[0] = Eq(f[1]-1,f[0])
latex_array_src(triangle)
all(map(lambda eq: eq.subs(fibs), triangle))
to_matrix_notation(triangle, f , range(0, 11))
triangle = [eq.subs({f[0]:fibs[f[0]]}, simultaneous=True) for eq in triangle[1:]]
latex_array_src(triangle)
to_matrix_notation(triangle, f, range(1,11))
Explanation: therefore we can conjecture the following identity:
$$ \sum_{k\geq 0}{{{n-k}\choose{k}}}f_{k} = [t^{n}]\frac{t}{1-2t+t^{3}-t^{4}}$$
Matrix characterization of $f_{2n+1}, \forall n \in\mathbb{N}$
End of explanation
<END_TASK>