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¹³ trajectory stepsfrom N = 10¹¹ 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ᵏ⁺¹, 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 of$2$-adic information. Combined with a metric conflict between Henselattrition (2ᵈ⁺¹ (n+1) for danger runs of length d, density2⁻ᵈ) 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 $8$published 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.