`Compfiles/Usa1996P4.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

19 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1996, Problem 4

An n-term sequence (x₁, x₂, …, xₙ) in which each term is either 0 or 1 is called a binary sequence of length n. Let aₙ be the number of binary sequences of length n containing no three consecutive terms equal to 0, 1, 0 in that order. Let bₙ be the number of binary sequences of length n that contain no four consecutive terms equal to 0, 0, 1, 1 or 1, 1, 0, 0 in that order. Prove that bₙ₊₁ = 2aₙ for all positive integers n.

Imports (2)

Imported by 1 file

Compfiles.lean

def Usa1996P4.sget The i-th term of a binary sequence x : Fin n → Bool, or false if i is out of range line 31 source
Source documentation
The i-th term of a binary sequence x : Fin n → Bool, or false if i is out of range.

no axioms what this means
Statement uses: Nat, Fin, Bool
Proof uses: dite, LT.lt, Fin.mk, Not, Bool.false
2 instances, coercions and auxiliary constants left out.
```
def sget {n : ℕ} (x : Fin n → Bool) (i : ℕ) : Bool :=
…
```
abbrev Usa1996P4.GoodA Documented declaration: GoodA line 37 source
Source documentation
A binary sequence of length n (encoded as x : Fin n → Bool, with false standing for 0 and true for 1) is A-good if it contains no three consecutive terms equal to 0, 1, 0 in that order.

no axioms what this means
Statement uses: Nat, Fin, Bool
Proof uses: LT.lt, HAdd.hAdd, OfNat.ofNat, Not, And, Eq, Usa1996P4.sget, Bool.false, Bool.true
5 instances, coercions and auxiliary constants left out.
```
abbrev GoodA {n : ℕ} (x : Fin n → Bool) : Prop :=
…
```
abbrev Usa1996P4.GoodB A binary sequence of length n is B-good if it contains no four consecutive terms equal to 0, 0, 1, 1 or 1, 1, 0, 0 in that order line 43 source
Source documentation
A binary sequence of length n is B-good if it contains no four consecutive terms equal to 0, 0, 1, 1 or 1, 1, 0, 0 in that order.

no axioms what this means
Statement uses: Nat, Fin, Bool
Proof uses: LT.lt, HAdd.hAdd, OfNat.ofNat, Not, Or, And, Eq, Usa1996P4.sget, Bool.false, Bool.true
5 instances, coercions and auxiliary constants left out.
```
abbrev GoodB {n : ℕ} (y : Fin n → Bool) : Prop :=
…
```
theorem Usa1996P4.sget_lt line 52 source
no axioms what this means
Statement uses: Nat, Fin, Bool, LT.lt, Eq, Usa1996P4.sget, Fin.mk
Proof uses: dite_eq_left, Not, Bool.false
3 instances, coercions and auxiliary constants left out.
def Usa1996P4.diff The sequence of successive differences (XORs) of y line 57 source
Source documentation
The sequence of successive differences (XORs) of y.

no axioms what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Bool
Proof uses: Bool.xor, Usa1996P4.sget
7 instances, coercions and auxiliary constants left out.
```
def diff {n : ℕ} (y : Fin (n + 1) → Bool) : Fin n → Bool :=
…
```
def Usa1996P4.buildAux Auxiliary for build: the k-th term of the sequence with first term c and successive differences given by x line 62 source
Source documentation
Auxiliary for build: the k-th term of the sequence with first term c and successive differences given by x.

no axioms what this means
Statement uses: Nat, Fin, Bool
2 instances, coercions and auxiliary constants left out.
```
def buildAux {n : ℕ} (x : Fin n → Bool) (c : Bool) : ℕ → Bool
  | 0 => c
  | k + 1 => xor (buildAux x c k) (sget x k)

