New Syracuse step-14 certificate classes, chunk 2
DefinitionsyracuseSevenMod32New26Step14Chunk02Classes2-adiccertificate-setcollatznumber-theorysyracuse
Chunk 2 of 5 of the newly certifiable residue classes modulo with accelerated Syracuse descent time and total stripped exponent . This chunk contains 678 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 syracuseSevenMod32New26Step14Chunk02Classes : Finset ℕ := {
13518439, 13546599, 13553319, 13584103, 13590375, 13592647, 13608039, 13612263, 13627879,
13664359, 13677927, 13697191, 13705063, 13719879, 13722951, 13752935, 13779271, 13795687,
13836615, 13852007, 13853031, 13872295, 13909351, 13928615, 13952327, 13980487, 13989607,
13996103, 14055271, 14088103, 14092775, 14111591, 14186599, 14199143, 14217383, 14227303,
14240871, 14250663, 14336743, 14357831, 14363303, 14396135, 14453479, 14460999, 14486887,
14533735, 14546279, 14547303, 14553575, 14625511, 14627559, 14631783, 14646375, 14654119,
14704967, 14711463, 14747495, 14764359, 14777703, 14805863, 14821703, 14837095, 14846439,
14855335, 14878823, 14883495, 14921799, 14937191, 14968423, 14972647, 14978919, 14993735,
14995783, 15031015, 15038311, 15075815, 15109223, 15124839, 15143079, 15189927, 15212391,
15214663, 15240551, 15307239, 15340871, 15353063, 15364007, 15399239, 15400039, 15410407,
15415655, 15433895, 15444039, 15484391, 15490663, 15516775, 15541735, 15546983, 15559527,
15584487, 15603303, 15607975, 15611047, 15640807, 15675463, 15690855, 15721287, 15723687,
15767463, 15772135, 15778631, 15790951, 15847271, 15852615, 15878503, 15894119, 15906663,
15907687, 15909959, 15920231, 15935847, 15952711, 15987943, 16009031, 16014503, 16016103,
16043687, 16050535, 16071847, 16075495, 16128167, 16138087, 16140359, 16166247, 16169319,
16175591, 16243879, 16274087, 16304871, 16311143, 16328807, 16333479, 16356167, 16356967,
16384327, 16385127, 16394471, 16398695, 16426855, 16443719, 16457063, 16473703, 16485223,
16516455, 16543815, 16562855, 16573799, 16593063, 16600935, 16673095, 16675943, 16713447,
16733287, 16762695, 16765095, 16769767, 16770791, 16773991, 16776039, 16804199, 16811943,
16827111, 16851047, 16877159, 16905319, 16912039, 16944871, 16963687, 16999143, 17041319,
17081671, 17095015, 17121127, 17137991, 17139015, 17179495, 17195335, 17210727, 17211751,
17236839, 17238887, 17254503, 17268071, 17285287, 17296231, 17313095, 17348327, 17367367,
17410919, 17440103, 17446823, 17529703, 17549991, 17573479, 17576103, 17615207, 17634471,
17667303, 17681319, 17693415, 17693863, 17695463, 17716551, 17717351, 17745511, 17759079,
17817447, 17834087, 17845607, 17854951, 17876839, 17902951, 17923239, 17989479, 18005095,
18035527, 18061639, 18063687, 18089447, 18093671, 18106215, 18131175, 18136423, 18145767,
18164583, 18187495, 18205159, 18223175, 18237543, 18262503, 18267751, 18331815, 18355303,
18361575, 18389735, 18429863, 18444455, 18449127, 18455399, 18457671, 18499399, 18513991,
18533031, 18555719, 18556519, 18571111, 18573383, 18584679, 18599271, 18630727, 18656615,
18665959, 18678503, 18729799, 18757959, 18758759, 18764455, 18780647, 18800487, 18817351,
18830695, 18833767, 18890087, 18910375, 18916199, 18933863, 18964647, 18966695, 18975591,
19027687, 19034183, 19046727, 19063143, 19072487, 19105895, 19115239, 19119463, 19148871,
19149671, 19237223, 19263335, 19278951, 19372775, 19395911, 19402407, 19409255, 19434215,
19440711, 19454055, 19482215, 19483463, 19524967, 19528039, 19547879, 19571815, 19585383,
19628135, 19632807, 19665639, 19669863, 19684455, 19692199, 19715687, 19721959, 19740999,
19753191, 19802439, 19893415, 19916103, 19916903, 19932519, 20033863, 20090183, 20121415,
20124839, 20170663, 20191079, 20228007, 20270759, 20287975, 20327079, 20335975, 20345319,
20355239, 20357863, 20391143, 20402087, 20414631, 20438119, 20450663, 20458407, 20475623,
20495463, 20510055, 20522471, 20538215, 20554855, 20589287, 20597607, 20610151, 20644007,
20653927, 20656199, 20713543, 20726087, 20759367, 20769639, 20798823, 20805543, 20810215,
20829031, 20842599, 20843847, 20847271, 20851943, 20888423, 20890695, 20916583, 20932199,
20945767, 20957511, 20993191, 21024423, 21026023, 21052135, 21052583, 21076071, 21088615,
21104231, 21178439, 21204327, 21212071, 21213671, 21220167, 21253799, 21363815, 21394247,
21420359, 21448167, 21457639, 21463911, 21504487, 21554535, 21567079, 21581895, 21604583,
21654631, 21687463, 21714023, 21715623, 21743783, 21748455, 21751527, 21783911, 21793255,
21807847, 21811047, 21816391, 21825863, 21870439, 21872711, 21915239, 21950119, 21972807,
22116679, 22119751, 22123175, 22130023, 22133095, 22159207, 22161479, 22174823, 22176071,
22189415, 22192487, 22207655, 22212327, 22248807, 22249831, 22264423, 22268647, 22276967,
22292583, 22348903, 22386407, 22390631, 22414567, 22431207, 22442727, 22448999, 22464615,
22473959, 22484903, 22497447, 22526631, 22564711, 22580551, 22595943, 22636871, 22637671,
22653287, 22728871, 22733543, 22754631, 22782791, 22783591, 22799431, 22810951, 22842183,
22845607, 22869095, 22893031, 22927463, 22948775, 22991527, 23005095, 23028583, 23074407,
23076007, 23101767, 23111911, 23116135, 23143271, 23172455, 23174503, 23179175, 23191719,
23194343, 23196391, 23243239, 23261255, 23275623, 23299559, 23452327, 23480135, 23483559,
23493479, 23506023, 23549799, 23562567, 23563367, 23564615, 23611463, 23637351, 23646695,
23667783, 23704039, 23713959, 23716583, 23737447, 23745191, 23774951, 23796839, 23803111,
23809383, 23834343, 23876071, 23887015, 23932839, 23948007, 23956327, 23968871, 23974567,
24013671, 24014919, 24069991, 24072263, 24084807, 24143175, 24143975, 24157543, 24168935,
24171335, 24187751, 24202567, 24205991, 24244295, 24316231, 24325351, 24332647, 24351911,
24383143, 24408231, 24412903, 24431719, 24434791, 24440487, 24476519, 24504679, 24532839,
24534887, 24537159, 24548455, 24556775, 24566119, 24570791, 24572391, 24584935, 24650599,
24670887, 24693575, 24753767, 24781127, 24791271, 24811111, 24812711, 24816359, 24848615,
24853863, 24904935, 24913255, 24924999, 24928423, 24933095, 24938343, 24940615, 24953159,
24970599, 24985191, 24995687, 25025895, 25026919, 25074343, 25102503, 25105575, 25151975,
25159495, 25163495, 25184583, 25185383, 25208743, 25216839, 25242727, 25273159, 25301319,
25316711, 25326055, 25334951, 25395943, 25474151, 25476199, 25491815, 25517927, 25520199,
25531719, 25548135, 25555431, 25566375, 25576295, 25623143, 25648231, 25669543, 25685735,
25693031, 25694279, 25764167, 25773287, 25832679, 25836903, 25843623, 25856167, 25865063,
25917159, 25923655, 25926503, 26020327, 26031271, 26053959, 26087591, 26114151, 26141511,
26171495, 26200903, 26204327, 26227815, 26265319, 26285383, 26321639, 26345575, 26386279,
26388551, 26422183, 26434727, 26443623, 26474855, 26486247, 26495719, 26542567, 26555111,
26559335, 26607783, 26633543, 26675047, 26689863, 26753703, 26762599, 26781863, 26852199,
26854471, 26863943, 26864743, 26906471, 26908519, 26910791, 26923335, 26964839, 26988199,
27044519, 27053415, 27068007, 27070631, 27072679, 27096167, 27103911, 27133671, 27155559,
27161255, 27161831, 27193063, 27212903, 27227495, 27230567, 27232167, 27234791, 27255655,
27291559, 27306727, 27311975
}Source
Exact refinement of the seven-mod-32 Syracuse residual tree at modulus 2^26, using Terras uniformity.