New Syracuse step-13 certificate classes, chunk 1
DefinitionsyracuseSevenMod32New26Step13Chunk01Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 1 of 2 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 785 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 syracuseSevenMod32New26Step13Chunk01Classes : Finset ℕ := {
43079, 56423, 68967, 89255, 93927, 115815, 150247, 209639, 215911, 228455, 287047, 359783,
387943, 408231, 436391, 462151, 518471, 519271, 577863, 694375, 706919, 750695, 788199, 816359,
830375, 886695, 946087, 997735, 1072743, 1130663, 1156423, 1166567, 1184583, 1185383, 1190055,
1222887, 1354215, 1373031, 1429351, 1476199, 1534791, 1570023, 1591111, 1598183, 1720167,
1722439, 1748327, 1757671, 1768615, 1856167, 1938247, 1951591, 1966407, 2039143, 2067303,
2092263, 2125895, 2175143, 2176743, 2358119, 2406567, 2430055, 2433127, 2460487, 2494119,
2495719, 2526951, 2544967, 2545767, 2677095, 2761575, 2814695, 2836583, 2863943, 2895175,
2908519, 2930407, 2974183, 3028903, 3132071, 3155559, 3182919, 3216551, 3249383, 3263399,
3277543, 3298631, 3342407, 3399527, 3415143, 3427687, 3437031, 3452647, 3508967, 3551143,
3587175, 3617607, 3645767, 3671527, 3718503, 3727847, 3766951, 3805255, 3820871, 3856103,
3877191, 3943655, 3971815, 3978087, 4037479, 4039751, 4096071, 4189095, 4224327, 4245415,
4311879, 4340039, 4362727, 4372071, 4409575, 4465895, 4489383, 4492455, 4515943, 4548775,
4609767, 4730951, 4731751, 4777799, 4834119, 4897511, 4977991, 4991335, 5127335, 5153895,
5214887, 5247719, 5265735, 5266535, 5304039, 5474471, 5615943, 5629287, 5633959, 5657447,
5672263, 5732455, 5788775, 5826279, 5852839, 5937319, 5984167, 6040487, 6120295, 6173415,
6194503, 6267239, 6351719, 6387623, 6392295, 6411111, 6514279, 6541639, 6575271, 6576871,
6608103, 6670695, 6760519, 6795751, 6909863, 6945095, 6976327, 7030247, 7039719, 7045991,
7086567, 7092839, 7130343, 7149159, 7153831, 7163975, 7186663, 7236711, 7297703, 7313319,
7325863, 7330535, 7398471, 7407943, 7454791, 7498567, 7532199, 7533799, 7554887, 7698759,
7712103, 7715175, 7771495, 7846503, 7874663, 7902023, 7968487, 7996647, 8024807, 8031079,
8066983, 8315623, 8336711, 8350055, 8364871, 8393031, 8475111, 8490727, 8509543, 8573607,
8658087, 8683847, 8725351, 8756583, 8761255, 8843335, 8858951, 8894183, 8988007, 9075559,
9131879, 9213159, 9227175, 9262407, 9283495, 9296039, 9319527, 9357031, 9385191, 9391463,
9550951, 9581383, 9691623, 9710439, 9725255, 9751015, 9753415, 9769831, 9813607, 9907431,
9933991, 9994983, 10013799, 10059847, 10116967, 10119239, 10154471, 10252967, 10275655, 10363207,
10376551, 10398439, 10435943, 10512551, 10520423, 10522695, 10567271, 10573543, 10656423,
10684583, 10695527, 10745575, 10766663, 10941767, 11073895, 11113799, 11130215, 11158375,
11173991, 11205223, 11211495, 11230311, 11267815, 11305319, 11355367, 11425703, 11579719,
11613351, 11636039, 11669671, 11708775, 11723591, 11736935, 11872935, 11927655, 11947943,
12004263, 12016807, 12055911, 12068327, 12077799, 12124647, 12335783, 12351399, 12363943,
12374887, 12434279, 12436551, 12446023, 12490599, 12492871, 12546919, 12570279, 12571879,
12626599, 12654759, 12678247, 12715751, 12743911, 12750183, 12809575, 12814247, 12837735,
12894055, 12909671, 12940103, 13003495, 13050343, 13058215, 13069159, 13083975, 13112135,
13233319, 13261479, 13294311, 13353703, 13371719, 13388135, 13416295, 13418567, 13662535,
13696167, 13721927, 13794663, 13810279, 13866599, 13879143, 13894759, 13904103, 13925991,
13932263, 13986983, 13988583, 14026087, 14030759, 14104295, 14110567, 14169959, 14202791,
14272327, 14274727, 14300487, 14334119, 14356807, 14357607, 14423271, 14472519, 14621863,
14648423, 14714087, 14725031, 14748519, 14789095, 14791495, 14804839, 14836071, 14901735,
15028391, 15082311, 15145703, 15157319, 15192551, 15226983, 15269959, 15283303, 15286375,
15291047, 15436519, 15513927, 15560775, 15694503, 15733607, 15783655, 15804743, 15905639,
15928999, 15954087, 15985319, 16008807, 16074471, 16108903, 16111975, 16151879, 16168295,
16172967, 16243303, 16268391, 16393447, 16416935, 16442695, 16484199, 16531047, 16624871,
16648359, 16651431, 16707751, 16746855, 16761671, 16825063, 16871911, 16993095, 17054887,
17093991, 17115879, 17168999, 17193287, 17225319, 17240135, 17262823, 17342631, 17345703,
17369191, 17373863, 17389479, 17472359, 17484103, 17528679, 17556839, 17561511, 17584999,
17631047, 17716327, 17753831, 17891431, 17947751, 17985255, 18007143, 18088423, 18107239,
18122055, 18194791, 18327719, 18353479, 18454375, 18456647, 18504423, 18585703, 18590375,
18613863, 18649767, 18707687, 18721703, 18734247, 18773351, 18795239, 18872647, 18917223,
18945383, 18964071, 19020391, 19021991, 19053223, 19075911, 19163463, 19240871, 19367527,
19372199, 19395687, 19531687, 19555175, 19889767, 19950759, 19974247, 19983591, 20007079,
20010151, 20066471, 20068071, 20133735, 20230631, 20277607, 20293223, 20305767, 20324455,
20351815, 20387047, 20413607, 20436295, 20596583, 20598855, 20612199, 20706023, 20727911,
20755271, 20809191, 20865511, 20915559, 20967079, 20992167, 21023399, 21046887, 21074247,
21075047, 21177415, 21211047, 21233735, 21250151, 21306471, 21343975, 21431527, 21442471,
21455015, 21553511, 21562855, 21637991, 21653607, 21712199, 21741159, 21747431, 21769319,
21799751, 21869415, 21931079, 21949095, 22066407, 22080423, 22115655, 22132071, 22207079,
22263399, 22300903, 22304103, 22332263, 22383783, 22407271, 22434631, 22669127, 22671527,
22695015, 22730919, 22788839, 22791911, 22843559, 22848231, 23045223, 23101543, 23134375,
23157063, 23160135, 23216455, 23232871, 23289191, 23309479, 23365799, 23426791, 23492455,
23525287, 23529959, 23548775, 23623783, 23636327, 23664487, 23687847, 23795015, 23800487,
23833319, 23898183, 23970919, 23983463, 24064743, 24091303, 24201543, 24274279, 24283623,
24374375, 24405607, 24432967, 24468199, 24649575, 24651847, 24677735, 24790247, 24801191,
24836423, 24837223, 24852839, 24921575, 24927847, 24984167, 24996711, 25021671, 25045159,
25048231, 25128039, 25158471, 25160871, 25204647, 25228135, 25289799, 25315687, 25331303,
25343847, 25389895, 25425127, 25451687, 25453287, 25512679, 25575271, 25606503, 25765991,
25770663, 25793351, 25794151, 25821511, 25822311, 25831655, 25880903, 25894247, 25953639,
26030247, 26038119, 26113127, 26150631, 26199879, 26202279, 26206951, 26213223, 26241383,
26249127, 26288231, 26382055, 26518855, 26575175, 26647911, 26676071, 26691687, 26750279,
26785511, 26884007, 26966887, 26987175, 27010663, 27104487, 27118503, 27131047, 27132647,
27153735, 27154535, 27182695, 27254631, 27314023, 27472711, 27500871, 27526631, 27573607,
27582951, 27601767, 27642343, 27704935, 27768999, 27792487, 27826919, 27881639, 27886311,
27894855, 27951175, 28008295, 28010567, 28036455, 28195143, 28195943, 28254535, 28267879,
28270951, 28327271, 28347559, 28371047, 28403879, 28464871, 28543079, 28552423, 28586855,
28674407, 28833095, 28871399, 28920647, 28962151, 28965223, 29008999, 29065319, 29102823,
29129383, 29152871, 29190375, 29239623, 29471047, 29558599, 29607847, 29628263, 29707943,
29725159, 29764263, 29828327, 29839271, 29851815, 29875303, 29912807, 29947239, 29959655,
30034791, 30091111, 30093383, 30196551, 30242727, 30247399, 30266215, 30281031, 30325607,
30327879, 30353767, 30369383, 30461607, 30463207, 30489767, 30513255, 30541415, 30615623,
30641511, 30649255, 30800999, 30831431, 30885351, 30941671, 30991719, 31091815, 31124647,
31151207, 31185639, 31188711, 31245031, 31253575, 31307623, 31309895, 31553863, 31556935,
31570279, 31613255, 31626599, 31629671, 31685991, 31701607, 31714151, 31729767, 31786087,
31823591, 31901799, 31911143, 31922087, 31934631, 32001895, 32033127, 32166055, 32170727,
32191815, 32220775, 32279367, 32330215, 32428711, 32511591, 32538951, 32549095, 32611687,
32628903, 32633575, 32680423, 32698439, 32736743, 32917319, 32930663, 32943207
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.