Syracuse descent within ten steps on 424 progressions inside $n \equiv 15 \pmod{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 $47$ residues modulo $2^{13}=8192$: 191, 207, 255, 303, 543, 623, 719, 799, 1071, 1135, 1215, 1247, 1327, 1567, 1727, 1983, 2015, 2079, 2095, 2271, 2431, 2607, 3039, 3135, 3455, 3551, 3903, 3967, 4079, 4159, 4223, 4927, 5023, 5103, 5439, 5615, 5871, 6047, 6559, 6607, 6815, 7023, 7375, 7631, 7791, 7967, 8047.
2. $S_{15}$ consists of the following $99$ residues modulo $2^{15}=32768$: 127, 415, 831, 1151, 1775, 1903, 2303, 2719, 2767, 2799, 2847, 3743, 4031, 4287, 4655, 5231, 5311, 5599, 5631, 6175, 6255, 6783, 7199, 7487, 8063, 8431, 9087, 9375, 9679, 9711, 10655, 10735, 10863, 11119, 11567, 11679, 11807, 11967, 12063, 12143, 12511, 12543, 13007, 13087, 13567, 13695, 14031, 14271, 14399, 14895, 15295, 15343, 15839, 15919, 16287, 16863, 17727, 18639, 18751, 18895, 19199, 19919, 20079, 20527, 20783, 20927, 21023, 21103, 21471, 21727, 21807, 22047, 22207, 22655, 22751, 22911, 23231, 23359, 23615, 23935, 24303, 24559, 24639, 25247, 25503, 25583, 26527, 27759, 27839, 27855, 28703, 28879, 29743, 30591, 30687, 30767, 31711, 32239, 32575.
3. $S_{16}$ consists of the following $278$ residues modulo $2^{16}=65536$: 479, 559, 767, 1183, 1519, 1535, 2367, 2495, 2671, 2687, 2927, 3103, 3487, 3535, 3695, 4319, 4335, 4799, 4815, 4895, 4991, 5087, 5343, 5375, 5423, 5583, 5663, 5823, 6207, 6639, 6703, 6975, 7103, 7231, 7471, 7551, 7711, 7871, 8095, 8671, 8863, 9119, 9199, 9599, 9935, 10559, 11247, 11727, 11823, 11887, 12319, 12495, 12799, 13279, 13535, 13615, 13855, 13951, 14015, 14207, 14303, 14383, 14543, 15103, 15167, 15423, 15487, 15599, 15743, 15855, 16191, 16431, 16511, 16831, 17055, 17135, 17311, 17391, 18159, 18559, 19135, 19151, 19231, 20127, 20207, 20511, 20591, 20687, 21039, 21615, 21695, 22015, 22399, 22495, 22575, 23167, 23583, 23663, 23711, 23743, 24047, 24383, 24703, 24815, 25471, 25599, 26015, 26063, 26351, 26367, 27039, 27119, 27343, 27423, 27903, 27951, 28095, 28191, 28319, 28351, 28447, 28527, 28927, 29087, 29231, 29631, 29807, 29823, 29887, 30079, 30207, 30415, 30575, 30655, 30975, 31199, 31359, 31471, 31727, 31775, 32223, 32303, 32703, 33007, 33087, 33663, 34111, 34255, 34271, 34927, 35023, 35231, 35279, 35311, 35583, 36143, 36159, 36383, 36543, 36639, 36719, 36911, 37119, 37167, 37311, 37407, 37487, 38047, 38271, 38607, 38847, 39039, 39135, 39295, 39535, 39615, 39919, 40351, 40415, 40495, 40687, 40943, 41023, 41183, 42239, 42303, 42911, 43071, 43215, 43471, 43775, 43967, 44143, 44223, 44239, 44959, 45103, 45359, 45503, 45535, 45599, 45679, 46127, 47231, 47327, 47423, 47487, 47807, 48095, 48879, 49135, 49215, 49311, 49567, 49983, 50143, 50303, 50847, 51055, 51103, 51455, 51871, 51951, 52031, 52335, 52415, 52431, 52735, 53183, 53439, 53887, 53919, 54303, 54319, 54751, 55327, 55407, 55535, 56191, 56287, 56639, 57215, 57375, 57759, 57839, 58175, 58495, 58527, 58863, 59247, 59263, 59647, 60015, 60063, 60143, 60271, 60831, 60911, 61135, 61375, 61631, 61663, 62159, 62239, 62719, 62943, 63023, 63519, 63551, 63599, 64047, 64207, 64287, 64447, 64831, 65183, 65407, 65439.

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

These progressions refine the $136$ residual classes modulo $4096$ of the open theorem syracuse_descent_residual_fifteen_mod16_mod4096: every one of the $424$ progressions lies inside one of those classes, and together they cover $852$ of the $2176$ 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. The preamble raises maxRecDepth only so that the $278$-element literal can be elaborated; it does not affect the meaning of the statement.