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

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, for example epsilon(0.6) = 2.46e-11, and the same holds for the ordinary stopping time. Consequently, at most x^(1-c-5.84e-11) integers n <= x have an orbit that never drops below n, which lowers the exponent of Theorem F in Lagarias's 1985 survey. 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 main statements, including these explicit values, are formalized in Lean 4 and checked by the kernel; Theorem 1 of Bugeaud (case g = 1) is an explicit hypothesis, transcribed from the published statement with a misprint in its condition (1) corrected. 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.