lean_workbook_plus_41069
ProvedWe will form a recursive sequence with initial conditions and where represents the number of ways can receive the ball after passes. So for the th term of the sequence, we have 2 cases. Case 1: If the th place is . In this case, there are ways of arriving to this point and clearly the th place can be . So the total ways of having the th position as is . Case 2: If the th position is not , say , for some . Then, in this case we cannot have the th place as (since the th place will be ) or (since the th place is already ). So we have ways in this case. So are recursion can be written as with initial conditions . So solving the characteristic equation and finding the coefficients, we get . Let to get .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_41069 (a : ℕ → ℚ) (h₀ : a 0 = 0) (h₁ : a 1 = 1) (h₂ : ∀ n, a (n + 2) = 2 * a (n + 1) + 3 * a n) : a 7 = 547 := by sorry
Source