New Syracuse residual classes at with descent time 13
DefinitionsyracuseSevenMod32New23Step13Classes2-adiccertificate-setcollatznumber-theorysyracuse
The finite set of 1570 residue representatives modulo that first become uniformly certifiable at this refinement stage with accelerated Syracuse descent time and total stripped exponent . The set is computed exactly from the residual branch descending from syracuse_descent_residual_seven_mod32_mod1048576.
Definition code
import Mathlib.Data.Finset.Insert
set_option maxRecDepth 200000
def syracuseSevenMod32New23Step13Classes : Finset ℕ := {
327, 20647, 24935, 30023, 32359, 33127, 43687, 51111, 51879, 51943, 58215, 71847, 73063, 75367,
90599, 93351, 95335, 101543, 102727, 103527, 110919, 116839, 117575, 125031, 132839, 145735,
149671, 152743, 160999, 167271, 168007, 168423, 169575, 173927, 177767, 198471, 205895, 207079,
212583, 215271, 220775, 226663, 228967, 231335, 239527, 247719, 254823, 262215, 263399, 268135,
271591, 276327, 278631, 286887, 289959, 291559, 295079, 298151, 299335, 307527, 309927, 311143,
313447, 320871, 321639, 322791, 326759, 329063, 334951, 346279, 347815, 354471, 357191, 365031,
372455, 373223, 385383, 392039, 404135, 415463, 420167, 420583, 435815, 436583, 448679, 458823,
460007, 464743, 467431, 468199, 470951, 472935, 475303, 479143, 480359, 483495, 486247, 491687,
501063, 509671, 510439, 515175, 517863, 529223, 531559, 536647, 537447, 552679, 560871, 565991,
569063, 574183, 575303, 581991, 583495, 587111, 591335, 599527, 600743, 601191, 617191, 624231,
625383, 631623, 632423, 639815, 650407, 652391, 659783, 666471, 667559, 674663, 675751, 678567,
682087, 682855, 691015, 703207, 711399, 730983, 733255, 740679, 741447, 754407, 754791, 762983,
769639, 770791, 775527, 775911, 783687, 783719, 788391, 788807, 797031, 797799, 803687, 805223,
820455, 828231, 833383, 835655, 836423, 850535, 852135, 875175, 876391, 877895, 878663, 882599,
883367, 886087, 887271, 895463, 897895, 906087, 920903, 924839, 929095, 933031, 934215, 937287,
942407, 951399, 951783, 958823, 959559, 959591, 964327, 965479, 967751, 972519, 977575, 985415,
993607, 993639, 1001831, 1006951, 1009255, 1015143, 1020583, 1028007, 1032359, 1043303, 1045223,
1051495, 1053415, 1062823, 1071015, 1071431, 1072231, 1079207, 1079623, 1094503, 1094887,
1101479, 1102695, 1103079, 1108903, 1109671, 1109735, 1113255, 1122631, 1129639, 1134759,
1139015, 1144135, 1148391, 1153127, 1160551, 1181287, 1188679, 1195367, 1211751, 1223527,
1227367, 1235559, 1255495, 1263687, 1280167, 1281383, 1283303, 1283687, 1289127, 1291879,
1296231, 1297319, 1298919, 1299687, 1305511, 1311463, 1311847, 1314983, 1320007, 1321191,
1323175, 1329383, 1331367, 1332551, 1332583, 1340743, 1343079, 1349351, 1360743, 1361831,
1362279, 1392743, 1397415, 1404071, 1405607, 1405671, 1412263, 1413447, 1421639, 1433447,
1434983, 1435751, 1439655, 1440871, 1443175, 1447847, 1461927, 1463111, 1463143, 1471303,
1477959, 1477991, 1480295, 1488487, 1516615, 1517799, 1521383, 1525223, 1525991, 1527655,
1529959, 1538151, 1551079, 1562791, 1572967, 1574119, 1581159, 1581543, 1582311, 1586279,
1587047, 1589351, 1594471, 1602279, 1605799, 1619879, 1623783, 1631591, 1631975, 1637479,
1639783, 1645671, 1651527, 1658535, 1667143, 1667911, 1670311, 1679687, 1680103, 1683175,
1689415, 1691815, 1697607, 1700007, 1717575, 1723495, 1731687, 1743015, 1751207, 1752423,
1759399, 1761767, 1764519, 1769959, 1773895, 1774695, 1778151, 1781671, 1789863, 1791079,
1796199, 1796967, 1802087, 1809063, 1817319, 1820391, 1825511, 1828583, 1833319, 1840359,
1840743, 1846183, 1853287, 1872039, 1876711, 1878247, 1884903, 1886023, 1889607, 1893447,
1894215, 1919303, 1925991, 1934567, 1942343, 1947495, 1949767, 1950535, 1961127, 1966247,
1970503, 1979111, 1984615, 1992007, 1992039, 1992807, 2000199, 2001383, 2005735, 2009575,
2013927, 2022119, 2035367, 2038951, 2048327, 2051399, 2065511, 2072935, 2073703, 2091687,
2115175, 2115943, 2121063, 2123367, 2129991, 2130023, 2131175, 2135911, 2138183, 2142119,
2144103, 2146375, 2157415, 2162855, 2165607, 2180839, 2185543, 2188615, 2193319, 2193735,
2196807, 2197991, 2206183, 2208583, 2208999, 2210151, 2216807, 2218343, 2221927, 2235559,
2243751, 2244935, 2246471, 2253127, 2253159, 2261351, 2266471, 2269543, 2271911, 2274663,
2280103, 2288295, 2300071, 2302791, 2303591, 2317671, 2318823, 2319975, 2325863, 2331751,
2337959, 2338727, 2341479, 2347335, 2349671, 2354023, 2362215, 2367335, 2369607, 2369639,
2373959, 2377799, 2380967, 2382151, 2382567, 2390343, 2394279, 2403687, 2405607, 2411879,
2413031, 2413799, 2419623, 2425959, 2445479, 2454887, 2455271, 2463463, 2471271, 2476391,
2483047, 2499399, 2508007, 2511527, 2519719, 2520935, 2538087, 2541671, 2546279, 2549063,
2551015, 2553767, 2558439, 2561959, 2562791, 2566215, 2571367, 2574407, 2574503, 2577223,
2577255, 2582695, 2590887, 2593255, 2594407, 2601447, 2602599, 2609639, 2622567, 2631911,
2639335, 2640103, 2641767, 2643687, 2644071, 2652263, 2660071, 2664807, 2665191, 2672999,
2687047, 2692967, 2700391, 2703463, 2708135, 2711719, 2715559, 2716327, 2722663, 2745703,
2750375, 2750791, 2753895, 2757799, 2758567, 2765671, 2765991, 2773831, 2773863, 2781255,
2782023, 2787175, 2805927, 2810215, 2810599, 2814119, 2819559, 2823495, 2827751, 2828967,
2831687, 2835943, 2837607, 2838375, 2840679, 2845415, 2845799, 2848871, 2851687, 2853607,
2860647, 2861799, 2873511, 2876231, 2892263, 2896999, 2898535, 2905191, 2919239, 2923175,
2926663, 2927847, 2931015, 2934503, 2936039, 2942695, 2951335, 2954855, 2959527, 2961479,
2969671, 2970087, 2977863, 2978279, 2992359, 2999399, 3000135, 3002535, 3007559, 3008327,
3010727, 3011911, 3011943, 3026023, 3028295, 3033415, 3034215, 3042407, 3049831, 3068583,
3093223, 3103399, 3106151, 3111591, 3119015, 3119783, 3131559, 3136231, 3149479, 3150311,
3150695, 3151463, 3169447, 3178823, 3187783, 3188967, 3193703, 3195975, 3200743, 3201127,
3204167, 3213639, 3221831, 3221863, 3222247, 3229287, 3230023, 3230439, 3251559, 3260487,
3268775, 3273447, 3281639, 3289831, 3294951, 3296071, 3302727, 3302759, 3304263, 3310919,
3312103, 3320295, 3322727, 3324263, 3329703, 3332455, 3337895, 3338311, 3339495, 3346087,
3346503, 3360583, 3371175, 3376615, 3380583, 3383655, 3402407, 3402471, 3402855, 3416935,
3425895, 3434087, 3452071, 3461447, 3475559, 3476327, 3480231, 3481447, 3483751, 3488423,
3491559, 3496679, 3504455, 3517799, 3518535, 3520871, 3525991, 3528295, 3529063, 3557191,
3565799, 3568967, 3569383, 3570535, 3571303, 3577191, 3578727, 3583079, 3585383, 3590055,
3590471, 3598663, 3622119, 3626855, 3632295, 3635047, 3640487, 3641671, 3648679, 3649863,
3652199, 3658055, 3660391, 3660455, 3663175, 3663975, 3672551, 3678055, 3679591, 3680327,
3680359, 3685479, 3688519, 3693287, 3704999, 3706215, 3707719, 3714407, 3722599, 3723751,
3744839, 3765991, 3770695, 3774183, 3802343, 3810535, 3815271, 3818727, 3822247, 3829671,
3830439, 3830503, 3830887, 3831655, 3834023, 3836775, 3859783, 3864903, 3865703, 3868391,
3869159, 3871911, 3872679, 3873895, 3880103, 3881319, 3882087, 3886759, 3901287, 3911399,
3924711, 3934023, 3937607, 3948135, 3950055, 3954791, 3956327, 3962983, 3966887, 3975079,
3975911, 3990343, 4009895, 4012647, 4018087, 4025191, 4026279, 4033383, 4040775, 4041959,
4050151, 4061511, 4065447, 4068519, 4073639, 4076711, 4083047, 4084199, 4091975, 4092391,
4097895, 4104935, 4113127, 4113511, 4121319, 4124839, 4134215, 4142407, 4155751, 4156519,
4163943, 4170567, 4178759, 4182695, 4186951, 4189351, 4198727, 4209255, 4221031, 4233127,
4233895, 4236615, 4237383, 4238567, 4242151, 4242535, 4245991, 4246759, 4250727, 4256615,
4262055, 4263271, 4264807, 4270247, 4279623, 4280807, 4283559, 4288231, 4288999, 4292935,
4293735, 4296423, 4301927, 4310119, 4315239, 4318279, 4336359, 4344135, 4344167, 4344551,
4359399, 4359783, 4360551, 4365671, 4372327, 4379303, 4391079, 4403943, 4410183, 4410215,
4418375, 4421543, 4422759, 4428967, 4429735, 4445031, 4452423, 4453607, 4460199, 4460615,
4461415, 4463783, 4471975, 4473159, 4480167, 4481351, 4481767, 4485287, 4489543, 4489959,
4511079, 4511847, 4516967, 4531047, 4532967, 4541159, 4545895, 4554087, 4562279, 4566951,
4582247, 4586087, 4589671, 4594343, 4599015, 4602535, 4603751, 4606791, 4610375, 4611943,
4614215, 4614983, 4630695, 4633831, 4634983, 4642023, 4642407, 4643175, 4647847, 4649031,
4649447, 4650215, 4656455, 4657223, 4661991, 4664647, 4673703, 4679911, 4681895, 4684647,
4692839, 4699879, 4704583, 4712775, 4713575, 4727623, 4727655, 4740967, 4756135, 4759719,
4762791, 4772167, 4786279, 4790951, 4793703, 4794471, 4799143, 4799207, 4806567, 4821831,
4822631, 4830823, 4836711, 4839015, 4840615, 4848807, 4849991, 4850791, 4858183, 4860135,
4868327, 4876519, 4881255, 4888679, 4889447, 4901191, 4901223, 4901607, 4909383, 4922727,
4930919, 4931687, 4932839, 4937575, 4944999, 4945767, 4967239, 4973927, 4978599, 4982119,
4982503, 4990311, 4995431, 4996199, 5002055, 5002087, 5010247, 5010663, 5017671, 5018439,
5018855, 5020839, 5023591, 5024679, 5030215, 5031783, 5032871, 5048135, 5058727, 5062247,
5066599, 5068103, 5070439, 5080999, 5089191, 5101735, 5102951, 5120487, 5125223, 5133415,
5140391, 5141607, 5159591, 5162727, 5167431, 5170919, 5179111, 5182631, 5190823, 5190887,
5192039, 5197159, 5228359, 5230759, 5235431, 5236551, 5241703, 5244743, 5258855, 5262439,
5267047, 5269831, 5269863, 5277607, 5285799, 5301063, 5308519, 5316711, 5324967, 5350727,
5352679, 5356647, 5360103, 5360871, 5364455, 5364839, 5370727, 5378887, 5379687, 5384359,
5387079, 5393767, 5402343, 5403111, 5410535, 5417191, 5424231, 5466471, 5473895, 5474663,
5478567, 5486759, 5488711, 5497319, 5502055, 5505511, 5510247, 5516135, 5524327, 5530951,
5530983, 5539143, 5540327, 5543079, 5547335, 5548519, 5553255, 5556711, 5559111, 5561447,
5567335, 5568871, 5575527, 5594279, 5595879, 5598951, 5603655, 5604071, 5607143, 5611879,
5619303, 5623655, 5625191, 5630631, 5638055, 5653351, 5654119, 5655271, 5661543, 5662311,
5670503, 5676391, 5682279, 5700199, 5704551, 5713127, 5717863, 5719783, 5720167, 5720903,
5720935, 5726055, 5728327, 5729095, 5732679, 5739687, 5744807, 5763559, 5764327, 5770567,
5771335, 5778759, 5785415, 5792487, 5800679, 5805415, 5813607, 5813991, 5819495, 5821799,
5865543, 5870247, 5871463, 5873735, 5880423, 5888615, 5896807, 5906279, 5908551, 5909735,
5912487, 5913255, 5914471, 5916743, 5920679, 5921511, 5921895, 5922663, 5924935, 5933223,
5941415, 5942631, 5951975, 5953127, 5954727, 5959399, 5960167, 5962919, 5964103, 5967175,
5972295, 5975367, 5988711, 5990631, 5994215, 5995367, 5996903, 6002407, 6002791, 6003559,
6007463, 6010599, 6015655, 6015719, 6023495, 6030951, 6036839, 6039143, 6045031, 6050471,
6058663, 6066855, 6081351, 6088007, 6097383, 6100903, 6104423, 6116519, 6117287, 6124775,
6131783, 6132551, 6132967, 6137703, 6138791, 6145895, 6146983, 6151335, 6159527, 6160711,
6161127, 6164647, 6168903, 6172839, 6178279, 6182215, 6182247, 6183015, 6190439, 6191207,
6199399, 6204135, 6211175, 6212327, 6233447, 6241639, 6255719, 6261607, 6273703, 6277959,
6283111, 6286567, 6289735, 6290151, 6293223, 6318247, 6320199, 6321383, 6326119, 6327623,
6328391, 6329575, 6334311, 6335399, 6336999, 6342503, 6343591, 6353063, 6355815, 6358855,
6362439, 6362471, 6369447, 6370631, 6371047, 6372967, 6378823, 6379239, 6381159, 6383943,
6384743, 6391719, 6399911, 6400359, 6422631, 6430823, 6437479, 6439079, 6462119, 6463335,
6465607, 6470311, 6490279, 6492999, 6499687, 6501191, 6501223, 6509031, 6519975, 6529351,
6546503, 6551271, 6552423, 6555111, 6563303, 6572359, 6580551, 6589159, 6592679, 6600871,
6602087, 6607527, 6611431, 6616167, 6619239, 6619623, 6624359, 6627431, 6630247, 6632167,
6635687, 6654791, 6657959, 6658375, 6661447, 6670823, 6675559, 6682983, 6688423, 6689607,
6690023, 6695847, 6697799, 6702951, 6705223, 6713063, 6721255, 6733415, 6739271, 6740071,
6747463, 6752167, 6761191, 6767463, 6775655, 6784615, 6789287, 6797479, 6808039, 6812775,
6816231, 6820967, 6826855, 6834279, 6835047, 6847143, 6855399, 6863207, 6871399, 6877255,
6879591, 6883175, 6910119, 6914791, 6919495, 6923335, 6929255, 6930023, 6931527, 6935911,
6941799, 6948775, 6955879, 6957383, 6964071, 6972263, 6979655, 6979687, 6985575, 6987847,
6991015, 7000391, 7008999, 7010919, 7014503, 7017191, 7019175, 7022695, 7026599, 7030887,
7036007, 7036775, 7039047, 7058247, 7064935, 7065255, 7073447, 7073511, 7081287, 7089479,
7102823, 7111015, 7114599, 7121575, 7124711, 7129415, 7129767, 7145063, 7149735, 7153255,
7161063, 7165799, 7168487, 7173991, 7176263, 7180967, 7181415, 7182183, 7184455, 7223207,
7223623, 7224423, 7230631, 7231399, 7232615, 7270119, 7273639, 7275239, 7278759, 7283015,
7296359, 7299431, 7304551, 7306855, 7307623, 7310439, 7313511, 7318183, 7325607, 7326375,
7332711, 7341671, 7349863, 7355751, 7367847, 7368615, 7376039, 7377223, 7385415, 7391335,
7397223, 7399527, 7400679, 7410855, 7419047, 7420263, 7424167, 7427239, 7432359, 7441735,
7442919, 7443687, 7449511, 7451111, 7456615, 7457703, 7463655, 7471847, 7475367, 7483559,
7485159, 7492935, 7492967, 7493351, 7501159, 7512935, 7514471, 7529287, 7536711, 7537895,
7542631, 7546087, 7550823, 7561383, 7569575, 7571559, 7580903, 7589095, 7593831, 7597287,
7609447, 7612583, 7615335, 7621991, 7628967, 7631335, 7634087, 7638343, 7643463, 7646951,
7647719, 7652455, 7659879, 7669223, 7677415, 7678631, 7681767, 7689959, 7694695, 7695079,
7702887, 7703271, 7710311, 7711079, 7716199, 7722855, 7733351, 7741543, 7745447, 7753639,
7760743, 7768903, 7781479, 7795559, 7803751, 7804135, 7809959, 7811143, 7811911, 7811943,
7817063, 7819335, 7822503, 7830695, 7831879, 7840071, 7848679, 7853383, 7860071, 7861575,
7861607, 7865831, 7874023, 7875687, 7883495, 7899879, 7903399, 7904615, 7906119, 7911591,
7912807, 7914311, 7922151, 7930343, 7935079, 7949127, 7953063, 7957319, 7961255, 7965511,
7967911, 7969511, 7990631, 7992551, 7993703, 7999559, 8000743, 8006567, 8013671, 8015175,
8015943, 8020711, 8029287, 8037447, 8037479, 8043367, 8045639, 8049991, 8050407, 8058183,
8063303, 8071495, 8071527, 8079719, 8086375, 8093799, 8123111, 8131303, 8137959, 8141479,
8142695, 8144999, 8157095, 8157863, 8166119, 8169639, 8172359, 8172391, 8179367, 8180583,
8181351, 8187559, 8188391, 8207527, 8216903, 8218855, 8223591, 8226279, 8231783, 8234055,
8239975, 8242247, 8251719, 8251751, 8263847, 8268103, 8282599, 8289639, 8290375, 8290407,
8295527, 8296295, 8298567, 8319719, 8327911, 8332647, 8337735, 8352615, 8360775, 8368967,
8375975, 8377575, 8379559, 8383399, 8384167
}Source
Computational residue refinement of https://prove2.me/theorems/8d2d08ed-fda7-4e9b-b521-cfa49347ded2 using https://prove2.me/theorems/cd79de19-4613-42b0-afc9-48de75023e4a (Terras uniformity).