New Syracuse step-12 certificate classes, chunk 1
DefinitionsyracuseSevenMod32New26Step12Chunk01Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 1 of 1 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 525 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 syracuseSevenMod32New26Step12Chunk01Classes : Finset ℕ := {
133031, 156519, 611495, 667815, 831975, 925799, 1014951, 1197927, 1200199, 1329255, 1568423,
1624743, 1648231, 1676391, 2032871, 2056359, 2154855, 2164199, 2370663, 2401095, 2532423,
2985127, 3008615, 3332263, 3393255, 3449575, 3646567, 3735719, 3761479, 3817799, 3890535,
4289191, 4434663, 4692647, 4802887, 4875623, 4884967, 5006951, 5250919, 5253191, 5391591,
5522919, 5649575, 5729383, 5759815, 5891143, 6053031, 6114023, 6207847, 6367335, 6372007,
6482247, 6714471, 6751975, 6808295, 6850471, 7120199, 7176519, 7249255, 7568231, 7732391,
7915367, 8243687, 8370343, 8393831, 8487655, 8609639, 8611911, 8855879, 8872295, 8928615,
9472743, 9566567, 9730727, 9840967, 10209191, 10326503, 10429671, 10453159, 10560999, 10694727,
10797895, 10926951, 10929223, 10955111, 11062951, 11091111, 11593063, 11752551, 11790055,
11846375, 12158279, 12214599, 12231015, 12287335, 12315495, 12634471, 13112935, 13150439,
13281767, 13518663, 13649991, 13675879, 13685223, 13783719, 13994855, 14053447, 14421671,
14473319, 14604647, 14689127, 14951783, 15144103, 15247271, 15355239, 15364583, 15514727,
15732807, 15871207, 15965031, 16239431, 17142439, 17194087, 17231591, 17269095, 17599815,
17672551, 17864871, 17968039, 18047847, 18502823, 18723303, 18967271, 19032935, 19091527,
19225255, 19335495, 19351911, 19459751, 19830375, 19867879, 19924199, 19952359, 19989863,
20236103, 20292423, 20320583, 20585639, 20688807, 20712295, 21190759, 21223591, 21247079,
21284583, 21652807, 22072679, 22180519, 22232167, 22325991, 22447975, 22583975, 22588647,
22612135, 22694215, 22710631, 22956871, 23189095, 23226599, 23282919, 23540903, 23594823,
23651143, 23911527, 23944359, 23949031, 24005351, 24071015, 24263335, 24291495, 24317255,
24373575, 24549479, 24605799, 24643303, 24671463, 24685479, 24741799, 24985767, 25011527,
25039687, 25623719, 25806695, 25947367, 26031847, 26261671, 26285159, 26315591, 26350823,
26400071, 26669799, 26719047, 26763623, 26829287, 27038023, 27197511, 27270247, 27307751,
27364071, 27406247, 27622055, 27675975, 27711207, 27732295, 27833191, 28044199, 28079431,
28100519, 28227175, 28264679, 28320999, 28344487, 28632903, 28689223, 28752615, 28982439,
29120839, 29329575, 29484391, 29489063, 29512551, 29587559, 29643879, 29681383, 30028519,
30049607, 30122343, 30396743, 30431975, 30764967, 30800199, 30947943, 30985447, 31008935,
31168423, 31353671, 31388903, 31757127, 32205159, 32345831, 32714055, 32749287, 32843111,
33068263, 33082279, 33117511, 33138599, 33436487, 33546727, 33565543, 33668711, 33914951,
34231655, 34367655, 34428647, 34550631, 34796871, 35029095, 35066599, 35160423, 35434823,
35563879, 35592039, 35728039, 35803047, 35911015, 36206503, 36229991, 36426983, 36605287,
36764775, 36795207, 36905447, 36924263, 37088423, 37149415, 37243239, 37271399, 37273671,
37517639, 37665383, 37721703, 37749863, 37759207, 37787367, 37881191, 37885863, 37965671,
38127431, 38129831, 38155591, 38603623, 39082087, 39588711, 39809191, 39964007, 40123495,
40386151, 40479975, 40601959, 40848199, 40949095, 41024103, 41080423, 41117927, 41244583,
41486151, 41746535, 41802855, 41840359, 41943527, 41962343, 42208583, 42309479, 42311751,
42440807, 42445479, 42468967, 42576807, 42628455, 43744871, 43805863, 43829351, 43838695,
43862183, 43988839, 44148327, 44206919, 44467303, 44561127, 44664295, 44847271, 44929351,
45032519, 45105255, 45161575, 45199079, 45297575, 45508711, 45567303, 45804199, 45921511,
45935527, 45987175, 46062183, 46118503, 46156007, 46289735, 46524231, 46526631, 46550119,
47164583, 47220903, 47281895, 47347559, 47385063, 47478887, 47650119, 47753287, 47826023,
47919847, 48229479, 48288071, 48656295, 48707943, 48782951, 48876775, 48900263, 49083239,
49186407, 49244999, 49280231, 49308391, 49430375, 49648455, 49676615, 49749351, 49885351,
50068327, 50143335, 50237159, 50546791, 50605383, 50640615, 50739111, 50842279, 50865767,
50959591, 50973607, 50987751, 51008839, 51109735, 51327815, 51355975, 51381735, 51428711,
51438055, 51682023, 51749959, 51806279, 52050247, 52202663, 52226151, 52258983, 52319975,
52441959, 52688199, 52864103, 52957927, 53326151, 53563047, 53694375, 54097831, 54102503,
54121319, 54224487, 54318311, 54470727, 54686535, 54740455, 54796775, 54946919, 55040743,
55108679, 55164999, 55408967, 55425383, 55481703, 55556711, 55584871, 55678695, 55777191,
56025831, 56046919, 56185319, 56283815, 56394055, 56466791, 56553543, 56785767, 56842087,
57461223, 57480039, 57644199, 57705191, 57827175, 57829447, 57864679, 58073415, 58146151,
58232903, 58277479, 58784103, 58840423, 58868583, 58915431, 59135911, 59379879, 59637863,
59778535, 59834855, 60144487, 60146759, 60200807, 60203079, 60280487, 60336807, 60364967,
60519783, 60547943, 61063911, 61432135, 61504871, 61636199, 61697191, 61880167, 62358631,
62424295, 62499303, 62738599, 62792519, 62867527, 62902759, 62996583, 63001255, 63270983,
63639207, 63695527, 63719015, 63784679, 63822183, 63878503, 63953511, 64152903, 64361639,
64417959, 64582119, 64826087, 64950343, 65055911, 65079399, 65084071, 65182567, 65194311,
65238887, 65717351, 66359975, 66444455, 66505447, 66627431, 66674279, 66763431, 66873671,
67077735, 67082407, 67105895
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.