Prove2Me

Uniform eleven-step Syracuse descent on 961 progressions modulo 2182^{18}

Proved
syracuse_descent_progressions_mod262144

by FakeMink · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

iterationnumber-theorystopping-time

Let T(n)T(n) be the odd part of 3n+13n+1, the platform's Syracuse map, and let T11T^{11} denote eleven successive applications. Let RR be the explicit list of 961 distinct residues modulo 218=2621442^{18}=262144 enumerated in the formal statement. For every natural number nn,

n mod 262144∈R⟹T11(n)<n.n\bmod262144\in R \quad\Longrightarrow\quad T^{11}(n)<n.

This is a uniform statement on infinite arithmetic progressions, not a check of only their least representatives. The list has 573 classes from the current fifteen branch, 194 from the seven branch, and 194 from the twentyseven branch of the Collatz mission. It can be used to remove these classes from the corresponding residual descent obligations.

Formalization Note. The map is the existing definition syracuseStep; the explicit residue list is part of the theorem's type. No monotonicity of the Syracuse map is asserted.

Preamble
import Definitions.Def_syracuseStep
import Mathlib.Logic.Function.Iterate
import Mathlib.Tactic.Ring
import Std

set_option maxRecDepth 16384
Formal statement
theorem syracuse_descent_progressions_mod262144 (n : ℕ)
    (h : n % 262144 ∈ ([511, 1023, 1791, 2159, 3183, 3263, 3327, 3375, 3583, 3615, 3775, 4143, 4543, 5167, 5839, 5999, 6079, 6367, 6399, 6527, 6767, 6847, 9471, 10095, 10399, 10447, 10495, 11007, 11375, 11423, 11455, 12479, 12591, 12831, 12911, 13359, 13471, 13727, 15775, 16031, 16543, 17567, 18079, 18287, 18687, 19311, 19663, 19871, 20383, 20671, 20719, 20799, 21151, 22767, 22847, 23023, 24479, 24991, 25071, 25759, 26943, 27295, 27375, 27455, 27503, 27631, 28063, 28143, 29311, 30335, 31551, 31615, 31871, 32063, 32671, 33695, 33775, 34287, 34687, 34943, 35135, 35455, 37759, 38447, 38783, 38975, 39743, 40767, 41087, 41439, 41519, 41887, 41967, 42015, 42367, 43455, 44063, 44479, 44591, 45615, 45759, 46015, 46047, 46975, 48159, 48191, 48431, 48511, 48671, 48831, 48847, 48959, 49087, 49199, 49279, 49599, 50895, 51311, 51903, 52223, 52527, 52767, 52927, 52991, 53279, 53359, 53759, 53807, 54015, 54991, 55231, 55263, 55343, 55503, 55919, 56063, 56351, 56431, 56511, 58367, 58623, 59135, 59599, 60111, 60159, 60191, 60671, 60719, 60959, 61119, 61743, 61983, 62063, 62575, 62655, 62975, 63183, 63343, 63423, 63743, 64671, 65695, 66975, 67023, 67231, 67791, 68351, 68815, 68847, 69407, 69487, 69887, 69935, 70047, 70175, 70255, 70303, 70383, 70815, 71919, 72431, 73119, 74047, 74143, 74223, 76239, 76447, 76527, 77007, 77119, 77295, 77727, 80191, 81215, 81647, 82335, 83439, 83871, 84031, 84447, 84607, 84639, 84719, 84799, 86495, 86655, 86911, 88127, 88959, 89407, 90591, 90943, 91103, 91263, 91519, 91631, 92031, 93743, 95199, 95263, 95711, 95791, 96319, 97343, 97663, 98175, 98335, 98351, 98751, 98783, 98863, 100799, 101055, 101407, 102095, 102431, 102511, 102623, 103103, 103391, 104415, 104447, 104495, 104959, 105007, 105167, 105247, 105407, 105535, 105583, 105663, 105775, 105855, 105983, 106015, 106175, 107263, 107519, 108031, 108239, 108287, 109263, 109343, 109823, 110623, 111103, 111727, 111807, 111839, 111919, 112079, 112127, 112159, 112319, 112495, 112607, 112687, 112847, 112895, 113407, 116175, 117455, 117535, 118559, 118639, 118991, 119039, 119919, 119967, 119999, 120319, 122015, 122095, 122271, 123631, 124319, 124367, 125391, 126623, 126703, 126751, 126831, 126879, 127231, 127391, 129343, 129775, 130799, 131311, 131391, 132735, 133023, 133535, 133583, 133615, 133951, 134271, 134463, 135807, 136319, 137695, 138111, 138223, 138991, 140095, 140415, 140607, 140767, 141183, 141215, 141375, 143839, 144863, 144943, 145535, 146879, 147327, 147439, 147519, 147679, 148015, 148287, 148415, 148447, 148607, 149951, 150463, 150559, 151775, 152255, 152607, 153055, 154159, 154559, 154591, 154927, 155167, 155327, 155519, 155679, 157391, 159231, 159439, 159679, 159967, 160255, 160991, 161071, 161311, 161471, 161823, 161903, 161999, 162351, 162511, 162559, 162591, 162751, 164607, 165375, 166511, 168095, 168143, 168655, 168735, 169183, 169215, 169263, 169423, 169503, 169631, 169663, 171167, 171679, 173295, 173471, 174319, 175567, 175727, 175775, 176335, 176367, 176543, 176623, 178671, 178927, 179439, 180463, 180543, 180895, 180975, 182687, 182767, 183279, 183615, 183967, 184047, 185983, 187375, 187519, 187887, 188655, 189759, 190191, 190527, 190591, 190879, 190959, 192991, 193663, 194687, 195039, 195199, 195567, 196591, 196671, 197503, 197599, 197951, 198111, 200127, 201663, 201759, 202111, 202879, 203743, 204255, 204335, 204735, 204783, 204831, 204863, 204911, 205023, 206959, 207807, 208591, 208831, 208943, 209343, 209919, 210687, 210975, 211055, 211167, 211327, 211567, 211647, 211663, 211743, 211935, 212223, 213759, 214271, 214527, 215663, 216175, 216255, 216575, 217023, 217807, 217887, 218159, 218367, 218575, 219167, 219247, 221343, 222879, 223087, 223487, 223855, 224719, 224879, 225471, 225951, 225999, 226079, 226559, 227567, 228591, 229023, 229871, 230047, 230127, 230559, 232303, 232863, 232911, 232943, 233071, 233199, 233711, 236015, 237039, 237183, 237471, 238207, 238239, 239343, 239935, 240255, 240511, 240623, 242559, 242815, 243327, 244191, 244351, 244543, 244863, 245231, 246655, 246687, 246767, 247167, 247263, 247343, 247535, 247935, 249391, 251263, 251327, 251775, 252351, 252543, 253407, 253487, 253759, 253999, 254079, 254175, 254399, 254655, 254847, 256703, 256959, 257471, 258095, 258159, 258495, 258607, 259007, 259455, 260319, 260479, 260799, 261151, 261231, 261311, 261599, 261679, 262079, 5287, 6055, 8519, 10567, 12199, 13031, 13127, 13479, 13639, 17639, 19271, 19783, 20391, 20551, 24423, 25447, 26695, 26855, 27463, 27495, 27751, 29799, 30055, 30567, 31591, 32103, 33895, 34407, 35175, 38503, 39015, 39783, 41319, 42087, 46695, 47719, 55463, 55911, 56039, 58087, 59719, 60071, 62183, 62695, 62791, 66791, 67303, 68935, 69287, 69703, 70375, 74215, 74983, 75847, 76007, 77127, 78695, 79719, 80999, 81255, 83431, 84039, 84071, 84199, 84327, 84839, 87143, 88167, 90471, 91751, 96359, 97895, 98471, 98663, 100519, 104615, 105127, 109223, 109287, 109735, 112359, 112807, 115431, 116455, 116647, 117415, 118439, 119111, 119271, 120039, 123367, 123719, 124647, 125863, 126183, 126631, 131559, 132583, 132935, 133991, 136039, 136295, 138343, 140647, 140775, 140903, 141415, 147047, 147559, 151719, 154791, 155239, 157863, 158887, 161703, 162119, 162471, 164167, 164583, 165799, 166631, 167079, 168263, 168615, 168775, 169191, 169703, 172871, 173383, 173991, 175015, 175335, 175847, 176455, 176615, 180295, 181063, 182087, 182119, 182759, 183207, 183527, 183655, 185191, 185703, 187495, 189511, 189799, 190279, 190567, 194919, 196711, 197991, 204903, 207015, 209063, 211623, 212135, 215367, 215783, 217767, 218279, 218439, 218855, 219047, 221511, 222535, 224999, 225191, 225351, 225767, 225959, 226119, 229447, 230727, 231911, 232263, 233191, 235367, 236903, 237639, 238663, 239975, 240103, 243047, 244071, 244583, 246855, 246887, 251495, 252263, 258215, 260711, 261287, 1691, 1883, 2043, 2459, 2651, 2811, 6139, 7419, 8603, 8955, 9883, 12059, 13595, 14331, 15355, 16667, 16795, 19739, 20763, 21275, 23547, 23579, 28187, 28955, 34907, 37403, 37979, 44123, 44891, 47355, 49403, 51035, 51867, 51963, 52315, 52475, 56475, 58107, 58619, 59227, 59387, 63259, 64283, 65531, 65691, 66299, 66331, 66587, 68635, 68891, 69403, 70427, 70939, 72731, 73243, 74011, 77339, 77851, 78619, 80155, 80923, 85531, 86555, 94299, 94747, 94875, 96923, 98555, 98907, 101019, 101531, 101627, 105627, 106139, 107771, 108123, 108539, 109211, 113051, 113819, 114683, 114843, 115963, 117531, 118555, 119835, 120091, 122267, 122875, 122907, 123035, 123163, 123675, 125979, 127003, 129307, 130587, 135195, 136731, 137307, 137499, 139355, 143451, 143963, 148059, 148123, 148571, 151195, 151643, 154267, 155291, 155483, 156251, 157275, 157947, 158107, 158875, 162203, 162555, 163483, 164699, 165019, 165467, 170395, 171419, 171771, 172827, 174875, 175131, 177179, 179483, 179611, 179739, 180251, 185883, 186395, 190555, 193627, 194075, 196699, 197723, 200539, 200955, 201307, 203003, 203419, 204635, 205467, 205915, 207099, 207451, 207611, 208027, 208539, 211707, 212219, 212827, 213851, 214171, 214683, 215291, 215451, 219131, 219899, 220923, 220955, 221595, 222043, 222363, 222491, 224027, 224539, 226331, 228347, 228635, 229115, 229403, 233755, 235547, 236827, 243739, 245851, 247899, 250459, 250971, 254203, 254619, 256603, 257115, 257275, 257691, 257883, 260347, 261371] : List ℕ)) :
    syracuseStep^[11] n < n := by sorry
Source
Explicit independently certified affine residue refinement of Prove2Me Collatz frontier https://prove2.me/theorems/b5094e6b-1347-43fe-ac3d-adbf79509f5e; exact map https://prove2.me/theorems/2d5fcb43-85b2-4d75-beb8-3e236e66eac3. The refinement count and method were anticipated in the Collatz mission discussion: Steve1136, September 21, 2026, comment 67f53213-642c-408f-aeff-d989148c84d4, and Zexuan Liu, September 8, 2026, https://prove2.me/missions/Collatz_Conjecture. This contribution supplies an explicit independently kernel-checked coefficient/parity-vector certificate and a frontier reduction, not a new Collatz strategy. The remaining assertion adds only nonmembership in the certified mod-2^18 list to the exact parent statement. This computed table is not claimed to be a theorem quoted from the literature.

View graph