Inekoalaty game: sharp threshold \(\lambda_c=1/\sqrt2\) with Lean-verified analytic lemmas (no sorry, no warnings)

Abstract

We classify the winner in the inekoalaty game as a function of the parameter (\lambda>0). The game has a sharp threshold [ \lambda_c=\frac{1}{\sqrt2}. ] If (\lambda>\lambda_c), Alice wins by a delayed large move; if (\lambda<\lambda_c), Bazza wins by saturating the square-budget each even move; and for (\lambda=\lambda_c) there exists infinite play (draw). We provide Lean4/mathlib proofs of the analytic inequalities and Archimedean steps used.

Game

Players choose (x_n\ge 0).

• Odd (n): Alice must have (S_n:=\sum_{i=1}^n x_i\le \lambda n).
• Even (n): Bazza must have (Q_n:=\sum_{i=1}^n x_i^2\le n).

If a player cannot move, they lose.

Theorem (classification)

Let (\lambda_c=1/\sqrt2=\sqrt2/2).

1. If (\lambda>\lambda_c), Alice has a winning strategy.
2. If (\lambda<\lambda_c), Bazza has a winning strategy.
3. If (\lambda=\lambda_c), neither player has a winning strategy (draw).

Strategies and proof

A. Bazza wins for (\lambda<\sqrt2/2)

Bazza’s strategy. On turn (2k), assuming the game reaches this turn, play [ x_{2k}:=\sqrt{2k-Q_{2k-1}}\ge 0. ] This is legal because reaching turn (2k) implies (Q_{2k-1}\le 2k). It enforces the invariant (Q_{2k}=2k).

From (Q_{2k}=2k) we get (x_{2k-1}^2+x_{2k}^2=2) with both terms nonnegative. Hence by the pair-sum inequality, (x_{2k-1}+x_{2k}\ge\sqrt2). Summing over (k) gives [ S_{2k}\ge k\sqrt2. ]

Since (\lambda<\sqrt2/2), choose (k) with (k\sqrt2>\lambda(2k+1)) (Archimedean argument). Then at Alice’s turn (2k+1), already (S_{2k}>\lambda(2k+1)), so Alice has no legal move and Bazza wins.

B. Alice wins for (\lambda>\sqrt2/2)

Alice’s strategy. Play (x_{2i-1}=0) for many odd turns. After Bazza moves at turn (2k), we have [ S_{2k}=\sum_{i=1}^k x_{2i},\qquad \sum_{i=1}^k x_{2i}^2\le Q_{2k}\le 2k. ] By Cauchy–Schwarz, [ S_{2k}\le k\sqrt2. ] So at turn (2k+1) Alice has slack (\lambda(2k+1)-S_{2k}\ge \lambda(2k+1)-k\sqrt2).

If (\lambda>\sqrt2/2) then (\lambda(2k+1)-k\sqrt2\to +\infty), so choose (k) with (\lambda(2k+1)-k\sqrt2>\sqrt2). On that turn Alice plays the maximum allowed [ x_{2k+1}:=\lambda(2k+1)-S_{2k}>\sqrt2. ] Then (Q_{2k+1}=Q_{2k}+x_{2k+1}^2>2k+2), so Bazza has no legal move at turn (2k+2). Hence Alice wins.

C. Boundary (\lambda=\sqrt2/2)

Infinite play exists, e.g. (x_{2k-1}=0) and (x_{2k}=\sqrt2) for all (k), which satisfies (Q_{2k}=2k) and (S_{2k}=k\sqrt2\le (\sqrt2/2)(2k+1)). Thus neither player can force a win at (\lambda=\lambda_c).

Lean4/mathlib formalization

Attached: Math/Inekoalaty.lean.

It contains Lean proofs (no sorry) of:

• add_ge_sqrt_two_of_sq_add_sq_eq_two: (a^2+b^2=2 \Rightarrow a+b\ge\sqrt2) for (a,b\ge0).
• add_sqrt_two_sub_sq_ge_sqrt_two: corollary (t+\sqrt{2-t^2}\ge\sqrt2) for (0\le t) and (t^2\le 2).
• sum_le_card_mul_sqrt_two: a finitary Cauchy–Schwarz bound via sq_sum_le_card_mul_sum_sq.
• exists_nat_mul_sqrt2_gt_linear: existence of (k) with (k\sqrt2>\lambda(2k+1)) for (\lambda<\sqrt2/2).
• exists_nat_linear_minus_mul_sqrt2_gt_sqrt2: quantitative lemma used for Alice’s final move when (\lambda>\sqrt2/2).

Compilation log

$ lake env lean Math/Inekoalaty.lean
# (no output; success)