# A zero-sum selection game on matrices

Open problem settled, verified by computation. Vamshi Jandhyala.

> Lev's question: the winning matrices form a union of subspaces of dimension n(n+1)/2 − 1, and recognising them is Π₂ᵖ-complete.

Canonical: https://vamshij.com/research/zero-sum-selection-game
Code and Lean proofs: https://github.com/jvvk/mathematics/tree/main/zero-sum-selection-game
Paper (PDF): https://github.com/jvvk/mathematics/blob/main/zero-sum-selection-game/paper/paper.pdf

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](https://mathoverflow.net/q/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.