Uniqueness of solutions given initial values

Remarks

The proof is a strong induction on $n$. For $n < d$ the claim is the hypothesis. For $n \ge d$, the recurrence writes $u_n$ and $v_n$ by the same formula in the $d$ previous terms, which agree by induction. Existence also holds: for each choice of $u_0, \dots, u_{d-1}$ in $R$, the recurrence defines the later terms one by one. So the map $u \mapsto (u_0, \dots, u_{d-1})$ is a bijection from the solutions onto $R^d$; see the space of solutions. Example: let $\varphi$ and $\psi$ be the roots of $X^2 - X - 1$, and let $v_n = (\varphi^n - \psi^n)/\sqrt{5}$. Then $v$ solves $u_{n+2} = u_{n+1} + u_n$ over $\R$, and $v_0 = 0$, $v_1 = 1$. The Fibonacci sequence solves the same recurrence with the same two initial values, so it equals $v$; this proves Binet's formula. Fewer initial values are not enough: $(0, 1, 1, 2, 3, \dots)$ and $(0, 2, 2, 4, 6, \dots)$ both solve $u_{n+2} = u_{n+1} + u_n$ and agree in the first term only.

Going deeper

For a student

This fact is the basic tool for proving closed formulas for recurrent sequences. To check a formula, one checks that it satisfies the recurrence and that it has the right first $d$ terms. Together with existence, it shows that the solutions form a free module of rank $d$ with the initial values as coordinates. In Mathlib it is LinearRecurrence.eq_mk_of_is_sol_of_eq_init.