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

22 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2023, Problem 4

Positive integers a and N are fixed, and N positive integers are written on a blackboard. Alice and Bob play the following game. On Alice's turn, she must replace some integer n on the board with n + a, and on Bob's turn he must replace some even integer n on the board with n/2. Alice goes first and they alternate turns. If Bob has no valid moves on his turn the game ends.

After analyzing the N integers on the board, Bob realizes that, regardless of what moves Alices makes, he will be able to force the game to end eventually. Show that, in fact, no matter what either player does, for these values of a and N and these particular N integers, the game is guaranteed to end, regardless of either player's moves.

Imports (2)

Imported by 1 file

Compfiles.lean

inductive Usa2023P4.Player line 36 source
no axioms what this means
abbrev Usa2023P4.Blackboard line 40 source
no axioms what this means
Statement uses: Nat
Proof uses: Fin, PNat
structure Usa2023P4.State line 42 source
no axioms what this means
Statement uses: Nat
theorem Usa2023P4.halve_even line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Even, Nat, LT.lt, OfNat.ofNat, HDiv.hDiv
Proof uses: Subtype.mk, Eq, HAdd.hAdd, id
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Usa2023P4.valid_moves line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, Usa2023P4.State, Set
Proof uses: Usa2023P4.valid_moves.match_1, Usa2023P4.Blackboard, Set.ofPred, Exists, Fin, Eq, Usa2023P4.State.mk, Function.update, HAdd.hAdd, Usa2023P4.Player.Bob, Even, Subtype.mk, LT.lt, OfNat.ofNat, HDiv.hDiv, Usa2023P4.Player.Alice
10 instances, coercions and auxiliary constants left out.
inductive Usa2023P4.BobCanForceEnd line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, Usa2023P4.State
inductive Usa2023P4.EndInevitable line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, Usa2023P4.State
lemma Usa2023P4.lemma1 The N=1 case is degenerate line 79 source
Source documentation
The N=1 case is degenerate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Usa2023P4.State, OfNat.ofNat, Nat, Usa2023P4.BobCanForceEnd, Usa2023P4.EndInevitable
Proof uses: Usa2023P4.BobCanForceEnd.rec, Usa2023P4.Blackboard, Eq, Set, Usa2023P4.valid_moves, Usa2023P4.State.mk, Usa2023P4.Player.Bob, EmptyCollection.emptyCollection, Usa2023P4.EndInevitable.BaseCase, Membership.mem, Usa2023P4.EndInevitable.Step, Fin, Exists, Even, Function.update, Subtype.mk, LT.lt, HDiv.hDiv, Usa2023P4.Player.Alice, Eq.mpr and 10 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma lemma1 (a : ℕ+) (s : State 1) (he : BobCanForceEnd a 1 s) :
    EndInevitable a 1 s := by
