New Syracuse step-15 certificate classes, chunk 5
DefinitionsyracuseSevenMod32New26Step15Chunk05Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 5 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 syracuseSevenMod32New26Step15Chunk05Classes : Finset ℕ := {
21136231, 21137255, 21150023, 21150439, 21170503, 21177831, 21179623, 21184679, 21186919,
21202535, 21207207, 21210439, 21217351, 21220583, 21230695, 21238599, 21242023, 21244071,
21244263, 21269831, 21273255, 21277927, 21285991, 21290087, 21294759, 21301415, 21311559,
21322919, 21324519, 21327591, 21330791, 21342567, 21353287, 21358951, 21366695, 21380263,
21383495, 21383911, 21387111, 21387943, 21390183, 21399911, 21402727, 21416103, 21427047,
21446503, 21449575, 21456231, 21460903, 21461319, 21467815, 21480167, 21484391, 21498183,
21518663, 21519463, 21525159, 21534055, 21534887, 21543783, 21546055, 21547847, 21552295,
21556327, 21556967, 21571943, 21588807, 21589351, 21609063, 21613287, 21613671, 21624039,
21638055, 21641895, 21646151, 21652199, 21665383, 21666983, 21670055, 21670631, 21679783,
21681383, 21692743, 21695815, 21702887, 21717863, 21727399, 21731047, 21735271, 21752135,
21759207, 21763431, 21764263, 21765479, 21774183, 21782695, 21787367, 21792615, 21822631,
21824871, 21829543, 21831527, 21845159, 21848391, 21849959, 21871271, 21878375, 21881191,
21882215, 21886887, 21901479, 21903079, 21910375, 21915879, 21921127, 21925191, 21928039,
21928615, 21947239, 21956775, 21972199, 21981511, 21984359, 21985383, 21992263, 22001575,
22005607, 22006247, 22017767, 22018791, 22020423, 22021863, 22034791, 22038855, 22041703,
22049607, 22050023, 22052455, 22064039, 22065639, 22071111, 22079207, 22084455, 22093159,
22096999, 22099271, 22111591, 22112615, 22113447, 22115047, 22120295, 22120359, 22127431,
22136935, 22140775, 22155591, 22159463, 22159847, 22169767, 22172839, 22189223, 22190247,
22213735, 22222055, 22228327, 22230183, 22230759, 22237671, 22248615, 22250215, 22271303,
22284103, 22284455, 22293415, 22296423, 22328423, 22329255, 22336167, 22340423, 22345447,
22349735, 22364327, 22372199, 22373223, 22374471, 22385991, 22387015, 22390087, 22393319,
22403815, 22409703, 22410087, 22412135, 22418247, 22420647, 22426343, 22431591, 22433863,
22447431, 22455911, 22460583, 22463207, 22483271, 22484071, 22486887, 22502503, 22520167,
22523815, 22528071, 22540007, 22547303, 22549735, 22562919, 22580967, 22590279, 22598983,
22600807, 22603623, 22604647, 22605895, 22613351, 22618439, 22627559, 22633639, 22635239,
22637287, 22638311, 22691175, 22694631, 22700519, 22702951, 22713671, 22719335, 22748327,
22750567, 22755239, 22757223, 22760295, 22761543, 22772039, 22772839, 22774887, 22777927,
22794567, 22802087, 22828199, 22829799, 22831431, 22840551, 22844775, 22851495, 22858407,
22881895, 22885543, 22894439, 22895271, 22904167, 22908007, 22908231, 22910055, 22915559,
22917959, 22919783, 22921383, 22923623, 22931303, 22932327, 22944487, 22949191, 22952615,
22962535, 22971879, 22978727, 22980775, 22984423, 22995783, 23002279, 23003463, 23003879,
23005511, 23006535, 23021927, 23025767, 23028199, 23041767, 23046055, 23048679, 23058599,
23062855, 23068743, 23076199, 23082087, 23082919, 23119591, 23123815, 23125863, 23129767,
23140263, 23154855, 23162791, 23175911, 23185255, 23198023, 23208775, 23231655, 23238759,
23241575, 23251303, 23266535, 23268711, 23272167, 23276455, 23283783, 23288999, 23290023,
23292647, 23295079, 23297895, 23298919, 23303399, 23312711, 23317415, 23319015, 23325927,
23329127, 23329511, 23331559, 23332583, 23340103, 23345767, 23349991, 23352647, 23360743,
23372103, 23374759, 23383271, 23388519, 23395175, 23396423, 23397863, 23402087, 23406759,
23409767, 23409991, 23410407, 23412839, 23413607, 23414631, 23416903, 23417511, 23428199,
23431079, 23439591, 23444839, 23453543, 23462055, 23472999, 23475431, 23487815, 23500391,
23529319, 23532391, 23537895, 23539047, 23544135, 23548391, 23550631, 23562983, 23566247,
23576167, 23578791, 23582439, 23588711, 23594215, 23604327, 23607975, 23616871, 23622375,
23634759, 23636135, 23640231, 23640391, 23646887, 23659879, 23660871, 23663719, 23671623,
23675047, 23687239, 23694151, 23696551, 23697735, 23698151, 23699783, 23700807, 23704423,
23718215, 23728967, 23729383, 23729767, 23751495, 23760743, 23766087, 23767271, 23772519,
23778631, 23781863, 23785127, 23786727, 23807815, 23816295, 23819111, 23820967, 23823591,
23843655, 23849319, 23893095, 23898599, 23906119, 23907687, 23910119, 23916615, 23917031,
23924903, 23931207, 23950439, 23950663, 23962439, 23963815, 23965031, 23973735, 23987943,
23990599, 24015527, 24016103, 24025831, 24032103, 24048359, 24055463, 24065959, 24066375,
24067175, 24086439, 24089063, 24097607, 24104039, 24111783, 24135271, 24135495, 24139111,
24142183, 24146791, 24150087, 24154951, 24160999, 24166247, 24167271, 24191815, 24200935,
24205159, 24207847, 24218791, 24229095, 24238439, 24242279, 24249575, 24255655, 24266823,
24273063, 24275687, 24277735, 24278343, 24281959, 24282983, 24284007, 24285255, 24292711,
24294759, 24299431, 24302055, 24312999, 24314599, 24323559, 24329831, 24330407, 24343783,
24356167, 24358823, 24369767, 24371559, 24382311, 24384327, 24387751, 24394055, 24400551,
24416583, 24418983, 24423655, 24436583, 24447143, 24457287, 24493927, 24495975, 24519911,
24529223, 24533671, 24543399, 24545639, 24552295, 24561831, 24565927, 24569159, 24576071,
24581479, 24587367, 24597319, 24601959, 24602791, 24602983, 24610663, 24611687, 24617799,
24623847, 24626919, 24629095, 24636647, 24643911, 24645959, 24648807, 24658087, 24663783,
24670279, 24678567, 24682823, 24683239, 24686311, 24689511, 24691783, 24712007, 24717671,
24721127, 24742631, 24743655, 24755559, 24762471, 24774823, 24777895, 24784807, 24785767,
24791879, 24825511, 24834215, 24835815, 24843111, 24857703, 24860775, 24880231, 24888135,
24892775, 24893607, 24899431, 24909991, 24911015, 24917095, 24920935, 24936551, 24950951,
24951527, 24954599, 24967783, 24968359, 24969383, 24974439, 24977255, 24978279, 24992071,
24995143, 24998375, 25000615, 25004871, 25007271, 25008871, 25014183, 25024103, 25032007,
25038503, 25040103, 25051463, 25054535, 25061607, 25067879, 25089351, 25089767, 25090151,
25092967, 25110855, 25111879, 25117927, 25118311, 25124199, 25141415, 25147111, 25150311,
25151335, 25170407, 25181351, 25183975, 25188263, 25204039, 25209703, 25211751, 25221479,
25227751, 25240935, 25242343, 25260775, 25301735, 25305959, 25319751, 25322823, 25359079,
25360295, 25366599, 25375911, 25376487, 25377095, 25383783, 25408327, 25422759, 25429831,
25432231, 25452903, 25457991, 25466087, 25469095, 25471335, 25472167, 25474983, 25479079,
25480103, 25486151, 25495655, 25497447, 25499495, 25500327, 25515335, 25518567, 25522855,
25536423, 25538631, 25548967, 25552199, 25572455, 25579175, 25589479, 25595975, 25598823,
25605735, 25606311, 25608935, 25609959, 25610567, 25628999, 25629799, 25635495, 25638119,
25640551, 25643239, 25644391, 25655143, 25661607, 25666279, 25668327, 25669959, 25683303,
25687975, 25690215, 25692647, 25695463, 25699559, 25704167, 25711463, 25723047, 25727303,
25742695, 25744711, 25746535, 25759079, 25760935, 25779367, 25784039, 25788263, 25802663,
25803879, 25818471, 25834311, 25840359, 25842791, 25850535, 25880295, 25886791, 25887207,
25894055, 25902183, 25906023, 25906855, 25918567, 25926311, 25941863, 25944551, 25952423,
25957703, 25959527, 25963367, 25972071, 25977159, 25978183, 25981415, 25996007, 25997031,
25997223, 26006343, 26011463, 26023143, 26034503, 26036551, 26038183, 26049895, 26053351,
26060871, 26063687, 26066535, 26067111, 26067783, 26072391, 26077031, 26078055, 26095527,
26098343, 26107239, 26108263, 26109287, 26117991, 26118631, 26126503, 26131175
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.