New Syracuse step-15 certificate classes, chunk 7
DefinitionsyracuseSevenMod32New26Step15Chunk07Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 7 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 syracuseSevenMod32New26Step15Chunk07Classes : Finset ℕ := {
31308455, 31316583, 31319399, 31324071, 31340263, 31342919, 31345991, 31347559, 31359335,
31361127, 31362375, 31381223, 31393607, 31396007, 31398631, 31402311, 31403335, 31415655,
31418695, 31422567, 31432871, 31438567, 31438759, 31442855, 31463271, 31478887, 31479719,
31479911, 31501159, 31503207, 31515975, 31516391, 31522887, 31532391, 31536231, 31549799,
31559751, 31560167, 31577959, 31599271, 31610215, 31627431, 31650919, 31651751, 31659239,
31663335, 31675239, 31686823, 31689447, 31708487, 31709287, 31710311, 31714215, 31723687,
31730599, 31731559, 31746215, 31747815, 31749447, 31757543, 31762791, 31766855, 31769703,
31770535, 31771559, 31780199, 31781031, 31782247, 31786919, 31790951, 31794663, 31806791,
31807207, 31810407, 31814311, 31827879, 31840423, 31863527, 31863911, 31869799, 31870631,
31877479, 31884615, 31897191, 31901415, 31905639, 31925095, 31926119, 31926951, 31928391,
31929191, 31929575, 31934695, 31935847, 31947431, 31957351, 31957735, 31959783, 31981671,
31986535, 31991015, 32014503, 32027463, 32031559, 32036583, 32040807, 32041831, 32057671,
32079719, 32095335, 32109927, 32116039, 32125767, 32137703, 32158567, 32160615, 32162887,
32175431, 32178663, 32187751, 32188775, 32189159, 32195431, 32207015, 32217767, 32231751,
32236007, 32243879, 32254823, 32265383, 32266983, 32269639, 32296615, 32297799, 32302919,
32311143, 32324775, 32325959, 32328007, 32345191, 32348263, 32357991, 32359239, 32360807,
32361831, 32376423, 32381095, 32381671, 32398695, 32400743, 32404807, 32407655, 32410087,
32418983, 32422631, 32425895, 32442471, 32445159, 32447143, 32451815, 32476519, 32483239,
32484263, 32485863, 32496807, 32505927, 32521319, 32532071, 32538983, 32542567, 32543207,
32544615, 32546887, 32557383, 32557799, 32558183, 32564071, 32584935, 32591207, 32594663,
32599975, 32601959, 32604231, 32635207, 32636007, 32646375, 32652455, 32668839, 32669863,
32679783, 32680615, 32706727, 32708775, 32726631, 32729831, 32736103, 32737127, 32749895,
32750695, 32776039, 32778311, 32782951, 32783975, 32790855, 32797351, 32804199, 32813383,
32815783, 32818791, 32820039, 32820455, 32826727, 32839271, 32843943, 32851815, 32854087,
32861543, 32863591, 32876775, 32877799, 32891751, 32901287, 32909159, 32910183, 32911431,
32916711, 32920935, 32926023, 32942439, 32942823, 32953159, 32959655, 32962887, 32963687,
32970599, 32986215, 32987815, 32999591, 32999783, 33003431, 33013351, 33014599, 33015975,
33019623, 33023719, 33035623, 33048039, 33056935, 33064807, 33077991, 33080039, 33080423,
33098055, 33106599, 33107175, 33110631, 33117927, 33123175, 33130087, 33140583, 33141607,
33142631, 33154407, 33158247, 33159079, 33171815, 33174695, 33181607, 33182567, 33188679,
33200807, 33213543, 33222311, 33223911, 33228967, 33237863, 33239911, 33244999, 33246023,
33254503, 33257575, 33284935, 33286503, 33287335, 33289575, 33289959, 33294247, 33307815,
33311047, 33313895, 33330279, 33331111, 33341031, 33346919, 33351399, 33383783, 33387847,
33391943, 33402215, 33416263, 33421927, 33442151, 33446215, 33448263, 33464679, 33470311,
33475399, 33478247, 33486151, 33515751, 33520999, 33538215, 33549159, 33576295, 33578151,
33585063, 33592135, 33595559, 33604455, 33608551, 33621095, 33639143, 33642407, 33658183,
33686759, 33691815, 33698535, 33710247, 33714919, 33718375, 33719623, 33721191, 33732967,
33736807, 33746151, 33755879, 33759079, 33769639, 33774695, 33789287, 33792359, 33805543,
33807527, 33808743, 33809767, 33811175, 33812199, 33814439, 33829031, 33836903, 33837927,
33849703, 33868135, 33868519, 33874791, 33883975, 33892455, 33897127, 33899751, 33903975,
33920615, 33932135, 33945319, 33948775, 33958119, 33969255, 33980007, 33983847, 33990503,
34001063, 34006759, 34007367, 34024551, 34037351, 34040167, 34040999, 34054983, 34055783,
34061031, 34066759, 34069159, 34080103, 34081895, 34083143, 34087015, 34101991, 34114375,
34115751, 34124103, 34126503, 34143335, 34144359, 34157735, 34164583, 34173767, 34176167,
34179175, 34179399, 34180423, 34180839, 34199655, 34200679, 34223975, 34236743, 34238183,
34239591, 34253159, 34267975, 34277095, 34281319, 34284007, 34302823, 34313543, 34326343,
34328743, 34333415, 34341351, 34346599, 34348199, 34359143, 34360167, 34367847, 34373735,
34374983, 34375591, 34384103, 34396007, 34415463, 34417319, 34429255, 34430055, 34434983,
34440423, 34440807, 34443431, 34447719, 34451367, 34463911, 34466983, 34467559, 34468583,
34468967, 34470215, 34490471, 34492327, 34492903, 34505063, 34515431, 34527975, 34532199,
34540903, 34548647, 34549063, 34561191, 34571751, 34578599, 34580647, 34584295, 34591399,
34598247, 34600295, 34604967, 34606407, 34617959, 34621799, 34622183, 34645319, 34646887,
34649959, 34652231, 34655463, 34678119, 34678951, 34700391, 34701415, 34701639, 34702439,
34707303, 34709575, 34752327, 34757351, 34768103, 34774375, 34778215, 34785959, 34794215,
34797479, 34802535, 34808647, 34809447, 34820967, 34835783, 34836807, 34837607, 34838439,
34838631, 34843303, 34848935, 34851175, 34861127, 34866791, 34880167, 34883655, 34895783,
34896199, 34903271, 34908327, 34908519, 34909543, 34917287, 34918887, 34919271, 34936679,
34939975, 34952519, 34960615, 34973607, 34974631, 34981479, 34986151, 34990407, 35009639,
35017383, 35023687, 35026279, 35043943, 35047143, 35052199, 35058919, 35069031, 35072679,
35075303, 35081575, 35082407, 35091303, 35093351, 35100263, 35103463, 35106535, 35116263,
35125575, 35128423, 35136327, 35137767, 35139751, 35149671, 35162439, 35165927, 35198311,
35204007, 35205031, 35217575, 35222631, 35225447, 35226471, 35228519, 35241063, 35255655,
35257511, 35259751, 35260135, 35264359, 35264423, 35271495, 35273319, 35274919, 35280999,
35287111, 35288295, 35294567, 35309159, 35316071, 35325415, 35328839, 35329639, 35340391,
35344231, 35358631, 35367143, 35381735, 35389607, 35397735, 35400359, 35400551, 35415367,
35416167, 35427143, 35429543, 35438439, 35440487, 35443527, 35446951, 35454055, 35471687,
35474759, 35484487, 35486887, 35493799, 35503719, 35505991, 35506343, 35508391, 35531879,
35534151, 35544423, 35547879, 35583335, 35594727, 35597543, 35602599, 35613543, 35628359,
35655335, 35656519, 35669863, 35680423, 35693639, 35703911, 35706983, 35727207, 35728231,
35735143, 35735367, 35740391, 35746663, 35749959, 35751143, 35761255, 35768807, 35777703,
35800807, 35801191, 35805863, 35828967, 35831399, 35838311, 35838695, 35842983, 35857127,
35875175, 35892583, 35895463, 35901287, 35916103, 35918951, 35922791, 35932519, 35943079,
35949927, 35951783, 35960679, 35962951, 35965767, 35982183, 36007271, 36008103, 36012775,
36015847, 36025959, 36039335, 36062823, 36063463, 36066663, 36088551, 36090983, 36093799,
36096679, 36108615, 36109415, 36119367, 36120167, 36128487, 36134759, 36137031, 36142695,
36146343, 36148327, 36162919, 36169031, 36169831, 36172263, 36181351, 36185447, 36197191,
36202663, 36203239, 36203687, 36206919, 36210535, 36211559, 36222311, 36225351, 36227175,
36236519, 36240551, 36256359, 36260007, 36263655, 36268903, 36277607, 36297319, 36298087,
36320999, 36322407, 36341863, 36346535, 36354663, 36374695, 36377767, 36380999, 36384071,
36385639, 36386663, 36394343, 36397415, 36410983, 36412583, 36419303, 36422503, 36423527,
36431687, 36433063, 36435687, 36437095, 36439143, 36448487, 36453735, 36456775, 36457575,
36460647, 36461223, 36476647, 36476839, 36480935, 36496711, 36513127, 36528295, 36529511,
36530535, 36532967, 36540487, 36546151, 36558695, 36570471, 36571463
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.