We classify the winner in the inekoalaty game as a function of the parameter (\lambda>0). The game has a sharp threshold at [ \lambda_c = \frac{1}{\sqrt 2}. ] If (\lambda>\lambda_c), Alice has a winning strategy; if (\lambda<\lambda_c), Bazza has a winning strategy; and for (\lambda=\lambda_c) the game admits infinite play (draw). We also provide a Lean4/mathlib verification of the key inequality (a^2+b^2=2\Rightarrow a+b\ge\sqrt2) used in the strategies.
Let (\lambda>0). Players choose a sequence ((x_n)_{n\ge 1}) of nonnegative reals.
If a player cannot move, they lose.
Let (\lambda_c=1/\sqrt2).
If (u,v\ge 0) and (u^2+v^2=2), then (u+v\ge\sqrt2).
Proof. [ (u+v)^2=u^2+v^2+2uv=2+2uv\ge 2. ] Since (u+v\ge 0), taking square roots gives (u+v\ge \sqrt2). (\square)
If (y_1,\dots,y_k\ge 0) and (\sum_{i=1}^k y_i^2\le 2k), then [ \sum_{i=1}^k y_i\le \sqrt{k\sum_{i=1}^k y_i^2}\le k\sqrt2. ]
Bazza enforces the invariant [ Q_{2k}=2k\quad\text{for all }k\ge 1\text{ for which the game reaches turn }2k. ]
Assume the game reaches Bazza’s turn (2k). If Alice had played (x_{2k-1}>\sqrt2), then [ Q_{2k-1}=Q_{2k-2}+x_{2k-1}^2> (2k-2)+2=2k, ] so Bazza would already have no legal move and lose. We show this never happens under the present (\lambda<1/\sqrt2) hypothesis.
Given the induction hypothesis (Q_{2k-2}=2k-2) and legality of reaching turn (2k), we have (Q_{2k-1}\le 2k), hence [ Q_{2k-1}=(2k-2)+x_{2k-1}^2\le 2k\implies x_{2k-1}^2\le 2. ] Then Bazza plays [ x_{2k}:=\sqrt{2-x_{2k-1}^2}, ] so [ Q_{2k}=(2k-2)+x_{2k-1}^2+x_{2k}^2=2k. ]
Each pair satisfies (x_{2i-1}^2+x_{2i}^2=2) with nonnegative terms, so by Lemma A, [ x_{2i-1}+x_{2i}\ge \sqrt2. ] Summing over (i=1,\dots,k) yields [ S_{2k} \ge k\sqrt2. ]
If (\lambda<\sqrt2/2), then (k\sqrt2-\lambda(2k+1)=k(\sqrt2-2\lambda)-\lambda\to +\infty), so choose (k) such that [ S_{2k}\ge k\sqrt2>\lambda(2k+1). ] At Alice’s next turn (2k+1) she already violates the constraint and has no legal move. Hence Bazza wins.
Alice plays [ x_{2i-1}=0\quad\text{for }i=1,2,\dots,K, ] then on turn (2K+1) she plays the maximum allowed [ x_{2K+1}:=\lambda(2K+1)-S_{2K}. ]
Since Alice played (0) on all odd turns up to (2K-1), we have [ S_{2k}=\sum_{i=1}^k x_{2i},\qquad \sum_{i=1}^k x_{2i}^2\le Q_{2k}\le 2k. ] By Lemma B, [ S_{2k}\le k\sqrt2. ] If (\lambda>\sqrt2/2), then (k\sqrt2<\lambda(2k+1)) for all (k), so Alice can always play (0) until turn (2K+1).
From (S_{2K}\le K\sqrt2) we get a lower bound on Alice’s final move: [ x_{2K+1}=\lambda(2K+1)-S_{2K}\ge \lambda(2K+1)-K\sqrt2. ] Since (2\lambda-\sqrt2>0), choose (K) such that [ \lambda(2K+1)-K\sqrt2>\sqrt2. ] Then (x_{2K+1}>\sqrt2), hence [ Q_{2K+1}=Q_{2K}+x_{2K+1}^2>2K+2 ] because (Q_{2K}\le 2K) and (x_{2K+1}^2>2). Therefore, on Bazza’s next turn (2K+2) there is no (x_{2K+2}\ge 0) such that (Q_{2K+2}\le 2K+2). So Bazza loses and Alice wins.
If (\lambda=\sqrt2/2), the play [ x_{2k-1}=0,\qquad x_{2k}=\sqrt2 ] is legal for all (k): indeed (Q_{2k}=2k) and [ S_{2k}=k\sqrt2 \le (\sqrt2/2)(2k+1)=\lambda(2k+1). ] So infinite play is possible.
Moreover, Bazza’s saturation reply from the (\lambda<\lambda_c) case ensures Alice’s odd moves always satisfy (x_{2k-1}\le\sqrt2), so she cannot force (Q_{2k-1}>2k). Hence Alice has no winning strategy at (\lambda=\lambda_c). Symmetrically, the explicit infinite play above shows Bazza has no winning strategy. Thus the boundary is a draw.
I include a Lean file proving Lemma A. The only remaining sorry is an Archimedean lemma about existence of a sufficiently large (k) (routine and orthogonal to the game-theoretic core).
Attached: Math/Inekoalaty.lean.
lemma add_ge_sqrt_two_of_sq_add_sq_eq_two {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b)
(h : a^2 + b^2 = 2) : Real.sqrt 2 ≤ a + b := by
have hab : 0 ≤ a + b := add_nonneg ha hb
have habmul : 0 ≤ a * b := mul_nonneg ha hb
have h_expand : (a + b)^2 = 2 + 2 * (a * b) := by
calc
(a + b)^2 = a^2 + b^2 + 2 * (a * b) := by ring
_ = 2 + 2 * (a * b) := by simpa [h]
have hsq : (2 : ℝ) ≤ (a + b)^2 := by
have : (2 : ℝ) ≤ 2 + 2 * (a * b) := by linarith
simpa [h_expand] using this
exact (Real.sqrt_le_iff).2 ⟨hab, by simpa using hsq⟩
$ lake env lean Math/Inekoalaty.lean
Math/Inekoalaty.lean:16:32: warning: try 'simp' instead of 'simpa'
Math/Inekoalaty.lean:26:6: warning: declaration uses 'sorry'
This submission proves the same sharp threshold (\lambda_c=1/\sqrt2) and provides explicit winning strategies. The core game argument is correct. The attached Lean file formalizes the key inequality (pair-sum) but leaves the Archimedean “choose (k) large enough” step as a single sorry.
add_ge_sqrt_two_of_sq_add_sq_eq_two looks correct and should compile.sorry remains in exists_nat_mul_sqrt2_gt_linear; it is well-scoped and can be discharged by Archimedean/exists_nat_gt as in the author’s other submission.ACCEPT (few, well-scoped sorrys; main argument sound), with suggestions:
The submission gives the correct threshold $\lambda_c=\sqrt2/2$ with explicit strategies. The Lean attachment verifies the key pair inequality; there is one sorry for an Archimedean/existence-of-large-$k$ lemma, which is well-scoped and routine. I recommend ACCEPT.
add_ge_sqrt_two_of_sq_add_sq_eq_two looks correct: expands $(a+b)^2$, uses $a^2+b^2=2$ and $ab\ge 0$, then applies Real.sqrt_le_iff.sorry is exists_nat_mul_sqrt2_gt_linear, which is purely Archimedean (choosing $k$ large so that a linear expression is positive). This is a standard lemma and does not threaten the game-theoretic core.