Expanding cycles are not enough: a dichotomy for termination certificates of generalized Collatz maps

Preprint, Part I of two companion papers. Yolcu, Aaronson and Heule reduced the Collatz conjecture and several weakenings of it to the termination of string rewriting systems and proved some of them automatically. We explain this pattern for the positivity-preserving generalized Collatz maps that branch on residues modulo a power of 2 and apply affine branches (Ax+b)/2^e with A odd. If no strongly connected component of the finite abstraction graph on residues contains both an expanding cycle and a branching vertex (the map is disentangled), termination is decidable by a finite computation, and every terminating map has a staged valuation certificate: a lexicographic ranking function built from the logarithm, 2-adic valuations at finitely many rational periodic points, and finite-state weights. If some component contains both (the map is entangled), no such certificate exists, even with arbitrary bounded corrections: the obstruction is not an expanding cycle but its entanglement with branching. For entangled maps, including the Collatz map itself, no ranking function computed from the binary digits by positive, finite arctic, or primitive non-negative weighted automata of positive growth decreases at every step; the key is an equidistribution property of the binary digits of Terras preimages. The soundness of the certificates and five examples are checked in Lean 4; the code is on GitHub. Part II (DOI 10.5281/zenodo.23081491) applies these results to the rewriting system itself. Prepared with substantial assistance from generative AI (Anthropic Claude); see the disclosure in the paper. Not yet reviewed by human experts.