# A game with a nontrivial move set

KL-FCS-051 · Game theory · version 1.0.0

## Problem

Classify each heap size and certify a winning strategy under optimal normal play.

## Context

A winning move is defined against optimal opponent responses, rather than against one friendly execution.

## Definitions

- **Normal play**: The player with no legal move loses.
- **Winning position**: A state with at least one move to a losing position for the opponent.
- **Strategy**: A legal choice for every winning state in the declared game domain.

## Checked result

Winning heap sizes: [2, 3, 4, 5, 6, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20].

Every winning state has a legal move to a losing state. A losing state has no such move, so the opponent controls the next winning position.

## Checker reasoning

1. Set the empty heap to losing.
2. Process heap sizes in increasing order.
3. Mark a heap winning if an allowed subtraction reaches a losing heap.
4. Validate every submitted winning move and every losing-state marker.

## Dataset construction

{
  "family": "games",
  "task": "Classify each heap size and certify a winning strategy under optimal normal play.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete backward classification · 21 states",
  "acceptance": [
    "Set the empty heap to losing.",
    "Process heap sizes in increasing order.",
    "Mark a heap winning if an allowed subtraction reaches a losing heap.",
    "Validate every submitted winning move and every losing-state marker."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "moves": [
      2,
      3,
      5
    ],
    "max_heap": 20,
    "terminal_rule": "A player unable to move loses; no draws; perfect information."
  },
  "claim": {
    "winning_positions": [
      2,
      3,
      4,
      5,
      6,
      9,
      10,
      11,
      12,
      13,
      16,
      17,
      18,
      19,
      20
    ]
  },
  "witness": {
    "strategy": [
      null,
      null,
      2,
      2,
      3,
      5,
      5,
      null,
      null,
      2,
      2,
      3,
      5,
      5,
      null,
      null,
      2,
      2,
      3,
      5,
      5
    ]
  }
}
```

## Complexity

N heap sizes with m allowed moves require O(Nm) dynamic-programming checks.

## Limits

These are finite impartial subtraction games, not equilibrium analyses of simultaneous or imperfect-information games.

## Common error and further work

A single successful play does not establish a strategy against all opponent choices.

Add alternating-player reachability graphs and strategy certificates.

## Verification

Complete backward classification · 21 states. 21 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://isa-afp.org/entries/Parity_Game.html)