Formalize the perfect-play value of chess

### What is the conjecture

Under perfect play from the standard initial position, chess has the game-theoretic value of a draw. Equivalently, White has a strategy that avoids losing and Black has a strategy that avoids losing.

The earliest published statement I can find appears in the anonymously authored *Traité théorique et pratique du jeu des échecs* (1775), pp. 162–163. Later bibliographies attribute the work to Léger, Bernard, Carlier, and Verdoni, without identifying the author of this passage.

References:

* [Société d'Amateurs, *Traité théorique et pratique du jeu des échecs* (1775)](https://archive.org/details/traitthoriqueet00damgoog)
* [FIDE Laws of Chess](https://rcc.fide.com/fide-laws-of-chess_fulltexthtml/)
* [Wikipedia, *Solving chess*](https://en.wikipedia.org/wiki/Solving_chess)
* [Wikipedia, *First-move advantage in chess*](https://en.wikipedia.org/wiki/First-move_advantage_in_chess)

I propose to formalize current FIDE over-the-board chess. The model would include legal moves, checkmate, stalemate, dead positions, claim-based threefold repetition and 50-move draws, and automatic fivefold repetition and 75-move draws. It would exclude clocks, resignation, and draws by agreement because those are not properties of the abstract game tree.

### Prerequisites needed
Mathlib and this repository do not currently contain a chess model or a general perfect-information game framework suitable for this statement. The proposed file therefore needs problem-specific definitions for:

* the board, pieces, castling rights, en passant state, and move legality;
* histories and the FIDE draw rules;
* terminal outcomes, pure strategies, and finite plays from the initial position.

The basic finite types are already supported by [`Fin`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fin/Basic.html) and [`Fintype`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Basic.html). No general-purpose addition to `FormalConjecturesForMathlib` appears necessary.

I have a self-contained prototype of approximately 636 lines importing only `FormalConjecturesUtil`. Its main statement is `WhiteCanAvoidLoss ∧ BlackCanAvoidLoss`, and `lake --wfail build FormalConjectures.Wikipedia.Chess` succeeds.

Before opening a PR, I welcome guidance on the following:

1. Is this conjecture appropriate for the repository?
2. Is a self-contained specification of this size acceptable in a problem file?
3. Should the file live under `Books`, based on the 1775 source, or under `Wikipedia`, based on the
modern formulation?
4. Should the strategy and game-result definitions remain local, or should any generic part move
to `FormalConjecturesForMathlib`?

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-68 (Computer science)
* ams-91 (Game theory, economics, social and behavioral sciences)

### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

The issue identifies a proposed FormalConjectures.Wikipedia.Chess file and a roughly 636-line prototype, with `lake --wfail build FormalConjectures.Wikipedia.Chess` as the current check. First review the proposed board, history, draw-rule, strategy, and finite-play definitions, then resolve the repository-placement and generic-framework questions. Done means an accepted self-contained model builds and states `WhiteCanAvoidLoss ∧ BlackCanAvoidLoss`.

Written by the indexing model from the issue text.