Quantitative Collatz Descent to Stretched-Logarithmic Scale in Natural Density

Abstract

Let T(n)=n/2 for even n and T(n)=(3n+1)/2 for odd n, and write T_min(n)=min_{k≥0} T^k(n). For every 0<δ<δ_end=0.251245530155874..., we prove that T_min(n)≤exp((log n)^(1−δ)) on a set of natural density one, where δ_end=log(1/a_0)/log(2/a_0) and a_0=(log_2 3)/2. Earlier published natural-density theorems give fixed-power bounds; the present threshold is smaller than every fixed power. The descent is witnessed within 6.953 log n half-map iterations. Moreover, for every 0<σ<1−δ/δ_end, the number of exceptions up to X is at most 5X exp(−c(δ,σ)(log X)^σ) for all sufficiently large X. The main input is a central fixed-total Rényi estimate for one fixed 1/2<θ<1, which yields an asymptotically linear density pullback and an endpoint-only bootstrap. The principal theorem chain is formalized in Lean 4. In a smaller range, a companion theorem gives a shrinking-error two-sided orbit envelope and a uniform quantitative first-passage profile. These almost-all results neither prove descent for every initial value nor exclude exceptional cycles or divergent trajectories.

Keywords