/-- The sequence of length `n + 1` with first term `c` whose successive
differences are given by `x`. -/
```
Mentions: Usa1996P4.sget
def Usa1996P4.build The sequence of length n + 1 with first term c whose successive differences are given by x line 68 source
Source documentation
The sequence of length n + 1 with first term c whose successive differences are given by x.

no axioms what this means
Statement uses: Nat, Fin, Bool, HAdd.hAdd, OfNat.ofNat
Proof uses: Usa1996P4.buildAux
7 instances, coercions and auxiliary constants left out.
```
def build {n : ℕ} (x : Fin n → Bool) (c : Bool) : Fin (n + 1) → Bool :=
…
```
theorem Usa1996P4.build_zero line 71 source
standard axioms: propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa1996P4.build, OfNat.ofNat, HAdd.hAdd
Proof uses: id, of_eq_true, eq_self
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa1996P4.buildAux_succ line 76 source
standard axioms: propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa1996P4.buildAux, HAdd.hAdd, OfNat.ofNat, Bool.xor, Usa1996P4.sget
Proof uses: of_eq_true, eq_self
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Usa1996P4.sget_build line 80 source
no axioms what this means
Statement uses: Nat, Fin, Bool, LT.lt, HAdd.hAdd, OfNat.ofNat, Eq, Usa1996P4.sget, Usa1996P4.build, Usa1996P4.buildAux
Proof uses: dite_eq_left, Fin.mk, Not, Bool.false
9 instances, coercions and auxiliary constants left out.
theorem Usa1996P4.sget_diff_build line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, LT.lt, Eq, Bool.xor, Usa1996P4.sget, HAdd.hAdd, OfNat.ofNat, Usa1996P4.build
Proof uses: Eq.mpr, Usa1996P4.buildAux, id, congrArg, Usa1996P4.sget_build, Usa1996P4.buildAux_succ, Bool.bne_self_left
10 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Usa1996P4.sget_diff line 93 source
no axioms what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Bool, LT.lt, Eq, Bool.xor, Usa1996P4.sget, Usa1996P4.diff
Proof uses: Eq.mpr, Fin.mk, id, congrArg, Usa1996P4.sget_lt, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa1996P4.pattern_transfer A block 0,0,1,1 or 1,1,0,0 in y at position i corresponds exactly to a block 0,1,0 in the difference sequence of y at position i line 101 source
Source documentation
A block 0,0,1,1 or 1,1,0,0 in y at position i corresponds exactly to a block 0,1,0 in the difference sequence of y at position i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Bool, LT.lt, Eq, Bool.xor, Usa1996P4.sget, Iff, Or, And, Bool.false, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem pattern_transfer {n : ℕ} {y : Fin (n + 1) → Bool} {x : Fin n → Bool}
    (hxe : ∀ j : ℕ, j < n → xor (sget y j) (sget y (j + 1)) = sget x j)
    {i : ℕ} (hi : i + 3 < n + 1) :
    ((sget y i = false ∧ sget y (i + 1) = false ∧ sget y (i + 2) = true ∧
        sget y (i + 3) = true) ∨
      (sget y i = true ∧ sget y (i + 1) = true ∧ sget y (i + 2) = false ∧
        sget y (i + 3) = false)) ↔
    (sget x i = false ∧ sget x (i + 1) = true ∧ sget x (i + 2) = false) := by
…
```
Mentions: Usa1996P4.sget
theorem Usa1996P4.goodB_build line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Usa1996P4.GoodA, Usa1996P4.GoodB, HAdd.hAdd, OfNat.ofNat, Usa1996P4.build
Proof uses: LT.lt, Or, And, Eq, Usa1996P4.sget, Bool.false, Bool.true, Iff.mp, Usa1996P4.pattern_transfer, Usa1996P4.sget_diff_build, Fin.mk, id
10 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Usa1996P4.goodA_diff line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Bool, Usa1996P4.GoodB, Usa1996P4.GoodA, Usa1996P4.diff
Proof uses: LT.lt, And, Eq, Usa1996P4.sget, Bool.false, Bool.true, Or, Iff.mpr, Usa1996P4.pattern_transfer, Usa1996P4.sget_diff, Fin.mk, id
10 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem Usa1996P4.diff_build line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa1996P4.diff, Usa1996P4.build
Proof uses: funext, id, Eq.mpr, Bool.xor, Usa1996P4.sget, HAdd.hAdd, OfNat.ofNat, congrArg, Usa1996P4.sget_diff_build, Fin.isLt, Fin.mk, Usa1996P4.sget_lt, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa1996P4.build_diff line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Bool, Eq, Usa1996P4.build, Usa1996P4.diff
Proof uses: funext, LT.lt, id, Fin.mk, Nat.recAux, Usa1996P4.buildAux, of_eq_true, eq_self, Eq.mpr, congrArg, Nat.zero_lt_succ, Fin.zero_eta, Eq.refl, Bool.xor, Usa1996P4.sget, Usa1996P4.buildAux_succ, Eq.symm, Usa1996P4.sget_diff, Usa1996P4.sget_lt, Bool.bne_self_left
16 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
def Usa1996P4.seqEquiv Documented declaration: seqEquiv line 172 source
Source documentation
The 2-to-1 correspondence: a B-good sequence of length n + 1 is determined by its first term (two choices) and its difference sequence, which is an A-good sequence of length n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Prod, Subtype, Fin, Bool, Usa1996P4.GoodA, HAdd.hAdd, OfNat.ofNat, Usa1996P4.GoodB
Proof uses: Equiv.mk, Usa1996P4.seqEquiv.match_1, Subtype.mk, Usa1996P4.build, Prod.mk, Usa1996P4.diff
13 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def seqEquiv (n : ℕ) :
    {x : Fin n → Bool // GoodA x} × Bool ≃ {y : Fin (n + 1) → Bool // GoodB y} where
…
```
Mentions: Usa1996P4.GoodA, Usa1996P4.GoodB
problem Usa1996P4.usa1996_p4 line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Fintype.card, Subtype, Fin, HAdd.hAdd, OfNat.ofNat, Bool, Usa1996P4.GoodB, LT.lt, Not, Or, And, Usa1996P4.sget, Bool.false, Bool.true, HMul.hMul, Usa1996P4.GoodA
Proof uses: Prod, Fintype.card_congr, Usa1996P4.seqEquiv, Eq.mp, congrArg, Fintype.card_bool, Fintype.card_prod
40 instances, coercions and auxiliary constants left out.

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