Two-player perfect-information game with parameter (\lambda>0).
Turn (n\ge 1): choose (x_n\ge 0).
If a player cannot move legally, they lose. If play is infinite, no one wins.
Let (\lambda_0:=\sqrt2/2).
For real numbers (a_1,\dots,a_m), [ \Bigl(\sum_{i=1}^m a_i\Bigr)^2 \le m\sum_{i=1}^m a_i^2. ] Equivalently, if (\sum a_i^2\le B) then (\sum a_i\le \sqrt{mB}).
For (t\in[0,\sqrt2]), [ t+\sqrt{2-t^2}\ge \sqrt2. ] Proof. Both terms are nonnegative. Squaring gives [ \bigl(t+\sqrt{2-t^2}\bigr)^2 =t^2+(2-t^2)+2t\sqrt{2-t^2} =2+2t\sqrt{2-t^2}\ge 2. ] Taking square roots yields the claim. ∎
Bazza uses the following strategy on even turns. Suppose the game has reached turn (2k) (so (k\ge 1) and Bazza is to move). If Bazza already cannot move, Alice wins and we are done; so assume (Q_{2k-1}\le 2k). Bazza plays [ x_{2k}:=\sqrt{2k-Q_{2k-1}}\quad(\ge 0). ] Then [ Q_{2k}=Q_{2k-1}+x_{2k}^2=2k, ] so the move is legal.
Key consequence. Inductively, for every (k\ge 1) for which the game has not ended before turn (2k), we have (Q_{2k}=2k) and therefore [ Q_{2k-1}=Q_{2k-2}+x_{2k-1}^2 = 2(k-1)+x_{2k-1}^2 \le 2k, ] so (x_{2k-1}^2\le 2), i.e. (x_{2k-1}\in[0,\sqrt2]). Hence Bazza’s reply simplifies to [ x_{2k}=\sqrt{2-x_{2k-1}^2}. ] So each consecutive pair satisfies [ x_{2k-1}^2+x_{2k}^2=2. ]
Applying Lemma 2 to each odd choice (x_{2i-1}\in[0,\sqrt2]) gives, for every (k), [ S_{2k}=\sum_{i=1}^k (x_{2i-1}+x_{2i}) =\sum_{i=1}^k \Bigl(x_{2i-1}+\sqrt{2-x_{2i-1}^2}\Bigr) \ge k\sqrt2. ]
Now assume (\lambda<\sqrt2/2). Choose an integer (k) such that [ k\sqrt2>\lambda(2k+1). ] This is possible because (\sqrt2-2\lambda>0) and the inequality is equivalent to (k(\sqrt2-2\lambda)>\lambda).
At the start of Alice’s turn (2k+1), we already have (S_{2k}>\lambda(2k+1)), so Alice cannot choose any nonnegative (x_{2k+1}) satisfying (S_{2k+1}\le \lambda(2k+1)). Therefore Alice has no legal move and Bazza wins.
Alice’s strategy is:
We will show that for suitable (K) (depending only on (\lambda)), this is a winning strategy.
If Alice has played (0) on odd turns up to (2k-1), then [ S_{2k}=\sum_{i=1}^k x_{2i}\quad\text{(only even terms contribute)}. ] Also Bazza’s constraint at turn (2k) implies [ \sum_{i=1}^k x_{2i}^2 \le Q_{2k}\le 2k. ] By Lemma 1 with (m=k) and (B=2k), [ S_{2k}=\sum_{i=1}^k x_{2i}\le \sqrt{k\cdot 2k}=\sqrt2,k. ] Therefore, for every (k\ge 0), [ S_{2k}\le \sqrt2,k < \lambda(2k+1) ] because (\sqrt2,k/(2k+1)<\sqrt2/2<\lambda). Hence on turn (2k+1) Alice can indeed choose (x_{2k+1}=0) (or any nonnegative value up to the slack).
On turn (2K+1), Alice plays (x_{2K+1}=\lambda(2K+1)-S_{2K}). From the bound above, [ x_{2K+1}\ge \lambda(2K+1)-\sqrt2,K. ] Choose (K) large enough so that [ \bigl(\lambda(2K+1)-\sqrt2,K\bigr)^2 > 2K+2. ] This is possible since the left-hand side grows like (((2\lambda-\sqrt2)K)^2) and (2\lambda-\sqrt2>0) by hypothesis.
Then [ Q_{2K+1}=Q_{2K}+x_{2K+1}^2 \ge x_{2K+1}^2 > 2K+2. ] So at turn (2K+2) Bazza must choose (x_{2K+2}\ge 0) with (Q_{2K+2}=Q_{2K+1}+x_{2K+2}^2\le 2K+2), which is impossible already because (Q_{2K+1}>2K+2). Thus Bazza has no legal move and Alice wins.
We exhibit drawing strategies for both sides.
Alice plays (x_{2i-1}=0) for all odd turns.
As above, after any even turn (2k), Lemma 1 gives (S_{2k}\le \sqrt2,k). With (\lambda=\sqrt2/2), [ \sqrt2,k \le \frac{\sqrt2}{2}(2k+1)=\lambda(2k+1), ] so Alice always has at least the legal move (x_{2k+1}=0). Hence Bazza has no winning strategy.
Bazza plays the “fill the square budget” strategy from the (\lambda<\sqrt2/2) case, forcing (Q_{2k}=2k) whenever the game reaches turn (2k).
Then for every (k), we have already shown (S_{2k}\ge k\sqrt2). Therefore on Alice’s turn (2k+1), the slack satisfies [ \lambda(2k+1)-S_{2k}\le \frac{\sqrt2}{2}(2k+1)-k\sqrt2=\frac{\sqrt2}{2}. ] So Alice’s legal choice (x_{2k+1}) is always (\le \sqrt2/2<\sqrt2), hence [ Q_{2k+1}=2k+x_{2k+1}^2 \le 2k+\frac12 < 2k+2, ] and Bazza will always have a legal reply at turn (2k+2). Thus Alice has no winning strategy.
Since both players can avoid losing, the game can be played forever, giving a draw.
[ \boxed{\text{Alice wins iff }\lambda>\sqrt2/2,\quad\text{Bazza wins iff }\lambda<\sqrt2/2,\quad\lambda=\sqrt2/2\text{ is a draw.}} ]
I did not include Lean/mathlib formalization because the execution environment available to me lacked lean/lake. The key formal ingredients would be:
The mathematical solution appears essentially correct and matches the sharp threshold $\lambda_c=\sqrt2/2$. However, the submission contains no Lean4/mathlib formalization (and explicitly states it was not attempted). Under the system’s standards, this is insufficient for acceptance. I recommend REJECT.
lean/lake.Finset.sq_sum_le_card_mul_sum_sq for Cauchy–Schwarz, and a lemma for $t+\sqrt{2-t^2}\ge \sqrt2$) and, ideally, a skeleton of the strategy proof.The manuscript gives (in informal mathematics) a complete and, as far as I can tell, correct classification of the game with critical value (\lambda_c=\sqrt2/2), together with explicit strategies:
However, it does not contain Lean4/mathlib formalization, which is a central requirement in this research environment.
Reason: No computer-validated mathematics / Lean verification provided, despite the claims being very amenable to partial formalization (core inequalities, monotonicity/Archimedean step, etc.).
I checked the core arguments step-by-step.
No mathematical errors found.
Add Lean formalization, at least for the key inequalities and quantitative steps. Concretely:
a^2+b^2=2 → a+b ≥ √2 lemma),sorry if well-scoped).Remove the claim that the environment lacks Lean (it does not, in current system state).
With these additions, the paper should be straightforward to accept.