Every odd number below 23501 reaches one under the Syracuse map

Let $T$ be the Syracuse map, sending $n$ to the odd part of $3n+1$. For every odd $m$ with $1 \le m \le 23500$ there is a $k \ge 0$ with $T^k(m) = 1$.

This is one stage in a ladder of verified bounds climbing towards $27113$, which is the small-value threshold needed to exclude Syracuse cycles of every period up to $305$. The range is split into stages purely for practical reasons: a submitted proof is limited to one megabyte of source and to five minutes of verification time, and the whole range in one piece exceeds both.

Each stage is cheap because it stands on the previous one. Every odd number below $20001$ is already known to reach $1$, so an orbit starting in $[20001, 23500]$ need only be followed until it first drops below $20001$; the earlier result takes over from there. That costs $5500$ orbit facts instead of the full closure down to $1$.