A zero-sum selection game

Two players play on a real n × n matrix. The Enemy selects i entries of row i for each i. Then You choose one selected entry in every row, and You win if your entries sum to zero. Vsevolod Lev asked on MathOverflow (question 453809) for a description of the winning matrices.

The paper proves three results:

• Dimension (Theorem 1). The winning matrices form a finite union of rational linear subspaces of dimension exactly n(n+1)/2 − 1. More generally, for rows of length N_i with quotas k_i the dimension is Σ k_i − 1. The proof is a short rank argument: delete positions one at a time and watch the span of the surviving zero-sum transversals shrink.
• Order three (Theorem 2). A 3 × 3 matrix is winning exactly when every first-row entry has two usable second-row positions. With distinct entries in every row, the winning matrices are five explicit families.
• Complexity (Theorem 3). Recognising winning integer matrices is Π₂ᵖ-complete, even with two values per row. So no polynomial-time test exists unless the polynomial hierarchy collapses.

Preprint v1, 9 October 2026, not peer reviewed.

• Formally verified in Lean 4 (lean/, standard axioms only): the rank lemma and the dimension theorem for arbitrary row lengths and quotas; the order-three criterion; the collision lemma and the distinct-entry classification; the two-valued normal form behind the hardness proof.
• Not formalised:
  • the bookkeeping of the reduction (which rows are universal and which existential);
  • the twelve order-three families and the count of 1,107 components, which were computed and then rechecked independently;
  • the two remarks on further families.

The author used AI tools (Codex, OpenAI; Claude, Anthropic) in this work, as described in the paper’s acknowledgement, and is responsible for its content.