New Syracuse step-15 certificate classes, chunk 9
DefinitionsyracuseSevenMod32New26Step15Chunk09Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 9 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 syracuseSevenMod32New26Step15Chunk09Classes : Finset ℕ := {
41823335, 41825607, 41828199, 41841991, 41845863, 41863079, 41907431, 41913703, 41921447,
41922407, 41922471, 41939687, 41945959, 41946791, 41957703, 41958503, 41971879, 41980391,
41985095, 41998439, 42015047, 42017095, 42026599, 42026823, 42040167, 42042855, 42046279,
42047079, 42068327, 42073191, 42074439, 42075239, 42083559, 42084583, 42089831, 42092263,
42107047, 42112103, 42117991, 42120423, 42129767, 42134439, 42141287, 42145127, 42147175,
42148583, 42160967, 42166439, 42169063, 42174311, 42184039, 42189127, 42206567, 42214247,
42221159, 42221735, 42225831, 42227431, 42261863, 42273639, 42275655, 42283175, 42291047,
42307911, 42314983, 42317415, 42338471, 42348615, 42349415, 42354919, 42383271, 42396839,
42411079, 42421351, 42424423, 42434151, 42436967, 42437799, 42451783, 42452807, 42455207,
42457255, 42460487, 42461287, 42466151, 42476903, 42480743, 42483815, 42488647, 42492071,
42494311, 42495143, 42503015, 42515175, 42516807, 42518247, 42518631, 42527975, 42537287,
42540135, 42541159, 42551463, 42574567, 42577639, 42579815, 42589543, 42590567, 42595655,
42608999, 42612455, 42633319, 42634983, 42669223, 42676135, 42678119, 42683207, 42696551,
42715623, 42723143, 42727783, 42734055, 42744999, 42749031, 42752103, 42772391, 42784103,
42802343, 42806375, 42821991, 42837607, 42850151, 42859111, 42860711, 42865383, 42880359,
42883399, 42886471, 42887271, 42889703, 42896199, 42902247, 42905511, 42915431, 42928999,
42931431, 42942791, 42944615, 42945863, 42952935, 42959591, 42980679, 42981479, 42985319,
43003207, 43015527, 43032743, 43038439, 43039847, 43052391, 43058279, 43079591, 43081575,
43083847, 43099239, 43102279, 43133671, 43136935, 43153127, 43156583, 43173991, 43182759,
43183335, 43188391, 43197287, 43206823, 43216743, 43233607, 43240103, 43246951, 43250407,
43251623, 43256295, 43257927, 43258727, 43263591, 43267815, 43270471, 43274087, 43275111,
43299655, 43300071, 43306343, 43314087, 43321159, 43326183, 43327815, 43343207, 43353575,
43357415, 43365735, 43371431, 43385575, 43386983, 43391655, 43396327, 43400551, 43406439,
43406663, 43407463, 43409895, 43414183, 43419815, 43428711, 43435623, 43438247, 43440743,
43443943, 43459943, 43463783, 43465831, 43470503, 43479207, 43480807, 43487719, 43490151,
43492967, 43497063, 43501671, 43501895, 43505511, 43507559, 43521351, 43534503, 43534567,
43536551, 43551559, 43559655, 43581543, 43583975, 43586791, 43596519, 43601831, 43618631,
43622247, 43624519, 43634023, 43636039, 43637863, 43668295, 43675367, 43677799, 43681639,
43694407, 43717095, 43721799, 43722215, 43725639, 43753799, 43755431, 43764551, 43778119,
43778535, 43779559, 43793511, 43794535, 43797351, 43812167, 43817639, 43820647, 43822311,
43826535, 43835879, 43845799, 43849031, 43850855, 43854695, 43855943, 43857127, 43863399,
43884903, 43885287, 43888359, 43901095, 43902791, 43905191, 43905767, 43927879, 43928679,
43944295, 43949927, 43952199, 43955015, 43957863, 43964743, 43969383, 43986855, 44000615,
44005287, 44007271, 44008935, 44017831, 44022887, 44028775, 44038503, 44043591, 44056167,
44065255, 44079847, 44085319, 44088167, 44090439, 44100711, 44116327, 44118759, 44134567,
44144487, 44146759, 44147783, 44149991, 44171431, 44181351, 44182375, 44190535, 44194535,
44197991, 44204103, 44215399, 44224167, 44225351, 44225767, 44228775, 44253511, 44256583,
44271975, 44273991, 44275815, 44280487, 44285543, 44288359, 44289383, 44291815, 44303975,
44326247, 44328295, 44336615, 44337639, 44375911, 44377159, 44379367, 44397799, 44411815,
44412775, 44413799, 44418663, 44422759, 44428391, 44433479, 44448071, 44448871, 44459623,
44460263, 44463463, 44485735, 44486983, 44493479, 44506215, 44516583, 44518215, 44520807,
44543079, 44543143, 44543719, 44562759, 44579175, 44579559, 44593991, 44599463, 44600487,
44610791, 44619111, 44623975, 44624807, 44631655, 44635495, 44642215, 44656807, 44660039,
44660455, 44663655, 44664679, 44667559, 44676455, 44694119, 44703591, 44704231, 44704839,
44705863, 44710503, 44712103, 44717799, 44719207, 44726119, 44747591, 44750439, 44751463,
44752039, 44756711, 44763623, 44766023, 44766823, 44774567, 44787943, 44794215, 44796007,
44798439, 44804327, 44805351, 44807783, 44813031, 44828487, 44828839, 44839783, 44845287,
44848487, 44853351, 44855207, 44857447, 44876647, 44884807, 44906855, 44911943, 44914599,
44927335, 44930983, 44935015, 44943527, 44947175, 44947783, 44948199, 44954471, 44975591,
44979015, 45007591, 45028679, 45032935, 45069159, 45071015, 45072455, 45075687, 45086023,
45099175, 45117607, 45124935, 45131847, 45145191, 45156167, 45157735, 45166663, 45172551,
45173575, 45178023, 45179623, 45181031, 45181255, 45182055, 45182695, 45197671, 45204583,
45213511, 45215079, 45215911, 45217511, 45239015, 45239399, 45261927, 45266151, 45280167,
45282151, 45294311, 45298407, 45301607, 45304679, 45311335, 45315399, 45316423, 45317223,
45318247, 45329767, 45333223, 45343815, 45355751, 45375815, 45387943, 45389159, 45389991,
45398887, 45401159, 45405799, 45413479, 45416551, 45427047, 45443303, 45443911, 45447911,
45448551, 45463143, 45464167, 45472871, 45476711, 45479143, 45493159, 45496999, 45500647,
45507303, 45510375, 45523111, 45525159, 45532007, 45534887, 45547847, 45549479, 45550919,
45572967, 45579879, 45585735, 45586151, 45593831, 45607239, 45608039, 45613543, 45620583,
45621991, 45629287, 45632359, 45634375, 45640871, 45645927, 45648743, 45660519, 45662535,
45664359, 45666631, 45673703, 45684647, 45686631, 45697191, 45701447, 45702247, 45723975,
45735271, 45739751, 45758183, 45777255, 45779047, 45783143, 45795687, 45811527, 45816135,
45820007, 45823847, 45839463, 45847367, 45853863, 45868871, 45873895, 45875527, 45876967,
45878599, 45879143, 45881191, 45894759, 45905127, 45910183, 45919143, 45939559, 45948263,
45954375, 45960871, 45962055, 45967719, 45971175, 45975463, 45979495, 45981767, 45983335,
45988583, 45990215, 45992039, 45995879, 46017191, 46024871, 46027943, 46034855, 46036839,
46041927, 46043303, 46062951, 46069671, 46074343, 46077159, 46083431, 46086503, 46092199,
46092775, 46093159, 46107751, 46107975, 46110823, 46115495, 46126407, 46127207, 46128231,
46138983, 46161511, 46165735, 46168167, 46180711, 46191271, 46198119, 46200167, 46208871,
46219431, 46222439, 46242119, 46245191, 46246823, 46248423, 46255335, 46260967, 46267239,
46273351, 46274151, 46278823, 46287719, 46298471, 46302311, 46311015, 46311655, 46318311,
46339399, 46343015, 46344039, 46344871, 46356807, 46396135, 46400359, 46431399, 46436071,
46442567, 46442983, 46445383, 46460999, 46461799, 46468455, 46476199, 46492391, 46495655,
46499303, 46500327, 46508199, 46515303, 46518119, 46519143, 46527847, 46533959, 46535143,
46555623, 46558055, 46564967, 46565543, 46605671, 46609127, 46610343, 46614375, 46616647,
46622311, 46623559, 46626535, 46627943, 46629191, 46658791, 46679879, 46682279, 46686535,
46686951, 46701927, 46716135, 46719143, 46725031, 46729703, 46748519, 46749543, 46750375,
46759271, 46764359, 46766183, 46787431, 46794343, 46804295, 46808935, 46811207, 46823527,
46826983, 46837095, 46839527, 46846439, 46856935, 46857383, 46858983, 46860615, 46867527,
46868551, 46877031, 46888167, 46894439, 46901159, 46902183, 46903367, 46918759, 46923847,
46938023, 46940263, 46944935, 46954215, 46977351, 46980967, 46984871, 46994759, 46996583,
47002855, 47009127, 47012583, 47017831, 47018855, 47020903, 47027015, 47033447, 47034087,
47040359, 47049063, 47053927, 47055175, 47057383, 47066471, 47084359
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.