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

34 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2025, Problem 5

Alice and Bazza are playing the inekoalaty game, a two-player game whose rules depend on a positive number λ known to both players. On the nth turn of the game (starting with n = 1) the following happens:

If n is odd, Alice chooses a nonnegative real number xₙ such that
x₁ + x₂ + ... + xₙ ≤ λn
If n is even, Bazza chooses a nonnegative real number xₙ such that
x₁² + x₂² + .. + xₙ² ≤ n.

If a player cannot choose a suitable n, the game ends and the other player wins. If the game goes forever, neither player wins. All chosen numbers are known to both players.

Determine all values of λ for which Alice has a winning strategy and all those for which Bazza has a winning strategy.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo2025P5.ValidSeq Whether all the numbers chosen are valid line 45 source
Source documentation
Whether all the numbers chosen are valid.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Fin
Proof uses: And, LE.le, OfNat.ofNat, Even, Finset.sum, Finset.Iic, HMul.hMul, HAdd.hAdd, Odd, HPow.hPow
23 instances, coercions and auxiliary constants left out.
```
def ValidSeq (c : ℝ) {n : ℕ} (x : Fin n → ℝ) : Prop := (∀ i : Fin n, 0 ≤ x i) ∧
…
```
def Imo2025P5.Wins Whether a sequence of numbers chosen is a win for the given player (expressed as the 0-based numbers of that player's moves, mod 2): the other player makes the first invalid move line 51 source
Source documentation
Whether a sequence of numbers chosen is a win for the given player (expressed as the 0-based numbers of that player's moves, mod 2): the other player makes the first invalid move.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Fin
Proof uses: Exists, And, Ne, HMod.hMod, OfNat.ofNat, IsLeast, Set.ofPred, Not, Imo2025P5.ValidSeq, HAdd.hAdd, Fin.take
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def Wins (c : ℝ) (p : ℕ) {n : ℕ} (x : Fin n → ℝ) : Prop := ∃ i : Fin n, (i : ℕ) % 2 ≠ p ∧
…
```
abbrev Imo2025P5.Strategy Documented declaration: Strategy line 58 source
Source documentation
A strategy for a given player gives a choice of number in every position, with the convention that invalid moves lose and the strategy's choices are ignored in cases where it is not that player's turn, a previous move was invalid or the sequence of previous moves is not possible under the strategy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: Nat, Fin, Real
```
abbrev Strategy : Type := ⦃k : ℕ⦄ → (Fin k → ℝ) → ℝ
```
def Imo2025P5.Strategy.play Playing a strategy, k turns, against a given sequence of opponent moves (possibly not valid) line 62 source
Source documentation
Playing a strategy, k turns, against a given sequence of opponent moves (possibly not valid).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy, Nat, Real, Fin
2 instances, coercions and auxiliary constants left out.
```
def Strategy.play (s : Strategy) (p : ℕ) (opponentMoves : ℕ → ℝ) : (k : ℕ) → Fin k → ℝ
| 0 => Fin.elim0
| k + 1 => Fin.snoc (s.play p opponentMoves k)
    (if k % 2 = p then s (s.play p opponentMoves k) else opponentMoves k)

/-- Whether a strategy wins for the given player, against all possible opponent moves. -/
```
Mentions: Imo2025P5.Strategy
def Imo2025P5.Strategy.Winning Whether a strategy wins for the given player, against all possible opponent moves line 68 source
Source documentation
Whether a strategy wins for the given player, against all possible opponent moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy, Real, Nat
Proof uses: Exists, Imo2025P5.Wins, Imo2025P5.Strategy.play
```
def Strategy.Winning (s : Strategy) (c : ℝ) (p : ℕ) : Prop :=
…
```
Mentions: Imo2025P5.Strategy
determine Imo2025P5.answer The answer to be determined line 72 source
Source documentation
The answer to be determined.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Set, Real
Proof uses: Prod.mk, Set.ofPred, LT.lt, HDiv.hDiv, Real.sqrt, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
determine answer : Set ℝ × Set ℝ :=
…
```
def Imo2025P5.ValidAt Validity of the move at (0-based) index j of the infinite sequence x, as a statement about natural-number-indexed sequences line 109 source
Source documentation
Validity of the move at (0-based) index j of the infinite sequence x, as a statement about natural-number-indexed sequences.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat
Proof uses: And, LE.le, OfNat.ofNat, Even, Finset.sum, Finset.range, HAdd.hAdd, HMul.hMul, Odd, HPow.hPow
19 instances, coercions and auxiliary constants left out.
```
def ValidAt (c : ℝ) (x : ℕ → ℝ) (j : ℕ) : Prop :=
…
```
lemma Imo2025P5.sum_Iic_coe line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Fin, Eq, Finset.sum, Finset.Iic, Finset.range, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Finset, Nat.range_succ_eq_Iic, Finset.map, Fin.valEmbedding, Eq.symm, Fin.map_valEmbedding_Iic, Function.Embedding, Finset.sum_map, Eq.refl
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P5.validSeq_iff ValidSeq for a length-n window of an infinite sequence, in terms of ValidAt line 120 source
Source documentation
ValidSeq for a length-n window of an infinite sequence, in terms of ValidAt.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Iff, Imo2025P5.ValidSeq, Fin, LT.lt, Imo2025P5.ValidAt
Proof uses: Iff.intro, LE.le, OfNat.ofNat, And, Even, Finset.sum, Finset.Iic, HMul.hMul, HAdd.hAdd, Odd, HPow.hPow, And.intro, Finset.range, Fin.mk, Eq.mp, congrArg, Imo2025P5.sum_Iic_coe, And.left, Fin.isLt, Eq.mpr and 3 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma validSeq_iff (c : ℝ) (x : ℕ → ℝ) (n : ℕ) :
    ValidSeq c (fun i : Fin n => x i) ↔ ∀ j < n, ValidAt c x j := by
…
```
Mentions: Imo2025P5.ValidSeq, Imo2025P5.ValidAt
lemma Imo2025P5.take_coe line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, Eq, Fin, Fin.take
Proof uses: funext, of_eq_true, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P5.wins_iff Wins for a length-n window of an infinite sequence, in terms of ValidAt line 142 source
Source documentation
Wins for a length-n window of an infinite sequence, in terms of ValidAt.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Iff, Imo2025P5.Wins, Fin, Exists, And, LT.lt, Ne, HMod.hMod, OfNat.ofNat, Imo2025P5.ValidAt, Not
Proof uses: id, Eq.mpr, IsLeast, Set.ofPred, Imo2025P5.ValidSeq, HAdd.hAdd, Fin.take, Eq, congrFun', congrArg, funext, Set, Eq.trans, Imo2025P5.take_coe, Iff.intro, Membership.mem, lowerBounds, Classical.byContradiction, Fin.mk, lt_trans and 15 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma wins_iff (c : ℝ) (p : ℕ) (x : ℕ → ℝ) (n : ℕ) :
    Wins c p (fun i : Fin n => x i) ↔
      ∃ j < n, j % 2 ≠ p ∧ (∀ m < j, ValidAt c x m) ∧ ¬ ValidAt c x j := by
…
```
Mentions: Imo2025P5.Wins, Imo2025P5.ValidAt
def Imo2025P5.Strategy.playSeq The infinite sequence of moves of a play line 175 source
Source documentation
The infinite sequence of moves of a play.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy, Nat, Real
Proof uses: Imo2025P5.Strategy.play, HAdd.hAdd, OfNat.ofNat, Fin.mk, Nat.lt_succ_self
3 instances, coercions and auxiliary constants left out.
```
def Strategy.playSeq (s : Strategy) (p : ℕ) (om : ℕ → ℝ) (j : ℕ) : ℝ :=
…
```
Mentions: Imo2025P5.Strategy
lemma Imo2025P5.play_castLE line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy, Nat, Real, LE.le, Fin, Eq, Imo2025P5.Strategy.play, Fin.castLE
Proof uses: Nat.recAux, OfNat.ofNat, Fin.elim0, Eq.symm, HAdd.hAdd, LT.lt, Or, Iff.mp, Nat.succ, Nat.lt_succ_iff_lt_or_eq, Nat.lt_succ_of_le, Fin.castSucc, Fin.ext, of_eq_true, eq_self, Eq.mpr, id, congrArg, congrFun', Fin.snoc_castSucc and 3 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P5.play_eq_playSeq line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy, Nat, Real, Eq, Fin, Imo2025P5.Strategy.play, Imo2025P5.Strategy.playSeq
Proof uses: funext, LE.le, HAdd.hAdd, OfNat.ofNat, Fin.isLt, Fin.castLE, Fin.mk, Nat.lt_succ_self, Imo2025P5.play_castLE, Eq.mp, congrArg, Fin.ext, rfl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P5.playSeq_apply line 207 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy, Nat, Real, Eq, Imo2025P5.Strategy.playSeq, ite, HMod.hMod, OfNat.ofNat, Fin
Proof uses: Fin.snoc, HAdd.hAdd, Imo2025P5.Strategy.play, Fin.last, rfl, Eq.mpr, id, congrArg, Fin.snoc_last, Imo2025P5.play_eq_playSeq, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Imo2025P5.respSeq The sequence of moves arising when the player with parity p plays the strategy s and the opponent always responds according to r line 216 source
Source documentation
The sequence of moves arising when the player with parity p plays the strategy s and the opponent always responds according to r.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy, Nat, Real
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, dite, Eq, HMod.hMod, OfNat.ofNat, Fin, Not
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def respSeq (s : Strategy) (p : ℕ) (r : Strategy) : ℕ → ℝ
  | j => if j % 2 = p then s (fun i : Fin j => respSeq s p r (i : ℕ))
         else r (fun i : Fin j => respSeq s p r (i : ℕ))
  termination_by j => j
  decreasing_by all_goals exact i.isLt
```
Mentions: Imo2025P5.Strategy
lemma Imo2025P5.play_respSeq line 222 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy, Nat, Eq, Fin, Real, Imo2025P5.Strategy.play, Imo2025P5.respSeq
Proof uses: Nat.recAux, funext, OfNat.ofNat, Fin.elim0, HAdd.hAdd, Eq.mpr, Fin.snoc, ite, HMod.hMod, id, congrFun', congrArg, congr, ite_congr, Eq.refl, Not, Fin.lastCases, Fin.last, Fin.snoc_last, dite and 9 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P5.exists_first_invalid A first invalid index exists as soon as any invalid index does line 243 source
Source documentation
A first invalid index exists as soon as any invalid index does.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, Exists, Not, Imo2025P5.ValidAt, And, LT.lt
Proof uses: Exists.intro, Nat.find, Classical.propDecidable, And.intro, Iff.mp, Classical.not_not, Nat.find_min, Nat.find_spec
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma exists_first_invalid {c : ℝ} {x : ℕ → ℝ} (hex : ∃ j, ¬ ValidAt c x j) :
    ∃ j, (∀ m < j, ValidAt c x m) ∧ ¬ ValidAt c x j := by
…
```
Mentions: Imo2025P5.ValidAt
lemma Imo2025P5.le_of_sq_le_sq' If 0 ≤ b and a ^ 2 ≤ b ^ 2 then a ≤ b line 249 source
Source documentation
If 0 ≤ b and a ^ 2 ≤ b ^ 2 then a ≤ b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HPow.hPow, Nat
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, HMul.hMul, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 62 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma le_of_sq_le_sq' {a b : ℝ} (hb : 0 ≤ b) (h : a ^ 2 ≤ b ^ 2) : a ≤ b := by
…
```
Mentions: h
lemma Imo2025P5.sum_range_two_mul line 252 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Finset.sum, Finset.range, HMul.hMul, OfNat.ofNat, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection, Finset, MulZeroClass.mul_zero, eq_self, Eq.mpr, id, congr, Finset.sum_congr, mul_add, mul_one, Membership.mem, Eq.refl, Finset.sum_range_succ, Eq.symm and 8 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo2025P5.sum_le_sqrt_two_mul Cauchy-Schwarz bound: if a sequence vanishes at even indices below 2 * k, is nonnegative there, and its squares sum to at most 2 * k, then its sum is at most √2 * k line 262 source
Source documentation
Cauchy-Schwarz bound: if a sequence vanishes at even indices below 2 * k, is nonnegative there, and its squares sum to at most 2 * k, then its sum is at most √2 * k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LT.lt, HMul.hMul, OfNat.ofNat, Even, Eq, LE.le, Finset.sum, Finset.range, HPow.hPow, Real.sqrt
Proof uses: HAdd.hAdd, Eq.mpr, id, congrArg, Imo2025P5.sum_range_two_mul, Finset.sum_congr, rfl, Finset, Membership.mem, Eq.mp, propext, Finset.mem_range, even_two_mul, zero_add, Eq.refl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_zero and 47 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma sum_le_sqrt_two_mul (x : ℕ → ℝ) (k : ℕ)
    (h0 : ∀ i < 2 * k, Even i → x i = 0)
    (hQ : ∑ i ∈ range (2 * k), x i ^ 2 ≤ 2 * (k : ℝ)) :
    ∑ i ∈ range (2 * k), x i ≤ Real.sqrt 2 * k := by
…
```
lemma Imo2025P5.sqrt_two_le_add If a, b ≥ 0 and a² + b² = 2 then a + b ≥ √2 line 293 source
Source documentation
If a, b ≥ 0 and a² + b² = 2 then a + b ≥ √2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, Nat, Real.sqrt
Proof uses: Imo2025P5.le_of_sq_le_sq', add_nonneg, Eq.mpr, id, congrArg, Real.sq_sqrt, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, HMul.hMul and 71 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma sqrt_two_le_add {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (h : a ^ 2 + b ^ 2 = 2) :
    Real.sqrt 2 ≤ a + b := by
…
```
Mentions: h
lemma Imo2025P5.bazza_step Documented declaration: bazza_step line 307 source
Source documentation
One round of greedy play when c ≤ √2/2, assuming the invariant after 2k moves and the validity of Alice's move at index 2k: Alice's move is at most √2/2, so Bazza's greedy reply at index 2k + 1 exists, and the squares of the pair sum to 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, LE.le, HDiv.hDiv, Real.sqrt, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, HSub.hSub, Finset.sum, Finset.range, HPow.hPow, Imo2025P5.ValidAt, And
Proof uses: Even, Odd, even_two_mul, mul_le_mul_of_nonneg_right, le_of_lt, Right.add_pos_of_nonneg_of_pos, mul_nonneg, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Nat.cast_nonneg', Nat.cast_one, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance and 107 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma bazza_step {c : ℝ} {x : ℕ → ℝ} (hc : c ≤ Real.sqrt 2 / 2) {k : ℕ}
    (hb : x (2 * k + 1) =
      Real.sqrt (((2 * k + 1 : ℕ) : ℝ) + 1 - ∑ i ∈ range (2 * k + 1), x i ^ 2))
    (hQ : ∑ i ∈ range (2 * k), x i ^ 2 = 2 * (k : ℝ))
    (hS : Real.sqrt 2 * k ≤ ∑ i ∈ range (2 * k), x i)
    (hv : ValidAt c x (2 * k)) :
    ∑ i ∈ range (2 * k + 1), x i ^ 2 = 2 * (k : ℝ) + x (2 * k) ^ 2 ∧
      0 ≤ x (2 * k + 1) ∧ x (2 * k + 1) ^ 2 = 2 - x (2 * k) ^ 2 := by
…
```
Mentions: Imo2025P5.ValidAt
lemma Imo2025P5.bazza_invariant Documented declaration: bazza_invariant line 336 source
Source documentation
Invariant of greedy play when c ≤ √2/2: while all moves so far are valid, the sum of squares after Bazza's move at index 2k - 1 is exactly 2k, and the plain sum is at least √2 * k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, LE.le, HDiv.hDiv, Real.sqrt, OfNat.ofNat, Odd, Eq, HSub.hSub, HAdd.hAdd, Finset.sum, Finset.range, HPow.hPow, LT.lt, HMul.hMul, Imo2025P5.ValidAt, And
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, implies_congr, forall_congr, False, congrArg, MulZeroClass.mul_zero, Eq.refl, implies_true, congr, congrFun', EmptyCollection.emptyCollection, Finset, CharP.cast_eq_zero, eq_self, and_self, Imo2025P5.bazza_step, Iff.mpr and 72 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma bazza_invariant {c : ℝ} {x : ℕ → ℝ} (hc : c ≤ Real.sqrt 2 / 2)
    (hgreedy : ∀ j, Odd j → x j = Real.sqrt ((j : ℝ) + 1 - ∑ i ∈ range j, x i ^ 2)) :
    ∀ k : ℕ, (∀ m < 2 * k, ValidAt c x m) →
      ∑ i ∈ range (2 * k), x i ^ 2 = 2 * (k : ℝ) ∧
        Real.sqrt 2 * k ≤ ∑ i ∈ range (2 * k), x i := by
…
```
Mentions: Imo2025P5.ValidAt
lemma Imo2025P5.bazza_validAt_odd When c ≤ √2/2 and Bazza plays greedily, no odd index is ever the first invalid one line 362 source
Source documentation
When c ≤ √2/2 and Bazza plays greedily, no odd index is ever the first invalid one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, LE.le, HDiv.hDiv, Real.sqrt, OfNat.ofNat, Odd, Eq, HSub.hSub, HAdd.hAdd, Finset.sum, Finset.range, HPow.hPow, LT.lt, Imo2025P5.ValidAt
Proof uses: HMul.hMul, Exists, Exists.intro, Eq.mp, HMod.hMod, congrArg, propext, Nat.odd_iff, And, Imo2025P5.bazza_invariant, Imo2025P5.bazza_step, Iff.mpr, And.intro, Even, False.elim, Nat.even_iff, Eq.mpr, id, Finset.sum_range_succ, congrFun' and 63 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma bazza_validAt_odd {c : ℝ} {x : ℕ → ℝ} (hc : c ≤ Real.sqrt 2 / 2)
    (hgreedy : ∀ j, Odd j → x j = Real.sqrt ((j : ℝ) + 1 - ∑ i ∈ range j, x i ^ 2)) :
    ∀ j, Odd j → (∀ m < j, ValidAt c x m) → ValidAt c x j := by
…
```
Mentions: Imo2025P5.ValidAt
def Imo2025P5.bazzaStrategy Bazza's greedy strategy: spend the entire quadratic budget line 382 source
Source documentation
Bazza's greedy strategy: spend the entire quadratic budget.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy
Proof uses: Nat, Fin, Real, Real.sqrt, HSub.hSub, HAdd.hAdd, OfNat.ofNat, Finset.sum, Finset.univ, HPow.hPow
15 instances, coercions and auxiliary constants left out.
```
noncomputable def bazzaStrategy : Strategy := fun k h => Real.sqrt ((k : ℝ) + 1 - ∑ i, h i ^ 2)
```
Mentions: Imo2025P5.Strategy, h
def Imo2025P5.zeroStrategy The all-zeros strategy line 385 source
Source documentation
The all-zeros strategy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2025P5.Strategy
Proof uses: Nat, Fin, Real, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def zeroStrategy : Strategy := fun _ _ => 0
```
Mentions: Imo2025P5.Strategy
lemma Imo2025P5.alice_not_wins If c ≤ √2/2 then Alice has no winning strategy: Bazza survives greedy play forever line 388 source
Source documentation
If c ≤ √2/2 then Alice has no winning strategy: Bazza survives greedy play forever.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, HDiv.hDiv, Real.sqrt, OfNat.ofNat, Nat, Not, Exists, Imo2025P5.Strategy, Imo2025P5.Strategy.Winning
Proof uses: False, Imo2025P5.Wins, Imo2025P5.Strategy.play, Imo2025P5.respSeq, Imo2025P5.bazzaStrategy, And, LT.lt, Ne, HMod.hMod, Imo2025P5.ValidAt, Eq.mp, Fin, congrArg, propext, Imo2025P5.wins_iff, Imo2025P5.play_respSeq, Odd, Eq, HSub.hSub, HAdd.hAdd and 14 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma alice_not_wins {c : ℝ} (hc : c ≤ Real.sqrt 2 / 2) :
    ¬ ∃ s : Strategy, s.Winning c 0 := by
…
```
Mentions: Imo2025P5.Strategy
lemma Imo2025P5.bazza_wins If c < √2/2 then Bazza's greedy strategy wins line 403 source
Source documentation
If c < √2/2 then Bazza's greedy strategy wins.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, HDiv.hDiv, Real.sqrt, OfNat.ofNat, Nat, Exists, Imo2025P5.Strategy, Imo2025P5.Strategy.Winning
Proof uses: Exists.intro, Imo2025P5.bazzaStrategy, Imo2025P5.Strategy.playSeq, Eq, rfl, Odd, HSub.hSub, HAdd.hAdd, Finset.sum, Finset.range, HPow.hPow, Eq.mpr, id, congrArg, ite, HMod.hMod, Fin, Imo2025P5.playSeq_apply, ite_eq_left, Iff.mp and 105 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma bazza_wins {c : ℝ} (hc : c < Real.sqrt 2 / 2) : ∃ s : Strategy, s.Winning c 1 := by
…
```
Mentions: Imo2025P5.Strategy
lemma Imo2025P5.zeros_sum_le The partial-sum bound coming from Cauchy-Schwarz, for play in which Alice has played all zeros so far line 443 source
Source documentation
The partial-sum bound coming from Cauchy-Schwarz, for play in which Alice has played all zeros so far.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, LT.lt, HMul.hMul, OfNat.ofNat, Even, Eq, Imo2025P5.ValidAt, LE.le, Finset.sum, Finset.range, Real.sqrt
Proof uses: Imo2025P5.sum_le_sqrt_two_mul, Nat.casesAuxOn, HPow.hPow, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', EmptyCollection.emptyCollection, Finset, MulZeroClass.mul_zero, CharP.cast_eq_zero, Eq.symm, HAdd.hAdd, And.right, Odd, And, Iff.mpr, HMod.hMod and 62 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma zeros_sum_le {c : ℝ} {x : ℕ → ℝ} (t : ℕ)
    (h0 : ∀ i < 2 * t, Even i → x i = 0)
    (hvalid : ∀ m < 2 * t, ValidAt c x m) :
    ∑ i ∈ range (2 * t), x i ≤ Real.sqrt 2 * t := by
…
```
Mentions: Imo2025P5.ValidAt
lemma Imo2025P5.zeros_validAt_even If c ≥ √2/2 and all of Alice's moves up to an even index 2 * t are 0, then her move at 2 * t is valid line 458 source
Source documentation
If c ≥ √2/2 and all of Alice's moves up to an even index 2 * t are 0, then her move at 2 * t is valid.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Nat, LE.le, HDiv.hDiv, Real.sqrt, OfNat.ofNat, HMul.hMul, Even, Eq, LT.lt, Imo2025P5.ValidAt
Proof uses: le_rfl, even_two_mul, Finset.sum, Finset.range, Imo2025P5.zeros_sum_le, And.intro, And, HAdd.hAdd, Odd, HPow.hPow, le_of_eq, Eq.symm, Eq.mpr, id, congrArg, Finset.sum_range_succ, add_zero, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 87 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma zeros_validAt_even {c : ℝ} {x : ℕ → ℝ} (hc : Real.sqrt 2 / 2 ≤ c) (t : ℕ)
    (h0 : ∀ i ≤ 2 * t, Even i → x i = 0)
    (hvalid : ∀ m < 2 * t, ValidAt c x m) :
    ValidAt c x (2 * t) := by
…
```
Mentions: Imo2025P5.ValidAt
lemma Imo2025P5.bazza_not_wins If c ≥ √2/2 then Bazza has no winning strategy: Alice survives forever by playing all zeros line 478 source
Source documentation
If c ≥ √2/2 then Bazza has no winning strategy: Alice survives forever by playing all zeros.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, HDiv.hDiv, Real.sqrt, OfNat.ofNat, Nat, Not, Exists, Imo2025P5.Strategy, Imo2025P5.Strategy.Winning
Proof uses: False, Imo2025P5.Wins, Imo2025P5.Strategy.play, Imo2025P5.respSeq, Imo2025P5.zeroStrategy, And, LT.lt, Ne, HMod.hMod, Imo2025P5.ValidAt, Eq.mp, Fin, congrArg, propext, Imo2025P5.wins_iff, Imo2025P5.play_respSeq, Even, Eq, Eq.mpr, ite and 9 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma bazza_not_wins {c : ℝ} (hc : Real.sqrt 2 / 2 ≤ c) :
    ¬ ∃ s : Strategy, s.Winning c 1 := by
…
```
Mentions: Imo2025P5.Strategy
lemma Imo2025P5.alice_wins If c > √2/2 then Alice wins: she plays zeros until index N, then spends her whole linear budget, which by then exceeds √(N + 2), so Bazza cannot answer line 493 source
Source documentation
If c > √2/2 then Alice wins: she plays zeros until index N, then spends her whole linear budget, which by then exceeds √(N + 2), so Bazza cannot answer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, HDiv.hDiv, Real.sqrt, OfNat.ofNat, Nat, Exists, Imo2025P5.Strategy, Imo2025P5.Strategy.Winning
Proof uses: lt_trans, div_pos, Real.sqrt_pos_of_pos, Mathlib.Meta.Positivity.pos_of_isNat, inferInstance, PartialOrder, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, HSub.hSub, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, AddMonoidWithOne, congrArg and 180 more
183 instances, coercions and auxiliary constants left out.

Tactic trace: 124 steps
Open to load the checked before-and-after goal states.
```
lemma alice_wins {c : ℝ} (hc : Real.sqrt 2 / 2 < c) : ∃ s : Strategy, s.Winning c 0 := by
…
```
Mentions: Imo2025P5.Strategy
problem Imo2025P5.imo2025_p5 line 601 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Prod, Set, Real, Prod.mk, Set.ofPred, Exists, Imo2025P5.Strategy, Imo2025P5.Strategy.Winning, OfNat.ofNat, Nat, Imo2025P5.answer
Proof uses: LT.lt, HDiv.hDiv, Real.sqrt, Set.ext, id, Iff, Membership.mem, Iff.intro, Decidable.byContradiction, Not, Imo2025P5.alice_not_wins, Iff.mp, LE.le, not_lt, Imo2025P5.alice_wins, Imo2025P5.bazza_not_wins, Imo2025P5.bazza_wins, Eq.mpr, congrArg, Eq.refl
17 instances, coercions and auxiliary constants left out.

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