A strict improvement of the Terras-type bound for integers with long Collatz stopping times

Abstract

Preprint. Let T be the shortcut Collatz map and c = 1 - H(1/log2(3)) = 0.05004..., where H is the binary entropy. The Terras bijection between residues modulo 2^K and parity words shows that at most 2^(alpha(1-c)K + o(K)) integers n <= 2^(alpha K) have coefficient stopping time larger than K. We prove that this Terras-type bound is not sharp: for every alpha in (1/2, 0.659] there is epsilon(alpha) > 0 such that the count is at most 2^((alpha(1-c) - epsilon)K) for all large K, and the same holds for the ordinary stopping time. Consequently, for some epsilon > 0, at most x^(1-c-epsilon) integers n <= x have an orbit that never drops below n. The proof reduces the count, through a bilinear inequality and a decomposition of the frequencies into shells, to a lower bound for the heights of certain lattices, supplied by Bugeaud's bound for linear forms in two m-adic logarithms (m = 8). The qualitative statements are formalized in Lean 4 and checked by the kernel; the special case of Bugeaud's theorem is an explicit hypothesis, derived in Lean from a transcription of the published theorem. The explicit value epsilon(0.6) = 5.35e-14 rests on the written proof and on interval arithmetic outside Lean. The Lean code is published on GitHub. Prepared with substantial assistance from generative AI (Anthropic Claude); see the disclosure in the paper. Not yet reviewed by human experts.