Combinatorial Saturation and Machine-Checked Reduction of the Collatz Conjecture

The branch locus of the Syracuse map saturates at exactly 21, 632cells. We reduce the Collatz conjecture to a finite-state mixing problem onthis saturated core: six structural properties, ranging from Diophantinedeficit bounds to 2-adic residue equidistribution, are each machine-checkedin Lean~4 to be equivalent to the full conjecture, and all six concern thedynamics of trajectories confined to the same 21, 632 branch cells on the (2, 3) -torus at resolutions k 216 = 2³ 3³. The saturation isestablished by exhaustive computation over 2. 5 10^13 trajectory stepsfrom N = 10^11 starting values, and is stable across three orders ofmagnitude in starting range. The principal technical innovation is a bit-peeling lemma: the compressedCollatz map T (n) = (3n+1) /2 satisfies T (n) 2ᵏ depends only onn 2^k+1, giving exact 1-bit erosion per compressed step. This isthe first formal proof that the Collatz map operates as a lossyinformation channel, each application irreversibly destroys one bit of2-adic information. Combined with a metric conflict between Henselattrition (2^d+1 (n+1) for danger runs of length d, density2^-d) and Baker separation (cell error shift > d/2), we show thatindividual danger runs of length d 2 are self-defeating. The frameworkis formalized in 10, 500 lines of Lean~4 with Mathlib, grounded in 8published axioms (Baker, Rhin, Hercher, Weyl, Matveev, Denjoy--Koksma, Furstenberg). The saturation constant 21, 632 represents a fundamentalinformation ceiling of the Syracuse map; we conjecture it is determined by thecontinued fraction expansion of 3.