New Syracuse step-15 certificate classes, chunk 6
DefinitionsyracuseSevenMod32New26Step15Chunk06Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 6 of 13 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 745 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 syracuseSevenMod32New26Step15Chunk06Classes : Finset ℕ := {
26131559, 26133607, 26152263, 26153447, 26160359, 26173927, 26203495, 26208583, 26225383,
26231655, 26240615, 26248519, 26253159, 26253991, 26255431, 26258663, 26266727, 26278503,
26282151, 26303207, 26311335, 26312775, 26321255, 26349639, 26360999, 26364231, 26365255,
26380647, 26384487, 26389159, 26391367, 26397031, 26400487, 26404711, 26417319, 26417895,
26421575, 26440807, 26441639, 26454183, 26465127, 26478311, 26478695, 26483367, 26484583,
26486855, 26488039, 26498983, 26499399, 26501607, 26505895, 26506471, 26512743, 26520487,
26521671, 26522471, 26528583, 26537063, 26542151, 26555495, 26570087, 26572135, 26576807,
26581863, 26593607, 26600295, 26621159, 26625255, 26626887, 26629479, 26630887, 26637159,
26651367, 26662119, 26671431, 26672231, 26688231, 26708135, 26708711, 26733479, 26742951,
26744167, 26745575, 26756583, 26765479, 26768711, 26773351, 26776231, 26786119, 26789799,
26819175, 26820775, 26826471, 26831719, 26834151, 26846535, 26856263, 26859111, 26860711,
26862951, 26867623, 26869831, 26874695, 26875495, 26883239, 26889895, 26891111, 26896615,
26907111, 26909351, 26912999, 26916455, 26921703, 26937511, 26948455, 26952935, 26953959,
26963047, 26966119, 26966695, 26969319, 26984295, 26989383, 26993479, 26995879, 26998503,
26999111, 27000935, 27010279, 27015527, 27019591, 27022439, 27030343, 27033767, 27039655,
27043687, 27044327, 27055847, 27056455, 27059943, 27071847, 27076935, 27090535, 27092327,
27113799, 27119463, 27124807, 27140583, 27146855, 27148455, 27150695, 27177831, 27178855,
27179687, 27194695, 27197927, 27202375, 27210919, 27249767, 27264839, 27275335, 27281223,
27286695, 27289927, 27321159, 27322183, 27337543, 27347687, 27366727, 27367335, 27378503,
27383527, 27384551, 27390823, 27407079, 27412551, 27424071, 27426919, 27428167, 27438439,
27441511, 27441895, 27445159, 27447783, 27458727, 27464423, 27467623, 27483239, 27493991,
27497831, 27498663, 27500903, 27505511, 27508807, 27519719, 27520743, 27522151, 27535719,
27546279, 27558247, 27562471, 27563879, 27566151, 27581543, 27600999, 27605671, 27608295,
27614375, 27615975, 27619047, 27629159, 27641703, 27657319, 27658151, 27665639, 27666663,
27671719, 27675367, 27681639, 27688551, 27689127, 27699879, 27715911, 27728039, 27737959,
27741031, 27749543, 27751751, 27752775, 27756391, 27757415, 27759271, 27775303, 27777703,
27782375, 27788647, 27810119, 27810535, 27810919, 27816007, 27825511, 27832647, 27843751,
27848423, 27866279, 27866855, 27873127, 27882855, 27887943, 27888967, 27900519, 27904743,
27911015, 27920551, 27930695, 27932519, 27933351, 27948135, 27961511, 27961703, 27968359,
27976519, 27981543, 27984199, 27985639, 27987271, 27989863, 28018855, 28022503, 28026727,
28033863, 28034887, 28037287, 28041959, 28043591, 28056935, 28076391, 28084135, 28096679,
28097255, 28104551, 28120167, 28120999, 28125863, 28136615, 28143527, 28150599, 28162727,
28173671, 28178343, 28178759, 28184231, 28185831, 28191079, 28192935, 28194535, 28200871,
28201447, 28201831, 28216647, 28219495, 28235079, 28235879, 28249447, 28257191, 28264039,
28269735, 28272967, 28275815, 28276839, 28293031, 28299943, 28308839, 28310247, 28313319,
28315495, 28326503, 28327079, 28329703, 28330727, 28333159, 28341479, 28349767, 28353863,
28355495, 28357095, 28364007, 28367207, 28370663, 28375911, 28387495, 28390727, 28404071,
28408935, 28410183, 28410983, 28411815, 28424935, 28432231, 28450919, 28451687, 28465479,
28476647, 28479655, 28481703, 28482919, 28504807, 28505191, 28511079, 28513511, 28519783,
28529127, 28540071, 28546983, 28554055, 28562759, 28569671, 28584871, 28588711, 28598631,
28604327, 28614823, 28616871, 28627623, 28627815, 28641191, 28655783, 28664295, 28664679,
28678471, 28681543, 28697927, 28698951, 28709703, 28717799, 28723047, 28725319, 28732231,
28738887, 28767463, 28790951, 28793159, 28799847, 28801895, 28808551, 28811623, 28824807,
28829031, 28830439, 28833703, 28844871, 28854375, 28857191, 28858215, 28873031, 28881735,
28895079, 28896103, 28897351, 28906663, 28931175, 28942503, 28966055, 28968679, 28988519,
28989543, 28991975, 28996839, 28999271, 29003111, 29017703, 29026023, 29032519, 29042023,
29046695, 29048935, 29060263, 29067175, 29086023, 29088423, 29093543, 29105255, 29117799,
29119655, 29121255, 29127143, 29135687, 29138087, 29142759, 29146983, 29149031, 29149863,
29161383, 29162599, 29173351, 29184871, 29185895, 29193031, 29198663, 29199079, 29199463,
29201511, 29215079, 29235943, 29241255, 29243239, 29256423, 29277287, 29293287, 29293735,
29295335, 29303271, 29311143, 29322087, 29336903, 29337511, 29340135, 29360199, 29365063,
29371111, 29394247, 29417319, 29436775, 29454247, 29457063, 29466983, 29476711, 29477351,
29486247, 29489479, 29495367, 29502823, 29510983, 29512167, 29514407, 29523111, 29533031,
29539943, 29546215, 29547239, 29551463, 29557991, 29567303, 29581479, 29583719, 29584103,
29590375, 29599911, 29604007, 29604167, 29609831, 29610663, 29617383, 29624423, 29624647,
29627495, 29629095, 29633767, 29637223, 29641063, 29660327, 29661511, 29663559, 29668199,
29669223, 29671495, 29674727, 29679975, 29689319, 29693543, 29698215, 29701863, 29706087,
29708359, 29716647, 29721319, 29721703, 29724391, 29727591, 29731047, 29736295, 29739335,
29747879, 29764455, 29771367, 29776615, 29782887, 29787367, 29799527, 29823847, 29833959,
29837031, 29842087, 29843303, 29845575, 29857703, 29867623, 29870247, 29870439, 29871463,
29873895, 29879207, 29880167, 29880391, 29880807, 29895783, 29914439, 29915463, 29926215,
29930855, 29931687, 29935527, 29949095, 29952327, 29955175, 29979879, 29985607, 29988007,
29989607, 29995879, 30000743, 30001991, 30005863, 30020839, 30030951, 30042951, 30052839,
30057543, 30062183, 30063207, 30070087, 30076583, 30078183, 30089543, 30092615, 30099271,
30099687, 30101671, 30102887, 30104295, 30105959, 30119527, 30127847, 30130023, 30131047,
30132071, 30140775, 30144839, 30147687, 30155591, 30156007, 30157031, 30162279, 30168935,
30179495, 30184551, 30185191, 30202183, 30205255, 30208487, 30217575, 30221671, 30241511,
30242119, 30245735, 30249031, 30256487, 30279015, 30283687, 30292583, 30294183, 30339815,
30348103, 30348903, 30357223, 30357831, 30359655, 30363495, 30371175, 30378087, 30386407,
30387431, 30389063, 30421063, 30430567, 30433639, 30446407, 30446823, 30448807, 30455719,
30458727, 30460839, 30467911, 30470311, 30472519, 30496071, 30499303, 30509415, 30510247,
30513063, 30516071, 30517159, 30524231, 30525255, 30525607, 30527655, 30533735, 30541031,
30545255, 30553415, 30564519, 30569191, 30575463, 30576711, 30587047, 30587623, 30609735,
30610535, 30620263, 30621287, 30642343, 30663015, 30676199, 30681447, 30706407, 30708039,
30725447, 30754631, 30755655, 30797159, 30800231, 30815047, 30817447, 30840743, 30857383,
30863207, 30867527, 30874791, 30878439, 30878823, 30884711, 30894439, 30900327, 30904999,
30909255, 30911847, 30915303, 30918375, 30925287, 30937415, 30940263, 30944103, 30955847,
30956647, 30964391, 30970023, 30971047, 30974695, 30977767, 30977959, 30987879, 30989479,
30994151, 31000423, 31001447, 31025383, 31034087, 31035111, 31044423, 31047271, 31050471,
31053927, 31057767, 31058599, 31074631, 31076263, 31082087, 31088999, 31108263, 31110247,
31131751, 31136423, 31147751, 31154663, 31164583, 31171687, 31172455, 31184231, 31191527,
31202471, 31212391, 31228007, 31230823, 31231847, 31241575, 31246663, 31259239, 31260839,
31269735, 31283527, 31286599, 31291239, 31292071, 31293511, 31305639
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.