New Syracuse step-14 certificate classes, chunk 4
DefinitionsyracuseSevenMod32New26Step14Chunk04Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 4 of 5 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 677 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 syracuseSevenMod32New26Step14Chunk04Classes : Finset ℕ := {
40358215, 40360615, 40371559, 40393447, 40415559, 40449191, 40456039, 40470855, 40471879,
40515431, 40531047, 40544615, 40559431, 40568551, 40572775, 40617799, 40620199, 40624871,
40659303, 40667047, 40687463, 40708775, 40726439, 40761671, 40783783, 40784359, 40832359,
40840103, 40852647, 40882855, 40891751, 40909415, 40913639, 40936775, 40946919, 40970407,
40991847, 40993095, 40993895, 41059559, 41065831, 41093991, 41129895, 41152583, 41171623,
41187239, 41199783, 41210727, 41281863, 41315143, 41350375, 41373863, 41382759, 41384807,
41407719, 41427783, 41441127, 41514087, 41548967, 41551591, 41572455, 41579751, 41586023,
41600615, 41631847, 41650087, 41718599, 41720999, 41729895, 41731943, 41745511, 41775943,
41839335, 41886183, 41894055, 41904999, 41919815, 41947975, 42019687, 42060263, 42069159,
42097319, 42122855, 42130151, 42166631, 42186919, 42192743, 42207559, 42210407, 42223975,
42243239, 42252135, 42254407, 42299559, 42304231, 42307303, 42330791, 42354279, 42382439,
42419943, 42426215, 42428487, 42454375, 42463719, 42498375, 42513767, 42532007, 42588775,
42613863, 42646119, 42672455, 42675527, 42685799, 42688871, 42702439, 42710759, 42713959,
42714983, 42730599, 42739943, 42745191, 42768103, 42788167, 42804583, 42824423, 42831943,
42861927, 42866599, 42940135, 42946407, 42960999, 42970343, 43029735, 43038631, 43043751,
43053223, 43078983, 43092327, 43100071, 43108167, 43110567, 43136327, 43169959, 43192647,
43193447, 43225255, 43259111, 43289319, 43308359, 43338567, 43380071, 43383143, 43397959,
43457703, 43461351, 43467623, 43483239, 43508199, 43527015, 43547303, 43560871, 43570791,
43583335, 43584359, 43608295, 43627335, 43630183, 43640679, 43657543, 43671911, 43691175,
43714663, 43719335, 43737575, 43814759, 43829575, 43874151, 43876423, 43976519, 43978919,
43981543, 44025767, 44046183, 44062823, 44105799, 44119143, 44143079, 44182183, 44193127,
44246247, 44269735, 44272359, 44293223, 44329127, 44330727, 44349767, 44352615, 44365159,
44377575, 44390119, 44452711, 44509031, 44511303, 44512103, 44530343, 44569447, 44614471,
44619495, 44640583, 44698951, 44741479, 44743527, 44745799, 44758343, 44771687, 44789927,
44879527, 44907687, 44931175, 44944743, 44959335, 44964007, 44987719, 44990567, 45008807,
45028071, 45059431, 45067175, 45079719, 45104231, 45121895, 45126119, 45140711, 45146983,
45218919, 45229287, 45252775, 45262695, 45309543, 45320039, 45366887, 45396295, 45398695,
45409639, 45460711, 45484199, 45494343, 45508935, 45525351, 45542567, 45553511, 45569127,
45582695, 45597511, 45606631, 45660903, 45662951, 45689511, 45712999, 45725543, 45741159,
45754727, 45764519, 45828935, 45872487, 45877159, 45890727, 45929831, 45974855, 46004839,
46029127, 46031175, 46047591, 46061159, 46098663, 46103911, 46121127, 46132071, 46167975,
46178471, 46191463, 46204007, 46225319, 46319719, 46329063, 46352551, 46388455, 46392679,
46397351, 46411943, 46419815, 46420839, 46451047, 46466887, 46552167, 46566759, 46583975,
46589671, 46638695, 46669927, 46697287, 46726247, 46727271, 46756679, 46759079, 46783591,
46821095, 46866919, 46885735, 46924263, 46929511, 46942055, 46943079, 46957895, 46967015,
47023335, 47030631, 47046823, 47049895, 47051495, 47073383, 47098343, 47110887, 47115111,
47154663, 47163559, 47189319, 47204711, 47232871, 47235143, 47290215, 47292487, 47335239,
47340263, 47361127, 47368871, 47391559, 47392359, 47419719, 47420519, 47421543, 47426215,
47434087, 47449703, 47466567, 47479111, 47492455, 47501799, 47522887, 47543527, 47557543,
47564391, 47600295, 47609191, 47626855, 47651943, 47683175, 47689447, 47708487, 47711335,
47720679, 47748839, 47781223, 47787943, 47800487, 47809383, 47811431, 47842663, 47847335,
47856231, 47857831, 47870023, 47898983, 47908327, 47911751, 47912551, 47927143, 47950055,
47999079, 48057671, 48076711, 48088903, 48089255, 48091303, 48114791, 48117063, 48238247,
48263335, 48276551, 48289895, 48318055, 48318279, 48383719, 48411879, 48421223, 48425895,
48440039, 48475495, 48505703, 48565095, 48608871, 48646375, 48725607, 48729255, 48751943,
48752743, 48768359, 48780103, 48786599, 48794471, 48808263, 48810087, 48819431, 48842919,
48880999, 48903911, 48924775, 48960679, 48969575, 49014599, 49040487, 49043559, 49063847,
49113447, 49129063, 49141607, 49171815, 49181159, 49187655, 49193703, 49222887, 49272135,
49272935, 49331303, 49343847, 49390695, 49425127, 49448039, 49479847, 49488743, 49541863,
49549383, 49550183, 49561927, 49591111, 49634663, 49645031, 49678439, 49683111, 49687783,
49701351, 49711271, 49751399, 49770663, 49772263, 49781607, 49793351, 49828007, 49875431,
49887975, 49910087, 49925479, 49969255, 50013255, 50046887, 50056007, 50069575, 50084967,
50085991, 50140487, 50142311, 50148583, 50154855, 50179815, 50241383, 50243655, 50256199,
50278311, 50314343, 50347623, 50410215, 50441447, 50472807, 50473831, 50489447, 50516807,
50548039, 50563431, 50576999, 50583271, 50619751, 50629095, 50670823, 50704231, 50705255,
50719847, 50751079, 50777191, 50778439, 50784935, 50809671, 50902247, 50910567, 50916263,
50923111, 50951495, 50959015, 50967911, 50985575, 50995047, 50997319, 51010663, 51039047,
51041895, 51042919, 51043495, 51048167, 51079399, 51085671, 51099239, 51104487, 51136743,
51139943, 51146663, 51168103, 51198311, 51206055, 51226471, 51267047, 51270471, 51362471,
51367143, 51390631, 51416391, 51447623, 51472711, 51473511, 51489127, 51504967, 51507367,
51508967, 51530855, 51573607, 51624679, 51635271, 51679399, 51681447, 51704935, 51708007,
51735367, 51764327, 51770599, 51784615, 51798759, 51801831, 51840935, 51864423, 51877191,
51904999, 51920743, 51923815, 51937383, 51951975, 51992903, 51993703, 52031207, 52068711,
52111463, 52138823, 52145319, 52166983, 52170055, 52201639, 52239719, 52262631, 52270951,
52273223, 52283495, 52316327, 52319399, 52328295, 52361127, 52365799, 52384615, 52399207,
52399431, 52402279, 52406951, 52430439, 52459623, 52472167, 52500327, 52538279, 52539879,
52552423, 52558695, 52589927, 52602471, 52630855, 52636327, 52722855, 52727527, 52734023,
52767655, 52783847, 52806759, 52819303, 52849511, 52900583, 52905831, 52908103, 52920647,
52993383, 53010599, 53041831, 53095751, 53118439, 53130983, 53152071, 53168487, 53210215,
53229479, 53268807, 53276327, 53304039, 53310311, 53312359, 53324903, 53340519, 53384295,
53449959, 53463975, 53478119, 53486663, 53499207, 53513575, 53600103, 53637031, 53646951,
53657447, 53672263, 53673063, 53684455, 53688679, 53706343, 53740775, 53763687, 53764263,
53766887, 53767335, 53768935, 53790823, 53800167, 53806439, 53818183, 53820007, 53823655,
53832551, 53846343, 53857511, 53862759, 53880999, 53919079, 53928423, 53950311, 53962855,
53987815, 53996711, 54024871, 54040487, 54052679, 54063975, 54078567, 54108999, 54109799,
54135111, 54137159
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.