pith. sign in

arxiv: 2604.07907 · v1 · submitted 2026-04-09 · 💻 cs.AI · cs.LO

Capture-Quiet Decomposition: A Verification Theorem for Chess Endgame Tablebases

Alexander Pavlov This is my paper

Pith reviewed 2026-05-10 16:49 UTC · model grok-4.3

classification 💻 cs.AI cs.LO
keywords chess endgamestablebase verificationWDL labelingretrograde analysisCapture-Quiet Decompositionchess AIgame verification
0
0 comments X

The pith

A WDL labeling for a chess endgame is correct if and only if terminals are labeled right, captures match verified smaller-piece tables, and quiet positions meet internal retrograde consistency.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Capture-Quiet Decomposition as a structural theorem that classifies every legal chess position as terminal, capture, or quiet. It proves that a Win-Draw-Loss labeling is correct precisely when terminals receive their true values, capture positions inherit labels from already-verified endgames with fewer pieces, and quiet positions satisfy retrograde rules inside the same endgame. This matters because self-consistent labelings alone can accept wrong answers, such as the all-draw assignment, while the capture links to external smaller models remove those trivial fixpoints. The theorem was exhaustively validated on every three- through six-piece endgame, producing the same results as full retrograde analysis in all cases.

Core claim

Every legal position belongs to exactly one of three exhaustive categories: terminal positions (no legal moves), capture positions (a move reduces total piece count), or quiet positions (all moves preserve piece count). A WDL labeling is correct if and only if terminals are labeled with their true outcomes, capture positions are labeled consistently with the verified WDL tables of the resulting smaller-piece endgames, and quiet positions satisfy the standard retrograde consistency conditions within the current endgame. This decomposition anchors the labeling to independently verified sub-models via captures, eliminating circular self-consistent but incorrect labelings.

What carries the argument

The Capture-Quiet Decomposition, which partitions every position into terminal, capture, or quiet and requires captures to be consistent with verified smaller-piece tables.

If this is right

  • Verification of a new endgame requires only prior confirmation of all its possible capture targets plus internal checks on quiet positions.
  • The all-draw labeling is rejected wherever any capture leads to a forced win or loss in a smaller table.
  • The decomposed verifier matches the violation counts of full retrograde analysis on all 517 tested endgames up to six pieces.
  • Once smaller tables are certified, each larger endgame becomes independently verifiable without re-examining the entire combined graph.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The method could support selective re-verification when only one endgame is updated, without touching unrelated tables.
  • Similar capture-based reductions might apply to verification in other games or planning domains that contain complexity-reducing moves.
  • The approach may make verification of seven-piece and larger tables feasible by keeping the internal check size manageable.

Load-bearing premise

Every capture move reduces to a smaller-piece-count endgame whose labeling has already been independently verified.

What would settle it

A single endgame in which the three conditions hold yet a full retrograde analysis on the complete position graph produces a different WDL label for any position.

read the original abstract

We present the Capture-Quiet Decomposition (CQD), a structural theorem for verifying Win-Draw-Loss (WDL) labelings of chess endgame tablebases. The theorem decomposes every legal position into exactly one of three categories -- terminal, capture, or quiet -- and shows that a WDL labeling is correct if and only if: (1) terminal positions are labeled correctly, (2) capture positions are consistent with verified sub-models of smaller piece count, and (3) quiet positions satisfy retrograde consistency within the same endgame. The key insight is that capture positions anchor the labeling to externally verified sub-models, breaking the circularity that allows trivial fixpoints (such as the all-draw labeling) to satisfy self-consistency alone. We validate CQD exhaustively on all 35 three- and four-piece endgames (42 million positions), all 110 five-piece endgames, and all 372 six-piece endgames -- 517 endgames in total -- with the decomposed verifier producing identical violation counts to a full retrograde baseline in every case.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript presents the Capture-Quiet Decomposition (CQD) as a structural theorem for verifying Win-Draw-Loss (WDL) labelings of chess endgame tablebases. It decomposes every legal position exhaustively into one of three categories (terminal, capture, or quiet) and claims that a labeling is correct if and only if (1) terminal positions are labeled correctly, (2) capture positions are consistent with verified sub-models of smaller piece count, and (3) quiet positions satisfy retrograde consistency within the same endgame. The paper reports that this decomposition breaks circularity in self-consistency checks and validates the claim by showing identical violation counts between the CQD verifier and a full retrograde baseline across all 517 endgames up to six pieces (including 42 million positions for three- and four-piece cases).

