`Compfiles/Usa2013P2.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

17 declarations, 0 contain sorry, 0 declared as axioms

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$.

Imports (5)

Imported by 1 file

Compfiles.lean

abbrev Usa2013P2.ColSeq A sequence of n+1 columns, each column one of the three symbols of Fin 3 (0 = u, 1 = v, 2 = w) line 70 source
Source documentation
A sequence of n+1 columns, each column one of the three symbols of Fin 3 (0 = u, 1 = v, 2 = w).

no axioms what this means
Statement uses: Nat
Proof uses: Fin, HAdd.hAdd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
abbrev ColSeq (n : ℕ) := Fin (n + 1) → Fin 3
```
abbrev Usa2013P2.AdjDistinct Adjacent columns are distinct line 73 source
Source documentation
Adjacent columns are distinct.

no axioms what this means
Statement uses: Nat, Usa2013P2.ColSeq
Proof uses: Fin, Ne, OfNat.ofNat, Fin.castSucc, Fin.succ
1 instances, coercions and auxiliary constants left out.
```
abbrev AdjDistinct {n : ℕ} (c : ColSeq n) : Prop := ∀ i : Fin n, c i.castSucc ≠ c i.succ
```
Mentions: Usa2013P2.ColSeq
def Usa2013P2.countCol The number of column sequences of length n+1 with distinct adjacent columns starting with s and ending with t line 77 source
Source documentation
The number of column sequences of length n+1 with distinct adjacent columns starting with s and ending with t.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat
Proof uses: Nat.card, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, Eq, HAdd.hAdd, Fin.last
6 instances, coercions and auxiliary constants left out.
```
noncomputable def countCol (n : ℕ) (s t : Fin 3) : ℕ :=
…
```
def Usa2013P2.a Documented declaration: a line 83 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, Usa2013P2.countCol, OfNat.ofNat, Fin
5 instances, coercions and auxiliary constants left out.
```
noncomputable def a (n : ℕ) : ℕ := countCol n 0 1 + countCol n 2 2
…
```
Mentions: Usa2013P2.countCol
def Usa2013P2.permEquiv Relabeling columns by a permutation of Fin 3 does not change the counts line 88 source
Source documentation
Relabeling columns by a permutation of Fin 3 does not change the counts.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, OfNat.ofNat, Equiv, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, Eq, HAdd.hAdd, Fin.last
Proof uses: Equiv.mk, Subtype.mk, Function.comp, Equiv.symm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def permEquiv {n : ℕ} (σ : Equiv.Perm (Fin 3)) (s t : Fin 3) :
    {c : ColSeq n // AdjDistinct c ∧ c 0 = s ∧ c (Fin.last n) = t} ≃
    {c : ColSeq n // AdjDistinct c ∧ c 0 = σ s ∧ c (Fin.last n) = σ t} where
…
```
Mentions: Usa2013P2.ColSeq, Usa2013P2.AdjDistinct
theorem Usa2013P2.card_eq_swap Swapping two column symbols does not change the counts line 107 source
Source documentation
Swapping two column symbols does not change the counts.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, Equiv.Perm, Equiv.swap, Usa2013P2.countCol
Proof uses: id, Eq.mpr, Nat.card, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, HAdd.hAdd, Fin.last, congrArg, Eq.symm, Nat.card_congr, Usa2013P2.permEquiv
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem card_eq_swap {n : ℕ} (s t s' t' p q : Fin 3)
    (hs : Equiv.swap p q s = s') (ht : Equiv.swap p q t = t') :
    countCol n s t = countCol n s' t' := by
…
```
Mentions: Usa2013P2.countCol
def Usa2013P2.dropLastEquiv Deleting the last column: sequences of length n+2 ending in t correspond to sequences of length n+1 ending in some r ≠ t line 116 source
Source documentation
Deleting the last column: sequences of length n+2 ending in t correspond to sequences of length n+1 ending in some r ≠ t.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Equiv, Subtype, Usa2013P2.ColSeq, HAdd.hAdd, And, Usa2013P2.AdjDistinct, Eq, Fin.last, Sigma, Ne
Proof uses: Equiv.mk, Sigma.mk, Fin.castSucc, Subtype.mk, Fin.init, Fin.snoc, Sigma.fst, Sigma.snd
17 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
def dropLastEquiv {n : ℕ} (s t : Fin 3) :
    {c : ColSeq (n + 1) // AdjDistinct c ∧ c 0 = s ∧ c (Fin.last (n + 1)) = t} ≃
    Σ r : Fin 3,
      {c : ColSeq n // AdjDistinct c ∧ c 0 = s ∧ c (Fin.last n) = r ∧ r ≠ t} where
…
```
Mentions: Usa2013P2.ColSeq, Usa2013P2.AdjDistinct
theorem Usa2013P2.countCol_succ The count recurrence obtained from dropLastEquiv line 169 source
Source documentation
The count recurrence obtained from dropLastEquiv.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, Usa2013P2.countCol, HAdd.hAdd, Finset.sum, Finset.univ, Nat.card, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, Fin.last, Ne
Proof uses: id, Eq.mpr, Sigma, congrArg, Nat.card_congr, Usa2013P2.dropLastEquiv, Nat.card_sigma, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem countCol_succ {n : ℕ} (s t : Fin 3) :
    countCol (n + 1) s t =
      ∑ r : Fin 3, Nat.card
        {c : ColSeq n // AdjDistinct c ∧ c 0 = s ∧ c (Fin.last n) = r ∧ r ≠ t} := by
…
```
Mentions: Usa2013P2.countCol, Usa2013P2.ColSeq, Usa2013P2.AdjDistinct
theorem Usa2013P2.card_drop_ne Dropping a decidable side condition from a column count line 177 source
Source documentation
Dropping a decidable side condition from a column count.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Ne, Eq, Nat.card, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, HAdd.hAdd, Fin.last, Usa2013P2.countCol
Proof uses: Nat.card_congr, Equiv.subtypeEquivRight, Iff.intro, And.intro, And.left, And.right
13 instances, coercions and auxiliary constants left out.
```
theorem card_drop_ne {n : ℕ} (s r t : Fin 3) (h : r ≠ t) :
    Nat.card {c : ColSeq n // AdjDistinct c ∧ c 0 = s ∧ c (Fin.last n) = r ∧ r ≠ t} =
      countCol n s r :=
…
```
Mentions: h, Usa2013P2.ColSeq, Usa2013P2.AdjDistinct, Usa2013P2.countCol
theorem Usa2013P2.card_eq_zero_of_ne A column count with contradictory side conditions is zero line 184 source
Source documentation
A column count with contradictory side conditions is zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, Nat.card, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, HAdd.hAdd, Fin.last, Ne
Proof uses: Eq.mpr, Fintype.card, Fin.castSucc, Fin.succ, id, congrArg, Nat.card_eq_fintype_card, IsEmpty, propext, Fintype.card_eq_zero_iff, IsEmpty.mk, And.right, Subtype.property, rfl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem card_eq_zero_of_ne {n : ℕ} (s r t : Fin 3) (h : r = t) :
    Nat.card {c : ColSeq n // AdjDistinct c ∧ c 0 = s ∧ c (Fin.last n) = r ∧ r ≠ t} = 0 := by
…
```
Mentions: h, Usa2013P2.ColSeq, Usa2013P2.AdjDistinct
theorem Usa2013P2.x_succ First recursion: x_{n+1} = y_n + x_n line 191 source
Source documentation
First recursion: x_{n+1} = y_n + x_n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2013P2.countCol, HAdd.hAdd, OfNat.ofNat, Fin
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, Finset.sum, Finset.univ, Nat.card, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, Fin.last, Ne, Usa2013P2.countCol_succ, Fin.sum_univ_three, congr, Usa2013P2.card_drop_ne, of_decide_eq_true, Bool and 20 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem x_succ (n : ℕ) : countCol (n + 1) 0 1 = countCol n 2 2 + countCol n 0 1 := by
…
```
Mentions: Usa2013P2.countCol
theorem Usa2013P2.y_succ Second recursion: y_{n+1} = 2 * x_n line 200 source
Source documentation
Second recursion: y_{n+1} = 2 * x_n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2013P2.countCol, HAdd.hAdd, OfNat.ofNat, Fin, HMul.hMul
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, Finset.sum, Finset.univ, Nat.card, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, Fin.last, Ne, Usa2013P2.countCol_succ, Fin.sum_univ_three, congr, Usa2013P2.card_drop_ne, of_decide_eq_true, Bool and 31 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem y_succ (n : ℕ) : countCol (n + 1) 2 2 = 2 * countCol n 0 1 := by
…
```
Mentions: Usa2013P2.countCol
theorem Usa2013P2.x_zero Base value: there is no sequence starting with u and ending with v when n = 0 line 211 source
Source documentation
Base value: there is no sequence starting with u and ending with v when n = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2013P2.countCol, OfNat.ofNat, Fin
Proof uses: id, Eq.mpr, Nat.card, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, HAdd.hAdd, Fin.last, Fintype.card, Ne, Fin.castSucc, Fin.succ, congrArg, Nat.card_eq_fintype_card, IsEmpty, propext, Fintype.card_eq_zero_iff, IsEmpty.mk, And.left and 11 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem x_zero : countCol 0 0 1 = 0 := by
…
```
Mentions: Usa2013P2.countCol
theorem Usa2013P2.y_zero Base value: exactly one sequence starts and ends with w when n = 0 line 220 source
Source documentation
Base value: exactly one sequence starts and ends with w when n = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2013P2.countCol, OfNat.ofNat, Fin
Proof uses: Unique, Subtype, Usa2013P2.ColSeq, And, Usa2013P2.AdjDistinct, HAdd.hAdd, Fin.last, Unique.mk, Inhabited.mk, Subtype.mk, And.intro, Fin.elim0, Ne, Fin.castSucc, Fin.succ, rfl, Subtype.ext, funext, Eq.mpr, id and 10 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem y_zero : countCol 0 2 2 = 1 := by
…
```
Mentions: Usa2013P2.countCol
theorem Usa2013P2.two_x_add_y The total number of sequences with fixed first column: 2 * x_n + y_n = 2^n line 232 source
Source documentation
The total number of sequences with fixed first column: 2 * x_n + y_n = 2^n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Usa2013P2.countCol, Fin, HPow.hPow
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Usa2013P2.x_zero, Usa2013P2.y_zero, Eq.refl, Usa2013P2.x_succ, Usa2013P2.y_succ, pow_succ
26 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem two_x_add_y (n : ℕ) : 2 * countCol n 0 1 + countCol n 2 2 = 2 ^ n := by
…
```
Mentions: Usa2013P2.countCol
theorem Usa2013P2.key The key identity: a_{n+1} + a_n = 2 ^ (n+1) line 240 source
Source documentation
The key identity: a_{n+1} + a_n = 2 ^ (n+1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, Usa2013P2.a, OfNat.ofNat, HPow.hPow
Proof uses: HMul.hMul, Usa2013P2.countCol, Fin, Usa2013P2.two_x_add_y, id, Eq.mpr, congrArg, Usa2013P2.x_succ, Usa2013P2.y_succ, pow_succ
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem key (n : ℕ) : a (n + 1) + a n = 2 ^ (n + 1) := by
…
```
Mentions: Usa2013P2.a
problem Usa2013P2.usa2013_p2 line 248 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, Usa2013P2.a, HSub.hSub, HPow.hPow
Proof uses: Usa2013P2.key, Eq.mp, congrArg
22 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.