Twentyseven-branch Syracuse descent remaining after 194 further certified progressions

Open

syracuse_descent_residual_twentyseven_mod32_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 $T^t$ its $t$ -fold iterate. Suppose $n$ satisfies every congruence and exclusion hypothesis of the current twentyseven-branch residual descent theorem. In particular,

n\equiv27\pmod{32}.

Let $R$ be the explicit 961-residue list 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.

This retains every hypothesis of the parent, including both inherited modulus-8192 exclusion groups. Within that parent the proved list handles 194 infinite arithmetic progressions. This child asks for descent on the complementary classes, with neither the starting value nor the descent time bounded. It remains unproved and is intended as an explicitly unresolved child, not a claim that the full parent 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 supports 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_twentyseven_mod32_mod262144 (n : ℕ)
    (h : n % 32 = 27)
    (h128 : n % 128 ≠ 59)
    (h256 : n % 256 ≠ 123 ∧ n % 256 ≠ 219)
    (h1024 : n % 1024 ≠ 347 ∧ n % 1024 ≠ 507 ∧ n % 1024 ≠ 923)
    (h4096 : n % 4096 ≠ 1019 ∧ n % 4096 ≠ 1435 ∧ n % 4096 ≠ 1787 ∧
      n % 4096 ≠ 2203 ∧ n % 4096 ≠ 2587 ∧ n % 4096 ≠ 2907 ∧
      n % 4096 ≠ 3675)
    (h8192 : n % 8192 ≠ 539 ∧ n % 8192 ≠ 1563 ∧ n % 8192 ≠ 2075 ∧
      n % 8192 ≠ 3483 ∧ n % 8192 ≠ 3835 ∧ n % 8192 ≠ 4507 ∧
      n % 8192 ≠ 4859 ∧ n % 8192 ≠ 5371 ∧ n % 8192 ≠ 5723 ∧
      n % 8192 ≠ 6747 ∧ n % 8192 ≠ 7259)
    (h8192b : n % 8192 ≠ 2331 ∧ n % 8192 ≠ 3067 ∧ n % 8192 ≠ 4091 ∧
      n % 8192 ≠ 4251 ∧ n % 8192 ≠ 4955 ∧ n % 8192 ≠ 5275 ∧
      n % 8192 ≠ 5787 ∧ n % 8192 ≠ 5979)
    (h32768 : n % 32768 ∉ ({411, 1275, 2299, 3163, 3611, 4187, 6907, 7163, 8187, 8347,
      8795, 9051, 9371, 10075, 12571, 12827, 13851, 16027, 16123, 17147,
      18011, 19035, 20507, 22811, 22939, 23803, 23835, 25691, 26267, 27291,
      29467, 30715, 30747, 31771, 31899, 32155, 32603} : Finset ℕ))
    (h65536 : n % 65536 ∉ ({603, 859, 1179, 1627, 4379, 4635, 6555, 7451, 7835, 7931,
      9819, 10907, 11035, 13339, 14363, 14747, 15515, 15643, 15771, 16411,
      16635, 17659, 18523, 19099, 19547, 19707, 21595, 22555, 23707, 23963,
      24571, 24731, 25371, 25851, 26459, 26619, 27675, 27739, 28507, 30235,
      30971, 32283, 32763, 32859, 32923, 33531, 34651, 35419, 35579, 36635,
      36891, 37467, 38171, 38427, 39195, 40187, 41243, 41627, 41723, 42075,
      42651, 43611, 44699, 45083, 45851, 47099, 47387, 48155, 48379, 48987,
      49563, 50267, 50843, 51451, 51611, 52507, 52763, 53339, 54043, 55291,
      55963, 56059, 56315, 56347, 57179, 57755, 57947, 58203, 58523, 59643,
      60571, 60955, 61531, 61723, 61979, 64251, 64507, 65179, 65275} : 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/a9e5f2b4-a7c1-4554-8901-f8a736ba125f 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, including both modulus-8192 exclusion groups, and adds only nonmembership in the supporting theorem's explicit mod-2^18 list. The method was anticipated in the mission discussion, including Steve1136's September 21 and Zexuan Liu's September 8, 2026 comments, https://prove2.me/missions/Collatz_Conjecture. This integrates an existing certified refinement, not a new Collatz strategy or a theorem quoted from the literature.

View graph