HEXAGONbeta

Positive density of Collatz convergence at every rate above 3/log(4/3)

A mix of human-written and AI-generated textHuman understanding: all partsmath.NT — Number Theorymath.DS — Dynamical Systems

Contributed by Idris Ali Shaik ↗

Version 1 / Oct 26, 2026 / CC BY 4.0

Abstract

We prove that a positive proportion of positive integers reach 1 within c log x ordinary Collatz steps for every fixed c > 3/log(4/3), with one positive lower natural-density bound independent of c. For each fixed positive target not divisible by three, the same range of times holds with a target-dependent bound, irrespective of its subsequent orbit. Targets divisible by three have predecessor basins of natural density zero. Diagonalization gives one positive-density set with a vanishing excess above the limiting time coefficient. The proof extends weighted inverse trajectories from a fixed finite family of roots and preserves positive weighted mass at every sufficiently large scale. We derive an explicit Fourier-decay estimate, at frequencies not divisible by three, for an auxiliary distribution on residue classes. Its proof uses paired geometric valuations and their exact binomial first-passage law. At order 6409, the coefficient C satisfies log_2 log_2 log_2 C < 176, compared with > 2^172 for the explicit coefficient in Mazur's work. Fractional-moment certificates, residue-capacity bounds, and an enlarged family of roots give explicit density estimates after harmonic and dyadic counting. Further refinements locate surviving mass within the root family, retain conditional residue information, and recover additional distinct sources with a bounded extra step cost. The primitive-decay theorem and the main qualitative density conclusions are formalized in Lean 4. The coefficient-size comparison and the complete optimized density bounds remain paper proofs.

Provenance statement

AI-assisted tools were used in manuscript preparation, Lean proof development, code preparation, and editorial revision.

Formalizations

Tools used

Lean
Lean

References

No bibliography entries.

Version history

  1. v1Submitted by Idris Ali ShaikInitial depositCurrentOct 24, 2026