Fifteen-branch Syracuse descent remaining after 573 further certified progressions

Open

syracuse_descent_residual_fifteen_mod16_mod262144

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

dynamical-systemsiterationnumber-theorystopping-time

Let $T(n)$ be the odd part of $3n+1$ , and let $T^t$ denote $t$ successive applications. Suppose $n$ satisfies every congruence and exclusion hypothesis of the current fifteen-branch residual descent theorem. In particular,

n\equiv15\pmod{16}.

Let $R$ be the explicit list of 961 residues modulo $2^{18}=262144$ from the proved uniform eleven-step descent theorem, repeated verbatim in the formal statement. Add the condition

n\bmod262144\notin R.

The remaining open assertion is

\exists t\in\mathbb N,\qquad T^t(n)<n.

Every hypothesis of the parent is retained. Within that parent, the proved list handles 573 infinite arithmetic progressions; this child states descent on the complementary classes. Neither the starting value nor the descent time is bounded, and this universal residual claim remains unproved. Its role is the explicitly unresolved child of a certified refinement, not a claim that the original frontier or Collatz is solved.

Formalization Note. The map is the existing syracuseStep. The extra condition is nonmembership in the same literal List ℕ as the proved supporting theorem. The recursion-depth setting only permits elaboration of the long literals.

Preamble

import Definitions.Def_syracuseStep
import Mathlib.Logic.Function.Iterate
import Mathlib.Data.Finset.Insert
set_option maxRecDepth 16384

Formal statement