Significance. If the theorem holds, the result supplies a principled, non-circular verification method for chess endgame tablebases by anchoring capture positions to independently verified smaller-piece-count models. This is a meaningful contribution to automated verification in combinatorial game theory and AI, as it directly addresses the fixpoint problem that allows trivial labelings (e.g., all-draw) to satisfy pure self-consistency. The exhaustive empirical confirmation—matching violation counts on every three-, four-, five-, and six-piece endgame—provides strong practical evidence of correctness and utility, especially given the scale (517 endgames total).

minor comments (2)
  1. The abstract states that the decomposition is exhaustive for every legal position, but a brief explicit proof or reference to the relevant section establishing that every position falls into exactly one of terminal/capture/quiet (with no overlap or omission) would strengthen the presentation.
  2. The validation reports identical violation counts on 517 endgames but does not specify the exact definition of a 'violation' or the precise metric used for comparison; adding this in the experimental section would aid reproducibility.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their thorough and positive review of our paper on Capture-Quiet Decomposition. We appreciate the recognition of the theorem's significance in providing a non-circular verification method for chess endgame tablebases. Since the major comments section is empty and the recommendation is minor revision, we provide a brief response to the summary below.

read point-by-point responses

  1. Referee: The manuscript presents the Capture-Quiet Decomposition (CQD) as a structural theorem for verifying Win-Draw-Loss (WDL) labelings of chess endgame tablebases. It decomposes every legal position exhaustively into one of three categories (terminal, capture, or quiet) and claims that a labeling is correct if and only if (1) terminal positions are labeled correctly, (2) capture positions are consistent with verified sub-models of smaller piece count, and (3) quiet positions satisfy retrograde consistency within the same endgame. The paper reports that this decomposition breaks circularity in self-consistency checks and validates the claim by showing identical violation counts between the CQD verifier and a full retrograde baseline across all 517 endgames up to six pieces (including 42 million positions for three- and four-piece cases).

    Authors: We thank the referee for this accurate summary of the manuscript. The description correctly reflects the core of the CQD theorem and the scope of the empirical validation performed. revision: no

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The Capture-Quiet Decomposition theorem defines WDL correctness via an exhaustive partition into terminals (labeled by direct rules), captures (anchored to independently verified smaller-piece-count models), and quiet positions (checked for intra-endgame retrograde consistency). This structure is self-contained: the inductive step relies on external smaller endgames rather than self-reference, terminals are fixed by chess rules without circularity, and sufficiency follows from the fact that external anchors break potential fixpoint cycles before propagation. Exhaustive empirical matching of violation counts to a full retrograde baseline across all 517 endgames up to six pieces supplies independent confirmation that the conditions are equivalent to correctness without any reduction of outputs to fitted inputs or self-citations. No load-bearing step collapses to a definition or prior self-result by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on the domain assumption that positions decompose exhaustively into the three categories and that captures always reduce piece count to independently verifiable subgames.

axioms (2)
  • domain assumption Every legal chess position belongs to exactly one of terminal, capture, or quiet.
    Stated as the starting point of the decomposition in the abstract.
  • domain assumption Capture moves always lead to endgames with strictly fewer pieces.
    Required for the anchoring to smaller verified sub-models.

pith-pipeline@v0.9.0 · 5480 in / 1322 out tokens · 53008 ms · 2026-05-10T16:49:48.060477+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

7 extracted references · 7 canonical work pages

  1. [1]

    R. de Man. Syzygy endgame tablebases.https://github.com/syzygy1/tb, 2013–2018

    work page 2013

  2. [2]

    J. Hurd. Formal verification of chess endgame databases. InProc. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), volume 3702 of LNCS, pages 84–98. Springer, 2005. 8

    work page 2005

  3. [3]

    E. Marzion. Formally verified endgame tablebase generator in Coq.https://emarzion. github.io/TB-Generator/, 2023

    work page 2023

  4. [4]

    Clarke, O

    E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. InProc. CAV, volume 1855 of LNCS, pages 154–169. Springer, 2000

    work page 2000

  5. [5]

    B. Knaster. Un théorème sur les fonctions d’ensembles.Annales de la Société Polonaise de Mathématique, 6:133–134, 1928

    work page 1928

  6. [6]

    A. Tarski. A lattice-theoretical fixpoint theorem and its applications.Pacific Journal of Math- ematics, 5(2):285–309, 1955

    work page 1955

  7. [7]

    Stone, N

    I. Stone, N. R. Sturtevant, and J. Schaeffer. Set-based retrograde analysis: Precomputing the solution to 24-card bridge double dummy deals. InProc. International Joint Conference on Artificial Intelligence (IJCAI), 2025. Also available as arXiv:2411.09089. 9

    work page arXiv 2025