Seven-branch Syracuse descent remaining after 194 further certified progressions
Opensyracuse_descent_residual_seven_mod32_mod262144iterationnumber-theorystopping-time
Let be the odd part of , and let denote its -fold iterate. Suppose satisfies all the congruence and exclusion hypotheses of the current seven-branch residual theorem. Let be exactly the 961-residue list used by syracuse_descent_progressions_mod262144, enumerated again in this theorem's formal statement. Add the hypothesis
The remaining open assertion is
This retains every hypothesis of the parent and excludes only classes handled by the uniform eleven-step certificate. Within this seven branch those are 194 progressions. Neither the starting value nor the descent time is bounded; this residual assertion is still unproved. The theorem is intended as the unresolved child of a case-split reduction, not as a restatement that the Collatz conjecture has been solved.
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_seven_mod32_mod262144 (n : ℕ)
(h : n % 128 = 39 ∨ n % 128 = 71 ∨ n % 128 = 103)
(h256 : n % 256 ≠ 39 ∧ n % 256 ≠ 199)
(h1024 : n % 1024 ≠ 423 ∧ n % 1024 ≠ 583 ∧ n % 1024 ≠ 999)
(h4096 : n % 4096 ≠ 231 ∧ n % 4096 ≠ 615 ∧ n % 4096 ≠ 935 ∧ n % 4096 ≠ 1703 ∧ n % 4096 ≠ 3143 ∧ n % 4096 ≠ 3559 ∧ n % 4096 ≠ 3911)
(h8192 : n % 8192 ∉ ({679, 1191, 2663, 3687, 4199, 4455, 5191, 5607, 5959, 6215,
6375, 6631, 6983, 7079, 7399, 7495, 7847, 7911, 8103} : Finset ℕ))
(h32768 : n % 32768 ∉ ({839, 1095, 2119, 2279, 2727, 2983, 3303, 4007, 6503, 6759,
7783, 9959, 10055, 11079, 11943, 12967, 14439, 16743, 16871, 17735,
17767, 19623, 20199, 21223, 23399, 24647, 24679, 25703, 25831, 26087,
26535, 27111, 27975, 28999, 29863, 30311, 30887} : Finset ℕ))
(h65536 : n % 65536 ∉ ({359, 1351, 2407, 2791, 2887, 3239, 3815, 4775, 5863, 6247,
7015, 8263, 8551, 9319, 9543, 10151, 10727, 11431, 12007, 12615,
12775, 13671, 13927, 14503, 15207, 16455, 17127, 17223, 17479, 17511,
18343, 18919, 19111, 19367, 19687, 20807, 21735, 22119, 22695, 22887,
23143, 25415, 25671, 26343, 26439, 27303, 27559, 27879, 28327, 31079,
31335, 33255, 34151, 34535, 34631, 36519, 37607, 37735, 40039, 41063,
41447, 42215, 42343, 42471, 43111, 43335, 44359, 45223, 45799, 46247,
46407, 48295, 49255, 50407, 50663, 51271, 51431, 52071, 52551, 53159,
53319, 54375, 54439, 55207, 56935, 57671, 58983, 59463, 59559, 59623,
60231, 61351, 62119, 62279, 63335, 63591, 64167, 64871, 65127} : 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 sorrySource
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.