Residual Syracuse descent inside $n \equiv 15 \pmod{16}$ modulo $2^{16}$

Let $T$ denote the Syracuse map on the natural numbers, $T(n)=(3n+1)/2^{v_2(3n+1)}$, the odd part of $3n+1$, and let $T^t$ denote its $t$-fold iterate, with $T^0(n)=n$. Consider a natural number $n$ with

satisfying the exclusions inherited from syracuse_descent_residual_fifteen_mod16_mod4096,

and the three further exclusions

where 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.

The open assertion is

This is the residual subproblem of syracuse_descent_residual_fifteen_mod16_mod4096 left after separating the $424$ arithmetic progressions of syracuse_descent_progressions_fifteen_mod16_mod65536, on which descent holds within ten Syracuse steps. The admissible $n$ form $1324$ of the $2176$ residue classes modulo $2^{16}$ lying over the $136$ classes modulo $4096$ of the parent statement, about $60.8\%$ of its density. Neither the starting value nor the descent time is bounded, and the assertion is an unproved special case of the Collatz conjecture.

Formalization Note. The Syracuse map is the existing platform definition syracuseStep. The first five hypotheses are copied verbatim from syracuse_descent_residual_fifteen_mod16_mod4096; the three new exclusions are negated memberships in explicit Finset ℕ literals. The preamble raises maxRecDepth only so that the $278$-element literal can be elaborated. No oddness or positivity hypothesis is needed, since $n\equiv15\pmod{16}$ forces both.