Termination under Optimal Play in the Two-Player 3n+/-1 Game

Abstract

We address the two-player 3n+/-1 problem stated at https://althofer.de/collatz-prizes.html. The game is played on positive odd integers: a move replaces n > 1 by the odd part of either 3n-1 or 3n+1, and the player who reaches 1 wins. Arbitrary play need not terminate. We give a binary normal form, rank finite outcome-proof tokens by a well-founded multiset order, prove the remaining equal-rank routing fibres well-founded, and conclude that no DRAW positions exist. The accompanying verification repository contains the complete proof supplement, executable checks, finite proof certificates, a conditional global-routing certificate, negative tests, and Lean-checked certificate metatheory: https://github.com/Grisha-Pochuev/3n-plus-minus-1-game The symbolic global certificate has status CONDITIONAL_MACHINE_CHECK. It checks the declared global assembly but retains four explicit human certificate-to-game obligations described in the repository. Correspondence: n_854@mail.ru