The argument developed in this paper is a component-wise descent for the Collatz problem, combining ananalytic reduction with a finite computer-assisted certification over dyadic residue classes. The first step isan anti-9 lift: every odd integer not divisible by 3 lies on the forward orbit of an odd multiple of 3. It istherefore enough to prove convergence for integers of the form 3u, where u is a positive odd integer. The descent is then carried by the parameter u. The initial dyadic valuation e (u) =v₂ (9u+1) separates theproof into two regimes. For e (u) >= 7, the congruence 9u+1 == 0 mod 128 gives u == 71 mod 128 andyields the explicit contraction u*= (u-7) /64. The integer u* is positive, odd, smaller than u, and the forwardorbit of 3u* meets the forward orbit of 3u. For e (u) <= 6, the positive odd parameters are organized into dyadic residue classes moduloMₜ=9*2^ (14+6t). On a certified terminal leaf, a finite valuation word is stable, so the accelerated iteratesbecome affine functions of u. The certificate records a finite accelerated trajectory, an inverse anti-9exponent, and the slope condition 2ʳ 3ᵏ < 2Aₖ; this propagates a descent inequality verified at theminimal representative to the whole leaf. The analytic part proves that every certified leaf yields a strict descent u' < u with orbit coalescence. Theremaining finite statement is established by a deterministic companion archive, which verifies coverage ofthe dyadic domain, stability of valuation words, validity of certificates, and convergence of the finite baserange. A supplementary Lean shell also checks the global descent structure modulo four explicitproject-specific assumptions. The result is therefore a computer-assisted theorem based on residue-classcertification, not on brute-force verification up to a single numerical bound
julian redero (Sat,) studied this question.