module
public import Mathlib.Algebra.BigOperators.Fin
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.SetTheory.Cardinal.Finite
public import Mathlib.Tactic.Ring
public section
/-!
# USA Mathematical Olympiad 2013, Problem 2
For a positive integer $n \ge 3$ plot $n$ equally spaced points around a circle.
Label one of them $A$, and place a marker at $A$. One may move the marker forward
in a clockwise direction to either the next point or the point after that. Hence
there are a total of $2n$ distinct moves available; two from each point. Let $a_n$
count the number of ways to advance around the circle exactly twice, beginning and
ending at $A$, without repeating a move. Prove that $a_{n-1} + a_n = 2^n$ for all
$n \ge 4$.
-/
namespace Usa2013P2
/-!
## Setting up the count
We unroll the two trips around the circle into the integer interval
`{0, 1, …, 2n}`: a path becomes a walk from `0` to `2n` in steps of size `1` or
`2`, and a *move* is a pair (starting point mod `n`, step length). Recording, for
each `i ∈ {0, …, 2n}`, whether the walk visits `i` yields a `2 × (n+1)` zero-one
matrix
```
[ p₀ p₁ … p_{n-1} p_n ]
[ p_n p_{n+1} … p_{2n-1} p_{2n} ]
```
with `p₀ = p_{2n} = 1`. The conditions of the problem translate as follows:
* steps have size at most `2` iff no two horizontally adjacent entries are both `0`;
* no repeated move of length `2` iff no column is `(0,0)` (points `i` and `i+n`
are both skipped exactly when the same length-2 move is used twice);
* no repeated move of length `1` iff no two adjacent columns are both `(1,1)`
(points `i, i+1, i+n, i+n+1` are all visited exactly when the same length-1
move is used twice).
Conversely every such matrix determines a unique valid path, so `a_n` counts
these matrices. Each column is one of `u = (1,0)`, `v = (0,1)`, `w = (1,1)`
(encoded as `0, 1, 2 : Fin 3`), and the conditions say exactly that adjacent
columns are distinct, the first column is `u` or `w`, the last column is `v` or
`w`, and the first column is `w` iff the last one is. Sequences starting with
`u` must end in `v`, and sequences starting with `w` must end in `w`, giving
`a_n = x_n + y_n` below. We then follow the first solution in Evan Chen's
*USAMO 2013 Solution Notes*: by symmetry (`Fin 3` column relabeling) and the
"delete the last column" bijection one gets `x_{n+1} = x_n + y_n`,
`y_{n+1} = 2 * x_n` and `2 * x_n + y_n = 2^n`, hence
`a_{n+1} + a_n = 2 ^ (n+1)`.
-/
/-- A sequence of `n+1` columns, each column one of the three symbols of `Fin 3`
(`0 = u`, `1 = v`, `2 = w`). -/
abbrev ColSeq (n : ℕ) := Fin (n + 1) → Fin 3
/-- Adjacent columns are distinct. -/
abbrev AdjDistinct {n : ℕ} (c : ColSeq n) : Prop := ∀ i : Fin n, c i.castSucc ≠ c i.succ
/-- The number of column sequences of length `n+1` with distinct adjacent columns
starting with `s` and ending with `t`. -/
noncomputable def countCol (n : ℕ) (s t : Fin 3) : ℕ :=
Nat.card {c : ColSeq n // AdjDistinct c ∧ c 0 = s ∧ c (Fin.last n) = t}
/-- The number of ways to advance around the circle exactly twice without
repeating a move: sequences starting with `u = 0` end in `v = 1`, and sequences
starting with `w = 2` end in `w = 2`. -/
noncomputable def a (n : ℕ) : ℕ := countCol n 0 1 + countCol n 2 2
theorem usa2013_p2 (n : ℕ) (hn : 4 ≤ n) : a (n - 1) + a n = 2 ^ n := sorry
end Usa2013P2
This problem has a complete formalized solution.