New Syracuse step-13 certificate classes, chunk 2
DefinitionsyracuseSevenMod32New26Step13Chunk02Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 2 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 syracuseSevenMod32New26Step13Chunk02Classes : Finset ℕ := {
32986983, 33001799, 33048647, 33074535, 33083879, 33104967, 33182375, 33234023, 33271527,
33370023, 33393511, 33452103, 33581159, 33606119, 33624935, 33639751, 33789095, 33820327,
33845415, 33850087, 33871975, 33972071, 33974343, 33993959, 34003303, 34007975, 34009575,
34022119, 34087783, 34190951, 34218311, 34228455, 34291047, 34350439, 34362183, 34377799,
34390343, 34422375, 34463079, 34542759, 34596679, 34622567, 34645927, 34753895, 34763239,
34913383, 34928999, 34985319, 35013479, 35060327, 35131463, 35269863, 35280807, 35293351,
35354343, 35363687, 35457511, 35524775, 35551335, 35638087, 35722567, 35782759, 35823463,
35825735, 35923431, 35979751, 35992295, 36289383, 36291655, 36301927, 36345703, 36347975,
36360519, 36425383, 36481703, 36505191, 36509863, 36541095, 36592743, 36630247, 36664679,
36667751, 36692839, 36728743, 36780391, 36949223, 36972711, 36998471, 37071207, 37155687,
37208807, 37263527, 37317447, 37352679, 37366695, 37380839, 37446503, 37502823, 37577031,
37649767, 37720903, 37749063, 37781095, 37821799, 37842087, 37865575, 37898407, 37901479,
38025063, 38121959, 38140775, 38184551, 38309607, 38365927, 38431591, 38490183, 38503527,
38569191, 38623911, 38644199, 38677831, 38700519, 38713063, 38734151, 38750567, 38811559,
38858407, 38883495, 38937415, 39012423, 39032039, 39046055, 39047655, 39060199, 39068743,
39081287, 39141479, 39146151, 39182183, 39229031, 39266535, 39322855, 39351015, 39388519,
39400263, 39415879, 39428423, 39501159, 39510503, 39544935, 39634759, 39691079, 39719239,
39754471, 39784103, 39840423, 39863911, 39878727, 39929575, 39957735, 39967079, 39984295,
40023399, 40087463, 40098407, 40110951, 40122695, 40297799, 40325959, 40331431, 40392423,
40506535, 40514407, 40562855, 40586343, 40589415, 40622247, 40645735, 40683239, 40727015,
40760647, 40899047, 40970983, 41030375, 41051463, 41095239, 41200807, 41224295, 41228967,
41267271, 41318119, 41327463, 41339207, 41383783, 41398599, 41421287, 41471335, 41579175,
41630823, 41635495, 41686343, 41724647, 41766823, 41789511, 41846631, 41862247, 41982631,
41987303, 42010791, 42092871, 42109287, 42170279, 42193767, 42265703, 42355527, 42390759,
42504871, 42587751, 42589351, 42625255, 42650343, 42681575, 42744167, 42758983, 42772327,
42819175, 42869223, 42908327, 42939559, 42993479, 43018567, 43049799, 43113191, 43119463,
43222631, 43227303, 43237447, 43250791, 43310183, 43343015, 43344615, 43347687, 43386791,
43404007, 43410279, 43466599, 43469671, 43481415, 43554151, 43629159, 43661991, 43690151,
43712839, 43715911, 43751143, 43772231, 43785575, 43849639, 43865255, 43921575, 43948135,
44004455, 44038887, 44041959, 44070119, 44084135, 44085735, 44104551, 44119367, 44140455,
44179559, 44248423, 44257767, 44268711, 44356263, 44384423, 44407111, 44410183, 44438343,
44451687, 44453959, 44583015, 44625991, 44775335, 44822183, 44878503, 44901991, 44914535,
44930151, 45022375, 45023975, 45145959, 45205351, 45261671, 45286631, 45310119, 45346023,
45392199, 45408615, 45417959, 45430503, 45464935, 45552487, 45608807, 45624423, 45654855,
45660327, 45683815, 45714247, 45716647, 45718247, 45749479, 45786183, 45798727, 45937127,
46068455, 46086471, 46117703, 46162279, 46227943, 46238887, 46262375, 46305351, 46349927,
46436679, 46586023, 46596167, 46647015, 46668903, 46703335, 46706407, 46762727, 46804903,
46900327, 46912871, 46941031, 46987879, 46989479, 47015239, 47020711, 47071559, 47074631,
47109863, 47130951, 47144295, 47208359, 47231847, 47442855, 47452327, 47478087, 47499175,
47542951, 47599271, 47625831, 47663335, 47688423, 47710311, 47719655, 47743143, 47907303,
47946407, 48031559, 48056647, 48087879, 48129383, 48138727, 48151271, 48260711, 48273255,
48275527, 48381095, 48409255, 48437415, 48504679, 48506951, 48519495, 48592231, 48620391,
48645351, 48728231, 48776679, 48883047, 48887719, 48903335, 48911207, 48983143, 48986215,
49013575, 49042535, 49080039, 49144903, 49306791, 49367783, 49427175, 49448263, 49461607,
49517927, 49520999, 49539815, 49621095, 49625767, 49708647, 49736007, 49769639, 49795399,
49797799, 49830631, 49908039, 49952615, 49968231, 50005735, 50062055, 50104231, 50163623,
50198855, 50221543, 50320039, 50346599, 50373959, 50384103, 50407591, 50430279, 50431079,
50496743, 50503015, 50567079, 50589767, 50752327, 50787559, 50811047, 50821991, 50864967,
50878311, 50986151, 51069031, 51155783, 51158183, 51169127, 51497447, 51603815, 51624103,
51647591, 51680423, 51741415, 51744487, 51767975, 51791463, 51819623, 51857127, 51863399,
51865671, 51900903, 51950951, 52025959, 52109639, 52112711, 52126055, 52147943, 52182375,
52225351, 52241767, 52269127, 52466919, 52480935, 52490407, 52516167, 52537255, 52726503,
52820327, 52835143, 52898535, 52904807, 52945383, 52964199, 52984487, 53020519, 53067367,
53094727, 53128359, 53151847, 53156519, 53251943, 53266759, 53311335, 53313607, 53416103,
53462951, 53580263, 53630311, 53683431, 53706919, 53766311, 53789799, 53814759, 53827303,
53948487, 53949287, 54051655, 54180711, 54182983, 54195527, 54208871, 54316711, 54344871,
54401191, 54427751, 54465255, 54516903, 54559079, 54577895, 54584167, 54699879, 54746727,
54833479, 54835879, 54846823, 54946119, 54962535, 54990695, 55006311, 55043815, 55100135,
55126695, 55150183, 55178343, 55201703, 55309671, 55314343, 55412039, 55468359, 55484775,
55541095, 55558311, 55569255, 55605159, 55628647, 55825639, 55849127, 55888231, 56003943,
56107111, 56163431, 56193863, 56196263, 56304103, 56322919, 56366695, 56379239, 56404199,
56460519, 56487079, 56510567, 56535527, 56548071, 56641895, 56670055, 56672327, 56772423,
56806055, 56828743, 56829543, 56857703, 56903751, 56916295, 56929639, 56938983, 57037479,
57064039, 57120359, 57148519, 57157863, 57186023, 57237671, 57248615, 57279847, 57284519,
57307207, 57336167, 57345511, 57364327, 57526087, 57528487, 57551975, 57554247, 57675431,
57713735, 57727079, 57755239, 57820903, 57858407, 57942887, 58002279, 58166439, 58189127,
58189927, 58205543, 58397863, 58480743, 58501031, 58608999, 58618343, 58630887, 58768487,
58827879, 58862311, 58917031, 58986567, 58987367, 58999111, 59071847, 59115623, 59120295,
59124967, 59207847, 59218791, 59230535, 59325159, 59362663, 59493191, 59522151, 59693383,
59784807, 59878631, 60000615, 60056935, 60066279, 60188263, 60246855, 60347751, 60396199,
60422759, 60432231, 60434503, 60447847, 60479079, 60480679, 60485351, 60516583, 60522855,
60541671, 60643239, 60663655, 60704231, 60799655, 60853575, 60884807, 60909895, 60910695,
60926311, 61072455, 61118631, 61142119, 61145191, 61201511, 61221799, 61239015, 61278119,
61301607, 61342183, 61360999, 61389159, 61548647, 61607239, 61708135, 61710407, 61756583,
61836391, 61839463, 61844135, 61867623, 61975463, 61977063, 61989607, 62027111, 62160039,
62221031, 62286695, 62343015, 62345287, 62357831, 62430567, 62479015, 62589255, 62605671,
62713511, 62749543, 62777703, 62821479, 63084135, 63121639, 63143527, 63177959, 63201447,
63204519, 63206119, 63228007, 63237351, 63243623, 63260839, 63299943, 63387495, 63424999,
63489863, 63515751, 63546183, 63546983, 63574343, 63605575, 63668967, 63790951, 63793223,
63839399, 63865959, 63942567, 63959783, 63966055, 64037191, 64062951, 64109927, 64138087,
64245927, 64328007, 64431175, 64444519, 64477351, 64500839, 64503911, 64538343, 64560231,
64594663, 64597735, 64696231, 64716647, 64747879, 64880807, 64906567, 64907367, 64962887,
64965959, 65035623, 65202855, 65320167, 65326439, 65334183, 65385831, 65434279, 65460839,
65485927, 65507815, 65517159, 65554663, 65579751, 65688391, 65701735, 65742311, 65837735,
65842407, 65865895, 65876039, 65922887, 65925287, 65947975, 65948775, 65964391, 66020711,
66108263, 66110535, 66136423, 66210631, 66244263, 66396007, 66442855, 66480359, 66536679,
66563239, 66619559, 66680551, 66746215, 66783719, 66794663, 66848583, 66877543, 66904903,
67027687, 67048775
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.