New Syracuse residual classes at with descent time 12
DefinitionsyracuseSevenMod32New23Step12Classes2-adiccertificate-setcollatznumber-theorysyracuse
The finite set of 525 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 syracuseSevenMod32New23Step12Classes : Finset ℕ := {
1127, 10471, 18663, 38631, 51559, 82023, 86695, 94887, 124263, 128935, 132455, 137127, 152391,
152423, 160583, 214503, 216935, 219239, 227431, 240359, 252071, 270823, 275559, 283751, 313063,
321255, 356423, 378695, 381095, 386887, 389287, 406855, 412775, 420967, 498343, 514791, 530023,
567527, 582727, 608583, 639047, 668391, 681287, 681319, 689479, 690663, 698855, 724647, 762215,
780967, 804455, 812647, 854887, 870119, 883015, 899431, 907623, 935751, 955751, 963943, 1027239,
1030759, 1036615, 1038951, 1056615, 1058887, 1058919, 1067079, 1071847, 1083559, 1092967,
1101159, 1102311, 1144551, 1152743, 1197287, 1200807, 1208999, 1210215, 1238343, 1247719,
1251239, 1260647, 1328615, 1333351, 1341543, 1354471, 1404839, 1411943, 1440071, 1447079,
1455271, 1470535, 1476455, 1499879, 1503399, 1512775, 1520967, 1535079, 1565511, 1587815,
1612455, 1615943, 1617127, 1625319, 1640615, 1648807, 1659367, 1667559, 1688679, 1696839,
1722695, 1739111, 1757863, 1782503, 1808295, 1838759, 1839975, 1858727, 1868103, 1890407,
1911527, 1919719, 1940839, 1985351, 1993543, 2013543, 2021735, 2027591, 2028775, 2035783,
2060455, 2092135, 2106215, 2141351, 2150727, 2164839, 2169511, 2173031, 2177703, 2215271,
2217575, 2255079, 2259815, 2268007, 2279751, 2287943, 2311399, 2316135, 2324327, 2368871,
2374759, 2396999, 2518951, 2520167, 2557671, 2561191, 2569383, 2570599, 2613991, 2623303,
2637415, 2645607, 2656167, 2664359, 2679623, 2731239, 2739431, 2762919, 2772327, 2781671,
2802791, 2845031, 2853223, 2925895, 2931815, 2935271, 2940007, 2945895, 2954087, 2972839,
2977511, 2982215, 2985703, 3033831, 3049063, 3054951, 3099463, 3099495, 3107655, 3118247,
3142887, 3149895, 3171047, 3179239, 3200359, 3275367, 3288295, 3291815, 3293031, 3301223,
3303495, 3319975, 3331687, 3338727, 3345735, 3353927, 3369191, 3373927, 3382119, 3389159,
3402055, 3445415, 3482983, 3495847, 3511111, 3529895, 3538087, 3539271, 3547463, 3577959,
3590887, 3612007, 3620199, 3634279, 3656519, 3671783, 3699943, 3706951, 3708135, 3712871,
3713959, 3721063, 3722151, 3737415, 3748007, 3751527, 3757383, 3759719, 3770279, 3778471,
3848871, 3930983, 3959111, 3997799, 4005991, 4014247, 4040007, 4049383, 4054119, 4068167,
4076359, 4091623, 4099815, 4163175, 4167847, 4176039, 4186599, 4191335, 4194791, 4199527,
4205415, 4213607, 4258151, 4293351, 4308583, 4314471, 4327335, 4342631, 4350823, 4389479,
4409447, 4415335, 4417607, 4459847, 4468039, 4503271, 4554823, 4559527, 4560743, 4563015,
4601767, 4609959, 4611175, 4648679, 4652199, 4661575, 4677991, 4686183, 4692071, 4696743,
4704935, 4720231, 4728423, 4734311, 4805799, 4822247, 4828071, 4835175, 4836263, 4850407,
4853927, 4862119, 4871495, 4871527, 4879719, 4972391, 4975847, 5007527, 5016903, 5026279,
5060327, 5068519, 5089639, 5111911, 5120103, 5190471, 5190503, 5209255, 5218631, 5244391,
5252583, 5278439, 5281959, 5290151, 5291367, 5300711, 5308903, 5313639, 5344071, 5372263,
5379303, 5385127, 5392231, 5394503, 5428551, 5436743, 5464935, 5523559, 5536423, 5544679,
5612615, 5618535, 5620807, 5646663, 5668935, 5668967, 5674855, 5677127, 5698279, 5706471,
5747527, 5754535, 5762727, 5792103, 5800295, 5810855, 5819047, 5839015, 5842535, 5857767,
5870695, 5912903, 5919911, 5993831, 5996135, 6014887, 6021991, 6057127, 6065319, 6066503,
6074695, 6080615, 6088807, 6089959, 6113447, 6121639, 6132199, 6140391, 6182631, 6203751,
6225991, 6227175, 6231911, 6235367, 6240103, 6250663, 6258855, 6298727, 6304615, 6336231,
6349159, 6358503, 6366695, 6367911, 6384359, 6392551, 6399591, 6434727, 6442919, 6450023,
6458183, 6500423, 6508615, 6537959, 6550855, 6550887, 6564967, 6595399, 6603591, 6642343,
6650535, 6704455, 6718567, 6726727, 6726759, 6732647, 6734919, 6739687, 6752583, 6760775,
6760807, 6768999, 6812391, 6820583, 6846375, 6861671, 6868647, 6869863, 6876839, 6896807,
6906183, 6915559, 6978919, 7066855, 7072679, 7098535, 7107911, 7110247, 7128999, 7171239,
7179431, 7180615, 7188807, 7202919, 7245159, 7247463, 7255655, 7283783, 7284967, 7293159,
7341287, 7349479, 7354215, 7356519, 7369447, 7372967, 7398759, 7404647, 7406951, 7412839,
7425703, 7435079, 7450343, 7526567, 7545319, 7548839, 7557031, 7558247, 7564135, 7587559,
7595751, 7643879, 7652071, 7653191, 7661383, 7709511, 7717703, 7728295, 7737671, 7759975,
7781095, 7789287, 7818567, 7832679, 7840871, 7883111, 7898343, 7911271, 7913543, 7930023,
7955783, 7960487, 7963975, 7965159, 7973351, 7983975, 8002727, 8010919, 8012103, 8020295,
8036711, 8055463, 8084839, 8087143, 8093031, 8105895, 8121191, 8129383, 8149319, 8157511,
8172775, 8180967, 8186791, 8212647, 8238439, 8266567, 8305255, 8313447, 8333383, 8341575,
8358055, 8361575, 8369767, 8376807
}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).