A computer-assisted well-founded descent for Collatz components under dyadic leaf certificates

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_2(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_t=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^r 3^k < 2^A_k; 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