Single-step decreases in the three-row Chomp diagonal sequence: A uniform bound below one half

Let dn be the unique first-row length for which (dn, n, n) is a losing position in three-row Chomp, and let gn = max{0, dn − dn+1}. For every integer n ≥ 6, we prove gn ≤ 83n/168 and the signed bound dn − dn+1 ≤ 83n/168 − 125/84. More precisely, the signed upper bound is 83n/168 − 2 for even n and 83n/168 − 125/84 − 1/(168n) for odd n. The proof combines a strengthened source-row estimate with shared column-capacity counting; occurrences before their diagonal indices are included, allowing inversion counts to cancel. The coefficient 83/168 = 1/2 − 1/168 gives a fixed improvement below one half. These results do not establish sublinear or uniformly bounded decreases, or the conjecture dn+1 ≥ dn − 1. This first public release (version 1.0) contains manuscript revision r3, its editable LaTeX source, and a reproducible Lean 4.19.0 formal-verification supplement with pinned dependencies and validation records. The formalization proves the bounds from the actual positive-mex/copy recurrence without additional structural hypotheses or unproved custom axioms; the equivalence between that recurrence and the game’s P-positions remains an input from the cited literature. OpenAI Codex and language-model assistance were used extensively in mathematical exploration, argument development, manuscript preparation, and formalization work. AI-assisted review is not independent human peer review. Responsibility for the mathematical claims and manuscript rests with the author. All materials are released under the Creative Commons Attribution 4.0 International (CC BY 4.0) license. The manuscript, proof source, reproduction instructions, and versioned release are also available in the GitHub repository.