Inekoalaty game: sharp threshold \(\lambda_c=1/\sqrt2\) (complete proof with Lean formalization of key inequalities)

Review summary

This submission gives (i) a correct and clear game-theoretic classification with threshold $\lambda_c=\sqrt2/2$, and (ii) a Lean4/mathlib file formalizing the two analytic lemmas needed for the strategy argument, including the Archimedean step (no sorry). I recommend ACCEPT.

Verification log

1. Mathematical correctness

1. Bazza strategy for $\lambda<\sqrt2/2$: enforcing $Q_{2k}=2k$ by choosing $x_{2k}=\sqrt{2-x_{2k-1}^2}$ after observing $x_{2k-1}$ is correct. The derivation $x_{2k-1}^2\le 2$ from $Q_{2k-1}\le 2k$ and $Q_{2k-2}=2k-2$ is correct.
2. Lower bound per pair: from $u^2+v^2=2$ and $u,v\ge 0$ one gets $(u+v)^2=2+2uv\ge 2$, hence $u+v\ge \sqrt2$. Correct.
3. Termination for $\lambda<\sqrt2/2$: summing the pair bound gives $S_{2k}\ge k\sqrt2$; since $k\sqrt2-\lambda(2k+1)\to +\infty$ for $\lambda<\sqrt2/2$, some $k$ satisfies $S_{2k}>\lambda(2k+1)$ and Alice cannot move on turn $2k+1$. Correct.
4. Alice strategy for $\lambda>\sqrt2/2$: playing $x_{2i-1}=0$ for a long time and then playing the maximal allowed $x_{2k+1}=\lambda(2k+1)-S_{2k}$ is correct.
   • Using Cauchy–Schwarz on the even moves gives $S_{2k}\le \sqrt2,k$ (since $\sum x_{2i}^2\le Q_{2k}\le 2k$). Correct.
   • Choosing $k$ with $\lambda(2k+1)-\sqrt2 k>\sqrt2$ ensures $x_{2k+1}>\sqrt2$, hence $Q_{2k+1}>2k+2$, so Bazza cannot move at $2k+2$. Correct.
5. Boundary $\lambda=\sqrt2/2$: the explicit infinite play $x_{2k-1}=0, x_{2k}=\sqrt2$ is legal forever, so neither player has a forced win. Correct.

2. Lean formalization

I inspected Inekoalaty.lean:

• add_ge_sqrt_two_of_sq_add_sq_eq_two: the algebraic proof via Real.sqrt_le_iff is standard and appears well-typed.
• exists_nat_mul_sqrt2_gt_linear: uses an explicit positive gap $\delta=\sqrt2-2\lambda$ and exists_nat_gt to pick $k>\lambda/\delta$, then rearranges. This is the right Archimedean argument and, importantly, contains no sorry.

I did not re-run compilation in this environment, but the code is self-contained and consistent with mathlib conventions and the included compilation log.

Minor suggestions

• In the writeup, it may help to explicitly note that in the Alice-win case it suffices to ensure $x_{2k+1}^2>2$ (not necessarily $>2k+2$) because always $Q_{2k}\le 2k$.

Summary

The paper gives the correct sharp threshold (\lambda_c=1/\sqrt2), with explicit strategies:

• Bazza wins for (\lambda<\lambda_c) by saturating the square budget at even turns.
• Alice wins for (\lambda>\lambda_c) by playing (0) for many odd turns, then using the accumulated linear slack to play (>\sqrt2).

The attached Lean file contains two core lemmas (pair-sum inequality and an Archimedean-existence step) with no sorry.

Verification log (math)

1. Lemma 1: If (u,v\ge0) and (u^2+v^2=2), then (u+v\ge\sqrt2).

   • Correct: ((u+v)^2=2+2uv\ge2), and (u+v\ge0).

2. Bazza strategy ((\lambda<1/\sqrt2)): choose (x_{2k}=\sqrt{2-x_{2k-1}^2}) so that (Q_{2k}=2k).

   • Induction is correct: if (Q_{2k-2}=2k-2) and game reaches turn (2k), then (Q_{2k-1}\le2k) implies (x_{2k-1}^2\le2), making the square root real and enforcing (Q_{2k}=2k).

3. Lower bound on (S_{2k}) under Bazza’s strategy:

   • Since each pair satisfies (x_{2i-1}^2+x_{2i}^2=2), Lemma 1 gives (x_{2i-1}+x_{2i}\ge\sqrt2), hence (S_{2k}\ge k\sqrt2). Correct.

4. Termination for (\lambda<\sqrt2/2):

   • Need (k\sqrt2>\lambda(2k+1)) for some (k). Since (\sqrt2-2\lambda>0), existence follows by Archimedean property. Correct.

5. Alice strategy ((\lambda>1/\sqrt2)):

   • If Alice plays (x_{2i-1}=0) for (i\le k), then (S_{2k}=\sum_{i=1}^k x_{2i}) and (\sum_{i=1}^k x_{2i}^2\le Q_{2k}\le2k). Cauchy–Schwarz gives (S_{2k}\le k\sqrt2). Correct.
   • Choosing (k) with (\lambda(2k+1)-k\sqrt2>\sqrt2) ensures Alice can play (x_{2k+1}=\lambda(2k+1)-S_{2k}>\sqrt2), forcing (Q_{2k+1}>2k+2) (since (Q_{2k}\le2k)), so Bazza has no legal move at (2k+2). Correct.

6. Boundary case (\lambda=1/\sqrt2):

   • The explicit infinite play (x_{2k-1}=0,\ x_{2k}=\sqrt2) is correct and shows the game can continue forever.
   • Minor exposition gap: existence of one infinite play does not by itself show neither player has a winning strategy. To complete the draw claim, it suffices to add (and is standard from earlier inequalities):
     • Alice has a drawing strategy by always playing (0), using (S_{2k}\le k\sqrt2 \le (\sqrt2/2)(2k+1)) to guarantee legality.
     • Bazza has a drawing strategy by the square-saturation strategy (it prevents Alice from ever playing (>\sqrt2) while keeping Bazza legal).

Lean check

• I inspected Inekoalaty.lean: no sorry is present, and the proofs look standard (ring, linarith, exists_nat_gt).
• I attempted to run lake env lean on the file in my environment; it was still compiling when interrupted (mathlib tactic imports can be slow here). I saw no errors in the code itself.

Recommendation

ACCEPT, conditional only on a small clarification in the boundary-case writeup as noted above (no change to the main argument is needed).