…
```
Mentions: Usa2023P4.State, Usa2023P4.BobCanForceEnd, Usa2023P4.EndInevitable
inductive Usa2023P4.EndInevitableIn end is inevitable in M moves line 97 source
Source documentation
end is inevitable in M moves

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, Usa2023P4.State
```
inductive EndInevitableIn (a : ℕ+) (n : ℕ) : ℕ → State n → Prop where
…
```
Mentions: Usa2023P4.State
lemma Usa2023P4.end_inevitable_n line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, Usa2023P4.State, Usa2023P4.EndInevitableIn, Usa2023P4.EndInevitable
Proof uses: Usa2023P4.EndInevitableIn.rec, Eq, Set, Usa2023P4.valid_moves, EmptyCollection.emptyCollection, Usa2023P4.EndInevitable.BaseCase, Usa2023P4.Blackboard, Membership.mem, Usa2023P4.State.mk, Usa2023P4.Player.Bob, Usa2023P4.EndInevitable.Step, Usa2023P4.Player.Alice
2 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P4.lemma3 line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2023P4.Blackboard, Eq, Finset.sum, Fin, Finset.univ, padicValNat, OfNat.ofNat, Not, Even
Proof uses: LT.lt, Dvd.dvd, Iff.mp, even_iff_two_dvd, HPow.hPow, Nat.succ, LE.le, Nat.pow_dvd_iff_le_padicValNat, PNat.ne_zero, Eq.mp, Membership.mem, Finset, congrArg, propext, Finset.sum_eq_zero_iff, AddUnits, Finset.mem_univ
42 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P4.lemma5 line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, padicValNat, HAdd.hAdd
Proof uses: Decidable.byContradiction, Not, Dvd.dvd, HPow.hPow, pow_padicValNat_dvd, Nat.pow_dvd_of_le_of_pow_dvd, Eq.mp, LE.le, Iff.mpr, Nat.dvd_add_iff_left, Iff.mp, Nat.pow_dvd_iff_le_padicValNat, Nat.ne_zero_of_lt
22 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P4.lemma5' line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, padicValNat, Eq, HAdd.hAdd
Proof uses: Dvd.dvd, HPow.hPow, pow_padicValNat_dvd, Exists, Nat.exists_eq_add_of_le, HMul.hMul, Eq.mpr, id, congrArg, Eq.mp, pow_add, add_assoc, mul_assoc, Eq.symm, mul_add, Eq.refl, Dvd.intro, LE.le, Iff.mp, Nat.pow_dvd_iff_le_padicValNat and 21 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P4.alice_move_preserves_nu line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, Usa2023P4.Blackboard, Fin, LT.lt, padicValNat, OfNat.ofNat, Usa2023P4.State, Membership.mem, Set, Usa2023P4.valid_moves, Usa2023P4.State.mk, Usa2023P4.Player.Alice, Usa2023P4.State.board
Proof uses: Eq, Function.update, HAdd.hAdd, Usa2023P4.Player.Bob, Exists, id, dite, Eq.mpr, congrArg, Function.update_self, Usa2023P4.lemma5, PNat.pos, Not, Function.update_of_ne, Ne.symm, Eq.symm
13 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P4.alice_move_preserves_nu' line 216 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, Usa2023P4.Blackboard, Fin, LT.lt, padicValNat, OfNat.ofNat, Usa2023P4.State, Membership.mem, Set, Usa2023P4.valid_moves, Usa2023P4.State.mk, Usa2023P4.Player.Alice, Eq, Usa2023P4.State.board
Proof uses: Function.update, HAdd.hAdd, Usa2023P4.Player.Bob, Exists, id, dite, Eq.mpr, congrArg, Function.update_self, Usa2023P4.lemma5', PNat.pos, Not, Function.update_of_ne, Ne.symm, Eq.refl, Eq.symm
13 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P4.bob_moves_after_alice line 239 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, Usa2023P4.Blackboard, Usa2023P4.State, Membership.mem, Set, Usa2023P4.valid_moves, Usa2023P4.State.mk, Usa2023P4.Player.Alice, Exists, Eq, Usa2023P4.Player.Bob
Proof uses: Fin, Function.update, HAdd.hAdd, of_eq_true, Eq.trans, True, congrArg, funext, And, Usa2023P4.Player, Usa2023P4.State.mk.injEq, eq_self, and_true, Eq.symm
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P4.lemma6 line 247 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Even, Eq, HAdd.hAdd, padicValNat, HDiv.hDiv
Proof uses: Dvd.dvd, Iff.mp, even_iff_two_dvd, LE.le, Eq.mpr, HPow.hPow, id, congrArg, Eq.symm, propext, Nat.pow_dvd_iff_le_padicValNat, pow_one, HSub.hSub, padicValNat.div
38 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P4.lemma2' When N ≥ 2, if ν2(x) < ν2(a) for all x ∈ S, the game must terminate in ∑_{x∈S} ν2(x) moves, no matter what either player does line 257 source
Source comment
When N ≥ 2, if ν2(x) < ν2(a) for all x ∈ S, the game must terminate in ∑_{x∈S} ν2(x) moves, no matter what either player does.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, LT.lt, OfNat.ofNat, Usa2023P4.State, Fin, padicValNat, Usa2023P4.State.board, Usa2023P4.EndInevitableIn, Finset.sum, Finset.univ
Proof uses: Nat.recAux, Eq, Not, Even, Usa2023P4.lemma3, Usa2023P4.Blackboard, Usa2023P4.Player, Usa2023P4.State.mk, Usa2023P4.Player.Bob, Usa2023P4.EndInevitableIn.BaseCase, id, Set, Usa2023P4.valid_moves, EmptyCollection.emptyCollection, Eq.mpr, Set.ofPred, Exists, Function.update, Subtype.mk, HDiv.hDiv and 52 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 158 steps
Open to load the checked before-and-after goal states.
```
lemma lemma2' (a : ℕ+) (N : ℕ) (hN : 1 < N) (s0 : State N)
    (hd : ∀ i : Fin N, padicValNat 2 (s0.board i) < padicValNat 2 a) :
    EndInevitableIn a N (∑ i : Fin N, padicValNat 2 (s0.board i)) s0 := by
