Syracuse descent within ten steps on 155 progressions modulo $2^{16}$

Let $T$ denote the Syracuse map on the natural numbers,

that is, the odd part of $3n+1$, where $v_2$ is the $2$-adic valuation, and let $T^t$ denote its $t$-fold iterate, with $T^0(n)=n$. Let $S_{13}$, $S_{15}$ and $S_{16}$ be the three finite sets of residues listed below. For every natural number $n$ satisfying

there is a natural number $t$ with

The residue sets are:

1. $S_{13}$ consists of the following $19$ residues modulo $2^{13}=8192$: 679, 1191, 2663, 3687, 4199, 4455, 5191, 5607, 5959, 6215, 6375, 6631, 6983, 7079, 7399, 7495, 7847, 7911, 8103.
2. $S_{15}$ consists of the following $37$ residues modulo $2^{15}=32768$: 839, 1095, 2119, 2279, 2727, 2983, 3303, 4007, 6503, 6759, 7783, 9959, 10055, 11079, 11943, 12967, 14439, 16743, 16871, 17735, 17767, 19623, 20199, 21223, 23399, 24647, 24679, 25703, 25831, 26087, 26535, 27111, 27975, 28999, 29863, 30311, 30887.
3. $S_{16}$ consists of the following $99$ residues modulo $2^{16}=65536$: 359, 1351, 2407, 2791, 2887, 3239, 3815, 4775, 5863, 6247, 7015, 8263, 8551, 9319, 9543, 10151, 10727, 11431, 12007, 12615, 12775, 13671, 13927, 14503, 15207, 16455, 17127, 17223, 17479, 17511, 18343, 18919, 19111, 19367, 19687, 20807, 21735, 22119, 22695, 22887, 23143, 25415, 25671, 26343, 26439, 27303, 27559, 27879, 28327, 31079, 31335, 33255, 34151, 34535, 34631, 36519, 37607, 37735, 40039, 41063, 41447, 42215, 42343, 42471, 43111, 43335, 44359, 45223, 45799, 46247, 46407, 48295, 49255, 50407, 50663, 51271, 51431, 52071, 52551, 53159, 53319, 54375, 54439, 55207, 56935, 57671, 58983, 59463, 59559, 59623, 60231, 61351, 62119, 62279, 63335, 63591, 64167, 64871, 65127.

Each residue determines an infinite arithmetic progression, so the statement covers every member of $19+37+99=155$ progressions, not a finite range of inputs.

These progressions refine the $45$ residual classes modulo $4096$ of the open theorem syracuse_descent_residual_mod4096: every one of the $155$ progressions lies inside one of those classes, and together they cover $325$ of the $720$ residue classes modulo $2^{16}$ that lie over them. Combined with the complementary residual statement, this splits that open theorem into a proved part with a uniform ten-step bound and a smaller open part.

Formalization Note. The Syracuse map is the existing platform definition syracuseStep, and $T^t$ is the Mathlib iterate syracuseStep^[t]. The three residue sets are written as explicit Finset ℕ literals, and the uniform bound $t\le10$ is part of the conclusion.