Syracuse descent within ten steps on 136 progressions inside $n \equiv 27 \pmod{32}$

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_{15}$ and $S_{16}$ be the two 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_{15}$ consists of the following $37$ residues modulo $2^{15}=32768$: 411, 1275, 2299, 3163, 3611, 4187, 6907, 7163, 8187, 8347, 8795, 9051, 9371, 10075, 12571, 12827, 13851, 16027, 16123, 17147, 18011, 19035, 20507, 22811, 22939, 23803, 23835, 25691, 26267, 27291, 29467, 30715, 30747, 31771, 31899, 32155, 32603.
2. $S_{16}$ consists of the following $99$ residues modulo $2^{16}=65536$: 603, 859, 1179, 1627, 4379, 4635, 6555, 7451, 7835, 7931, 9819, 10907, 11035, 13339, 14363, 14747, 15515, 15643, 15771, 16411, 16635, 17659, 18523, 19099, 19547, 19707, 21595, 22555, 23707, 23963, 24571, 24731, 25371, 25851, 26459, 26619, 27675, 27739, 28507, 30235, 30971, 32283, 32763, 32859, 32923, 33531, 34651, 35419, 35579, 36635, 36891, 37467, 38171, 38427, 39195, 40187, 41243, 41627, 41723, 42075, 42651, 43611, 44699, 45083, 45851, 47099, 47387, 48155, 48379, 48987, 49563, 50267, 50843, 51451, 51611, 52507, 52763, 53339, 54043, 55291, 55963, 56059, 56315, 56347, 57179, 57755, 57947, 58203, 58523, 59643, 60571, 60955, 61531, 61723, 61979, 64251, 64507, 65179, 65275.

Each residue determines an infinite arithmetic progression, so the statement covers every member of $37+99=136$ progressions, not a finite range of inputs. All of them lie in the class $n\equiv 27\pmod{32}$.

These progressions refine the $71$ residual classes modulo $8192$ of the open theorem syracuse_descent_residual_twentyseven_mod32_mod8192_excl8: every one of the $136$ progressions lies inside one of those classes, and together they cover $173$ of the $568$ residue classes modulo $2^{16}$ that lie over them. No further class is settled modulo $2^{14}$. 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 two residue sets are written as explicit Finset ℕ literals, and the uniform bound $t\le10$ is part of the conclusion.