…
```
Mentions: Usa2023P4.State, Usa2023P4.EndInevitableIn
lemma Usa2023P4.lemma2 When N ≥ 2, if ν2(x) < ν2(a) for all x ∈ S, the game must terminate no matter what either player does line 399 source
Source comment
When N ≥ 2, if ν2(x) < ν2(a) for all x ∈ S, the game must terminate no matter what either player does.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, LT.lt, OfNat.ofNat, Usa2023P4.State, Fin, padicValNat, Usa2023P4.State.board, Usa2023P4.EndInevitable
Proof uses: Usa2023P4.end_inevitable_n, Finset.sum, Finset.univ, Usa2023P4.lemma2'
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma lemma2 (a : ℕ+) (N : ℕ) (hN : 1 < N) (s0 : State N)
    (hd : ∀ i : Fin N, padicValNat 2 (s0.board i) < padicValNat 2 a) :
    EndInevitable a N s0 := by
…
```
Mentions: Usa2023P4.State, Usa2023P4.EndInevitable
lemma Usa2023P4.lemma7 Key fact: when ν₂(x) = ν₂(a), ν₂(x+a) ≥ ν₂(a) + 1 line 405 source
Source comment
Key fact: when ν₂(x) = ν₂(a), ν₂(x+a) ≥ ν₂(a) + 1

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, padicValNat, LE.le, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, rfl, Dvd.dvd, HPow.hPow, Eq.symm, Eq.mp, pow_padicValNat_dvd, HMul.hMul, Not, False, pow_succ, mul_dvd_mul_left, dvd_mul_right, Iff.mp, Nat.pow_dvd_iff_le_padicValNat, HMod.hMod, propext, Nat.dvd_iff_mod_eq_zero and 3 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma lemma7 {x a : ℕ} (hx : 0 < x) (ha : 0 < a)
    (heq : padicValNat 2 x = padicValNat 2 a) :
    padicValNat 2 a + 1 ≤ padicValNat 2 (x + a) := by
…
```
lemma Usa2023P4.alice_prevents_end When N ≥ 2, if ∃ i with ν₂(b i) ≥ ν₂(a) (+ offset by turn), then ¬BobCanForceEnd line 436 source
Source comment
When N ≥ 2, if ∃ i with ν₂(b i) ≥ ν₂(a) (+ offset by turn), then ¬BobCanForceEnd.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, LT.lt, OfNat.ofNat, Usa2023P4.State, Usa2023P4.BobCanForceEnd, Exists, Fin, LE.le, HAdd.hAdd, padicValNat, Usa2023P4.alice_prevents_end.match_1, Usa2023P4.Player, Usa2023P4.State.turn, Unit, Usa2023P4.State.board, False
Proof uses: Usa2023P4.BobCanForceEnd.rec, Usa2023P4.Blackboard, Eq, Set, Usa2023P4.valid_moves, Usa2023P4.State.mk, Usa2023P4.Player.Bob, EmptyCollection.emptyCollection, Even, Eq.mpr, Dvd.dvd, id, congrArg, propext, even_iff_two_dvd, Nat.dvd_of_pow_dvd, pow_padicValNat_dvd, Eq.mp, Not, Membership.mem and 26 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
```
lemma alice_prevents_end (a : ℕ+) (N : ℕ) (hN : 1 < N)
    (s : State N) (he : BobCanForceEnd a N s)
    (hinv : ∃ i : Fin N,
      padicValNat 2 ↑a + (match s.turn with | .Alice => 0 | .Bob => 1) ≤
      padicValNat 2 ↑(s.board i)) :
    False := by
…
```
Mentions: Usa2023P4.State, Usa2023P4.BobCanForceEnd
problem Usa2023P4.usa2023_p4 line 488 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PNat, Nat, LT.lt, OfNat.ofNat, Usa2023P4.Blackboard, Usa2023P4.BobCanForceEnd, Usa2023P4.State.mk, Usa2023P4.Player.Alice, Usa2023P4.EndInevitable
Proof uses: Eq, Or, LE.le.eq_or_lt, Usa2023P4.lemma1, Fin, padicValNat, Decidable.byContradiction, Not, LE.le, Exists, False, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Usa2023P4.alice_prevents_end, Exists.intro, HAdd.hAdd, Usa2023P4.alice_prevents_end.match_1 and 6 more
20 instances, coercions and auxiliary constants left out.

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