New Syracuse step-15 certificate classes, chunk 1
DefinitionsyracuseSevenMod32New26Step15Chunk01Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 1 of 13 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 746 exact residue representatives and is kept moderate in size for reusable Lean compilation.
Definition code
import Mathlib.Data.Finset.Insert
set_option maxRecDepth 200000
def syracuseSevenMod32New26Step15Chunk01Classes : Finset ℕ := {
1895, 2535, 4967, 9031, 12455, 15079, 16711, 18535, 22375, 35143, 45895, 46311, 49319, 55015,
59239, 60327, 61511, 76103, 89447, 95559, 111975, 129767, 130215, 133223, 137063, 137895, 140359,
156135, 176999, 186983, 195431, 200359, 206183, 210855, 213095, 216743, 225447, 233319, 233959,
243303, 248135, 256679, 257703, 267591, 270439, 273063, 280167, 280807, 284007, 302247, 306279,
312167, 313191, 314023, 337511, 339303, 342759, 345831, 348071, 350055, 359591, 363623, 363687,
365671, 370759, 380263, 383303, 383335, 387175, 400103, 414535, 423239, 425831, 439655, 443495,
444327, 456039, 459495, 468455, 497991, 501671, 514663, 524359, 539751, 542567, 581479, 599911,
602183, 616551, 623847, 641511, 649031, 651431, 664807, 673895, 674919, 687271, 688295, 697191,
710823, 710983, 714055, 722151, 745639, 746855, 751527, 755559, 768167, 768327, 768743, 771815,
775015, 791655, 802407, 823463, 824487, 827719, 828135, 834407, 836679, 844135, 846951, 853479,
862567, 866215, 870247, 885479, 896231, 900455, 912039, 919719, 922791, 928615, 935527, 963687,
969383, 970407, 972007, 979111, 988007, 992071, 992871, 1001191, 1007463, 1009735, 1018215,
1021031, 1025127, 1029351, 1031783, 1033031, 1038055, 1044327, 1044967, 1059943, 1074535,
1081447, 1083879, 1086119, 1090375, 1095015, 1096423, 1114279, 1114855, 1122151, 1136967,
1140039, 1143271, 1150311, 1152167, 1153767, 1160039, 1170023, 1170599, 1196359, 1205863,
1207655, 1208487, 1212775, 1221703, 1231591, 1236839, 1253703, 1264455, 1269095, 1270119,
1285287, 1289383, 1304935, 1309799, 1325415, 1326247, 1326439, 1340231, 1345703, 1348711,
1352551, 1353575, 1365351, 1369415, 1372647, 1385191, 1387239, 1397575, 1400423, 1400999,
1406279, 1406695, 1413191, 1440359, 1449831, 1450471, 1452103, 1464647, 1472359, 1483079,
1489575, 1496679, 1498279, 1499495, 1505191, 1507175, 1508839, 1509863, 1511495, 1521991,
1528679, 1534183, 1555815, 1559271, 1594727, 1599815, 1603687, 1613991, 1616231, 1617063,
1622887, 1633447, 1634471, 1640551, 1644391, 1645223, 1657959, 1660839, 1667751, 1674407,
1681255, 1694439, 1697895, 1699687, 1700711, 1715303, 1721831, 1728679, 1740871, 1743719,
1753415, 1753831, 1755463, 1772647, 1774919, 1780391, 1785447, 1800039, 1803879, 1808551,
1809127, 1813223, 1816423, 1817255, 1818695, 1826151, 1827175, 1828199, 1832039, 1832871,
1856359, 1870567, 1877063, 1878087, 1902407, 1903975, 1918567, 1925863, 1927495, 1928295,
1946727, 1950823, 1963367, 1964391, 1968039, 1970663, 1984231, 1987687, 1991527, 2021543,
2025191, 2042599, 2042983, 2044647, 2047847, 2048871, 2062663, 2063463, 2071207, 2079463,
2082535, 2090055, 2122055, 2128551, 2134183, 2135399, 2138855, 2159719, 2162791, 2164583,
2177351, 2181447, 2194791, 2210407, 2219111, 2222951, 2238791, 2254183, 2256615, 2263527,
2272423, 2278503, 2294087, 2294887, 2295719, 2295911, 2300583, 2329767, 2332391, 2335847,
2338887, 2348391, 2352455, 2353255, 2354279, 2359783, 2366823, 2376551, 2378599, 2385511,
2389735, 2392167, 2393415, 2396007, 2406759, 2410823, 2412871, 2423399, 2424999, 2430887,
2446503, 2447687, 2448103, 2450759, 2455399, 2466151, 2492903, 2502823, 2507079, 2510695,
2523495, 2526311, 2539687, 2541927, 2560167, 2566247, 2579815, 2597031, 2599079, 2607015,
2620135, 2624839, 2629479, 2631751, 2643879, 2657639, 2665319, 2666983, 2674855, 2685799,
2700615, 2724327, 2725735, 2728007, 2757959, 2760807, 2770151, 2775783, 2781095, 2794215,
2815911, 2816327, 2817127, 2827495, 2829671, 2832743, 2839015, 2839399, 2849959, 2850983,
2853991, 2857063, 2861127, 2861735, 2885223, 2887015, 2887847, 2901479, 2907751, 2921127,
2926951, 2933863, 2937511, 2955111, 2958823, 2964071, 2976615, 2978471, 2979047, 2988359,
2991207, 2993063, 3001575, 3005607, 3007207, 3020391, 3025063, 3025639, 3028135, 3032935,
3034791, 3035207, 3044711, 3046503, 3057895, 3066599, 3080359, 3091111, 3092551, 3107943,
3121895, 3123943, 3137703, 3138375, 3140775, 3144007, 3145831, 3147623, 3162439, 3164263,
3177639, 3184551, 3186535, 3188583, 3189223, 3195719, 3207239, 3208039, 3216743, 3235175,
3235431, 3243879, 3264359, 3269703, 3274087, 3278951, 3283623, 3291751, 3293351, 3295591,
3311207, 3323751, 3324583, 3324775, 3327047, 3337319, 3342823, 3347271, 3352935, 3356583,
3360615, 3369799, 3375431, 3379047, 3381927, 3393863, 3403431, 3405031, 3408039, 3426119,
3431591, 3433191, 3434823, 3448167, 3452007, 3459751, 3460775, 3467623, 3483239, 3488487,
3488935, 3490119, 3492167, 3492583, 3495783, 3511399, 3512231, 3545255, 3555175, 3557447,
3562855, 3564903, 3574247, 3583335, 3586407, 3592679, 3605223, 3638887, 3643559, 3660967,
3667047, 3690151, 3691175, 3696231, 3708775, 3711047, 3721959, 3727207, 3728231, 3745895,
3750567, 3758823, 3767143, 3773255, 3774055, 3795303, 3801415, 3802215, 3803047, 3811559,
3815783, 3816167, 3826535, 3839079, 3842919, 3843943, 3844775, 3856711, 3860807, 3867879,
3868263, 3872935, 3874151, 3890791, 3891367, 3902311, 3933543, 3940199, 3942471, 3960903,
3968359, 3973447, 3979943, 3989863, 3990887, 3999207, 4010151, 4018023, 4025703, 4027751,
4046183, 4055911, 4080871, 4090183, 4093031, 4127047, 4127847, 4130535, 4133735, 4150375,
4161127, 4179783, 4182183, 4184391, 4186855, 4187879, 4190055, 4191079, 4193127, 4199783,
4205671, 4212199, 4219047, 4220263, 4221287, 4222119, 4229031, 4229607, 4236103, 4244199,
4245607, 4247399, 4254951, 4268135, 4274791, 4278439, 4281511, 4287335, 4294247, 4297895,
4299495, 4317543, 4322407, 4329127, 4337831, 4338855, 4339431, 4351591, 4354215, 4361959,
4367431, 4380775, 4405095, 4416231, 4418663, 4442599, 4449095, 4451495, 4458407, 4495271,
4498759, 4501991, 4512103, 4518375, 4530919, 4533351, 4538215, 4547943, 4548967, 4555079,
4556103, 4564583, 4577127, 4580423, 4595559, 4595815, 4596583, 4597831, 4606311, 4612423,
4623175, 4627815, 4628839, 4634471, 4644007, 4652903, 4653927, 4655975, 4658407, 4667719,
4671591, 4684967, 4685159, 4686567, 4702375, 4704999, 4707655, 4713319, 4730183, 4742311,
4765415, 4784455, 4803303, 4808551, 4810823, 4820135, 4826983, 4828007, 4843623, 4857191,
4863911, 4867559, 4867943, 4870215, 4883559, 4886599, 4897127, 4899143, 4923239, 4931175,
4946791, 4953447, 4962983, 4967079, 4971879, 4975335, 4977383, 4990567, 4993191, 4999271,
5026631, 5032295, 5051559, 5054791, 5056615, 5061287, 5073223, 5074023, 5080551, 5084391,
5084775, 5098407, 5110503, 5110951, 5112551, 5112935, 5122279, 5127527, 5133639, 5134439,
5136871, 5144167, 5155687, 5162599, 5167271, 5171527, 5176167, 5186919, 5205159, 5228263,
5228647, 5233319, 5234535, 5235783, 5238439, 5244263, 5251175, 5261479, 5262695, 5263527
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.