theorem syracuse_descent_residual_fifteen_mod16_mod262144 (n : ℕ)
    (h : n % 16 = 15)
    (h128 : n % 128 ≠ 15)
    (h256 : n % 256 ≠ 79 ∧ n % 256 ≠ 95 ∧ n % 256 ≠ 175)
    (h1024 : n % 1024 ≠ 287 ∧ n % 1024 ≠ 367 ∧ n % 1024 ≠ 575 ∧ n % 1024 ≠ 735 ∧ n % 1024 ≠ 815 ∧ n % 1024 ≠ 975)
    (h4096 : n % 4096 ≠ 383 ∧ n % 4096 ≠ 463 ∧ n % 4096 ≠ 879 ∧ n % 4096 ≠ 1087 ∧ n % 4096 ≠ 1231 ∧ n % 4096 ≠ 1647 ∧ n % 4096 ≠ 1823 ∧ n % 4096 ≠ 1855 ∧ n % 4096 ≠ 2031 ∧ n % 4096 ≠ 2239 ∧ n % 4096 ≠ 2351 ∧ n % 4096 ≠ 2591 ∧ n % 4096 ≠ 2975 ∧ n % 4096 ≠ 3119 ∧ n % 4096 ≠ 3295 ∧ n % 4096 ≠ 4063)
    (h8192 : n % 8192 ∉ ({191, 207, 255, 303, 543, 623, 719, 799, 1071, 1135,
      1215, 1247, 1327, 1567, 1727, 1983, 2015, 2079, 2095, 2271,
      2431, 2607, 3039, 3135, 3455, 3551, 3903, 3967, 4079, 4159,
      4223, 4927, 5023, 5103, 5439, 5615, 5871, 6047, 6559, 6607,
      6815, 7023, 7375, 7631, 7791, 7967, 8047} : Finset ℕ))
    (h32768 : n % 32768 ∉ ({127, 415, 831, 1151, 1775, 1903, 2303, 2719, 2767, 2799,
      2847, 3743, 4031, 4287, 4655, 5231, 5311, 5599, 5631, 6175,
      6255, 6783, 7199, 7487, 8063, 8431, 9087, 9375, 9679, 9711,
      10655, 10735, 10863, 11119, 11567, 11679, 11807, 11967, 12063, 12143,
      12511, 12543, 13007, 13087, 13567, 13695, 14031, 14271, 14399, 14895,
      15295, 15343, 15839, 15919, 16287, 16863, 17727, 18639, 18751, 18895,
      19199, 19919, 20079, 20527, 20783, 20927, 21023, 21103, 21471, 21727,
      21807, 22047, 22207, 22655, 22751, 22911, 23231, 23359, 23615, 23935,
      24303, 24559, 24639, 25247, 25503, 25583, 26527, 27759, 27839, 27855,
      28703, 28879, 29743, 30591, 30687, 30767, 31711, 32239, 32575} : Finset ℕ))
    (h65536 : n % 65536 ∉ ({479, 559, 767, 1183, 1519, 1535, 2367, 2495, 2671, 2687,
      2927, 3103, 3487, 3535, 3695, 4319, 4335, 4799, 4815, 4895,
      4991, 5087, 5343, 5375, 5423, 5583, 5663, 5823, 6207, 6639,
      6703, 6975, 7103, 7231, 7471, 7551, 7711, 7871, 8095, 8671,
      8863, 9119, 9199, 9599, 9935, 10559, 11247, 11727, 11823, 11887,
      12319, 12495, 12799, 13279, 13535, 13615, 13855, 13951, 14015, 14207,
      14303, 14383, 14543, 15103, 15167, 15423, 15487, 15599, 15743, 15855,
      16191, 16431, 16511, 16831, 17055, 17135, 17311, 17391, 18159, 18559,
      19135, 19151, 19231, 20127, 20207, 20511, 20591, 20687, 21039, 21615,
      21695, 22015, 22399, 22495, 22575, 23167, 23583, 23663, 23711, 23743,
      24047, 24383, 24703, 24815, 25471, 25599, 26015, 26063, 26351, 26367,
      27039, 27119, 27343, 27423, 27903, 27951, 28095, 28191, 28319, 28351,
      28447, 28527, 28927, 29087, 29231, 29631, 29807, 29823, 29887, 30079,
      30207, 30415, 30575, 30655, 30975, 31199, 31359, 31471, 31727, 31775,
      32223, 32303, 32703, 33007, 33087, 33663, 34111, 34255, 34271, 34927,
      35023, 35231, 35279, 35311, 35583, 36143, 36159, 36383, 36543, 36639,
      36719, 36911, 37119, 37167, 37311, 37407, 37487, 38047, 38271, 38607,
      38847, 39039, 39135, 39295, 39535, 39615, 39919, 40351, 40415, 40495,
      40687, 40943, 41023, 41183, 42239, 42303, 42911, 43071, 43215, 43471,
      43775, 43967, 44143, 44223, 44239, 44959, 45103, 45359, 45503, 45535,
      45599, 45679, 46127, 47231, 47327, 47423, 47487, 47807, 48095, 48879,
      49135, 49215, 49311, 49567, 49983, 50143, 50303, 50847, 51055, 51103,
      51455, 51871, 51951, 52031, 52335, 52415, 52431, 52735, 53183, 53439,
      53887, 53919, 54303, 54319, 54751, 55327, 55407, 55535, 56191, 56287,
      56639, 57215, 57375, 57759, 57839, 58175, 58495, 58527, 58863, 59247,
      59263, 59647, 60015, 60063, 60143, 60271, 60831, 60911, 61135, 61375,
      61631, 61663, 62159, 62239, 62719, 62943, 63023, 63519, 63551, 63599,
      64047, 64207, 64287, 64447, 64831, 65183, 65407, 65439} : Finset ℕ))
    (h262144 : 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 ℕ)) :
    ∃ t : ℕ, syracuseStep^[t] n < n := by sorry

Source

Explicit certified refinement of https://prove2.me/theorems/5665af96-2aa2-40e1-bbbc-91f41434d7f9 using the existing Proved theorem syracuse_descent_progressions_mod262144, https://prove2.me/theorems/b4cf0c47-c078-4235-b853-32b5a518517e, and the exact Syracuse definition https://prove2.me/theorems/2d5fcb43-85b2-4d75-beb8-3e236e66eac3. The complementary assertion copies every original hypothesis and adds only nonmembership in that theorem's explicit mod-2^18 list. The finite-modulus refinement method was already anticipated in the Collatz mission discussion, including Steve1136's September 21 and Zexuan Liu's September 8, 2026 comments, https://prove2.me/missions/Collatz_Conjecture. This contribution integrates the existing certificate; no new Collatz strategy or literature theorem is claimed.

View graph