New Syracuse step-14 certificate classes, chunk 1
DefinitionsyracuseSevenMod32New26Step14Chunk01Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 1 of 5 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 678 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 syracuseSevenMod32New26Step14Chunk01Classes : Finset ℕ := {
36583, 113767, 144199, 207591, 213863, 230503, 254439, 273255, 288071, 296167, 313831, 316231,
329575, 332647, 371175, 376423, 404807, 427495, 437415, 440039, 460903, 465575, 470247, 496807,
538535, 557799, 560999, 575815, 576615, 610471, 620391, 622663, 664391, 679783, 682055, 717287,
725159, 739399, 759015, 773031, 774631, 787175, 795719, 808263, 815783, 837223, 838471, 868455,
873127, 909159, 926023, 939367, 961255, 998759, 1075367, 1083239, 1085511, 1098855, 1127239,
1130087, 1136359, 1142855, 1155399, 1219239, 1228135, 1237479, 1247399, 1256295, 1258343,
1271911, 1308391, 1329479, 1359463, 1481447, 1504583, 1511079, 1567399, 1590887, 1605703,
1636711, 1656551, 1676615, 1684711, 1693031, 1694055, 1710247, 1721191, 1736807, 1750375,
1768039, 1774311, 1793127, 1825383, 1825959, 1830631, 1849671, 1868135, 1886951, 1893223,
1918183, 1922407, 1988519, 2008935, 2024775, 2052935, 2055783, 2058407, 2119399, 2142535,
2144935, 2176167, 2197607, 2198855, 2232487, 2233511, 2241383, 2255175, 2271591, 2286407,
2289831, 2299751, 2313319, 2435751, 2453991, 2459239, 2487399, 2487623, 2490471, 2510759,
2567079, 2579623, 2616679, 2618727, 2623399, 2626023, 2631143, 2640615, 2687463, 2697959,
2719847, 2757351, 2812647, 2822215, 2867367, 2898599, 2914215, 2926759, 2927783, 2937703,
2951271, 2955943, 2994247, 2997095, 2999367, 3008839, 3045095, 3053415, 3054439, 3055687,
3066183, 3070631, 3109735, 3110759, 3125575, 3133095, 3134695, 3148263, 3158183, 3180871,
3189415, 3217575, 3241063, 3278567, 3282791, 3306727, 3312999, 3362471, 3372391, 3377063,
3400551, 3413319, 3416167, 3418791, 3456871, 3472487, 3493799, 3502919, 3505319, 3516487,
3566311, 3589223, 3601767, 3613159, 3621031, 3631975, 3646791, 3674951, 3688295, 3745639,
3769575, 3796135, 3819623, 3824295, 3857127, 3897255, 3916519, 3920743, 3934535, 3950951,
3979111, 3981383, 3992679, 4115111, 4117735, 4137799, 4138599, 4166759, 4225351, 4231847,
4258983, 4284743, 4296039, 4316327, 4357479, 4373095, 4377319, 4429415, 4431015, 4441959,
4455527, 4457575, 4466919, 4471143, 4485959, 4488807, 4495079, 4499303, 4546151, 4546727,
4549799, 4551399, 4588903, 4593575, 4596199, 4635303, 4645223, 4654567, 4667111, 4673383,
4732775, 4745543, 4765607, 4779175, 4835143, 4837543, 4840167, 4846439, 4861031, 4863303,
4896935, 4918375, 4919623, 4920423, 4949607, 4954279, 4962151, 4964423, 4977767, 4986087,
5022791, 5035335, 5064295, 5071591, 5092455, 5113767, 5129959, 5137255, 5184679, 5193575,
5208391, 5211239, 5276903, 5281127, 5287847, 5311335, 5351911, 5354311, 5356135, 5367655,
5398887, 5439815, 5440615, 5464551, 5475495, 5478119, 5498183, 5498983, 5512551, 5576615,
5591207, 5592231, 5645127, 5648551, 5656423, 5708519, 5720135, 5755367, 5765863, 5789799,
5812711, 5820583, 5831527, 5832775, 5846119, 5846343, 5849191, 5853863, 5906535, 5939943,
5975399, 5984743, 5995687, 5999335, 6076743, 6083239, 6123591, 6134087, 6136935, 6171367,
6178663, 6180935, 6226087, 6257319, 6283431, 6293351, 6296423, 6308167, 6309991, 6346471,
6352967, 6367559, 6380903, 6424679, 6429351, 6468455, 6491815, 6502311, 6516903, 6524775,
6539591, 6548135, 6549159, 6571623, 6597735, 6605479, 6628967, 6634215, 6637287, 6641511,
6657127, 6671719, 6674791, 6714695, 6731111, 6735783, 6750951, 6806119, 6831207, 6872935,
6956263, 6979751, 6988647, 7002439, 7005511, 7013607, 7037095, 7047015, 7093863, 7119175,
7135591, 7144935, 7187687, 7191911, 7211175, 7214247, 7270567, 7279463, 7309671, 7324487,
7335783, 7351399, 7365991, 7375335, 7381831, 7387879, 7434727, 7443623, 7445223, 7497319,
7499943, 7513159, 7555911, 7617703, 7656807, 7664103, 7676647, 7678695, 7731815, 7741287,
7743559, 7756103, 7788135, 7789735, 7798631, 7802951, 7813447, 7825639, 7850727, 7905447,
7908519, 7932007, 7936679, 7952295, 7965863, 7972711, 7989351, 8013287, 8032327, 8035175,
8044871, 8046919, 8076903, 8091495, 8108711, 8117607, 8119655, 8124327, 8147815, 8193863,
8218951, 8219751, 8279143, 8312999, 8316647, 8373991, 8381511, 8430311, 8451175, 8454247,
8510567, 8548071, 8569959, 8587175, 8627303, 8639847, 8651239, 8668007, 8670055, 8684871,
8698215, 8714855, 8716455, 8742215, 8757607, 8798535, 8831143, 8857703, 8871271, 8890535,
8916295, 8935335, 9017191, 9019463, 9067239, 9145447, 9148519, 9153191, 9176679, 9179303,
9212583, 9269927, 9270503, 9284519, 9297063, 9298663, 9326247, 9336167, 9358055, 9415399,
9435463, 9437287, 9469095, 9477991, 9480039, 9508199, 9526887, 9583207, 9584807, 9616039,
9634279, 9638727, 9652071, 9666887, 9673383, 9726279, 9739623, 9783623, 9803687, 9856359,
9865703, 9930343, 9935015, 9958503, 9987687, 10000231, 10002503, 10058599, 10086759, 10094503,
10117991, 10130535, 10136231, 10159719, 10164391, 10231655, 10233927, 10319207, 10347367,
10372327, 10452583, 10503655, 10510503, 10513575, 10537063, 10546407, 10569895, 10572967,
10608999, 10629287, 10630311, 10630887, 10696551, 10710119, 10734055, 10740551, 10793447,
10824807, 10840423, 10856039, 10868583, 10871879, 10887271, 10914631, 10949863, 10976423,
10978023, 10999111, 11033767, 11094759, 11100007, 11102279, 11159399, 11161671, 11175015,
11188583, 11244903, 11266791, 11268839, 11290727, 11318087, 11346247, 11348071, 11352743,
11372007, 11418983, 11428327, 11435623, 11447143, 11462983, 11478375, 11496615, 11520103,
11524775, 11529895, 11552935, 11554983, 11586215, 11609703, 11635015, 11637063, 11637863,
11679591, 11695207, 11732711, 11740231, 11773863, 11789031, 11796551, 11812967, 11831207,
11839079, 11869287, 11903719, 11906791, 11948519, 11994343, 12005287, 12017831, 12025703,
12047015, 12056935, 12100935, 12116327, 12125671, 12157255, 12158055, 12189863, 12200807,
12216423, 12223719, 12229991, 12271943, 12275015, 12303975, 12310247, 12316743, 12332135,
12344679, 12355047, 12362567, 12432231, 12493895, 12511911, 12538023, 12548967, 12591943,
12597991, 12605287, 12629223, 12643239, 12678471, 12694887, 12713127, 12723271, 12769895,
12796007, 12816871, 12826215, 12863719, 12866919, 12885159, 12895079, 12896103, 12946599,
12966215, 12970087, 12997447, 13051367, 13185095, 13199463, 13224423, 13231943, 13234343,
13257831, 13293735, 13329767, 13351079, 13351655, 13354727, 13374567, 13406375, 13407399,
13411047, 13417319, 13419591, 13445479, 13468391, 13494951
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.